Parametric theorem implied by goal

Question

During some development using cubical-agda, I noticed (and later checked) that my current goal, if proven would also imply such theorem:

parametric? : ∀ ℓ →  Type (ℓ-suc ℓ)  
parametric? ℓ = (f : {A : Type ℓ} → List A ≃ List A)
                   → (A : Type ℓ) → length ∘ equivFun (f {A}) ≡ length

I suspect that this is example of parametric theorem, which is true, but is unprovable in cubical agda. Is it the case?

Can I safely assume that my current goal is also unprovable?

user_17232565 · Answer

Yes, because it's false in the standard (simplicial sets) model.

If excluded middle holds, we can define f : {A : Type ℓ} → List A ≃ List A by first doing a case analysis on whether A is contractible or not. If A is not contractible, f gives the identity equivalence, but if A is contractible, then List A is equivalent to Nat, and, f can give an equivalence that, e.g., permutes odds and evens.

Parametric theorem implied by goal

1 Answers