CODEWITHSUNDEEP
agdacubical-type-theoryhomotopy-type-theory
Cactus
Cactus

Reputation: 27636

Is the univalence axiom injective?

Is the univalence axiom invertible (modulo paths)? Is it possible to prove, using Agda's Cubical library, to prove the following:

open import Cubical.Core.Glue

uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → 
  ua f ≡ ua g → equivFun f ≡ equivFun g

I suspect the above should hold, because in example 3.19 of the HoTT book, there is a step in the proof where an equivalence between two equivalences is used to prove the equivalence between their functions:

[...] so f is an equivalence. Hence, by univalence, f gives rise to a path p : A ≡ A.

If p were equal to refl A, then (again by univalence) f would equal the identity function of A.

Upvotes: 1

Views: 197

Answers (2)

Cactus
Cactus

Reputation: 27636

To put András's answer into code, we can prove injectivity of equivalency functions in general:

equivInj : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A ≃ B) → 
  ∀ x x′ → equivFun f x ≡ equivFun f x′ → x ≡ x′
equivInj f x x′ p = cong fst $ begin
  x , refl                   ≡⟨ sym (equivCtrPath f (equivFun f x) (x , refl)) ⟩
  equivCtr f (equivFun f x)  ≡⟨ equivCtrPath f (equivFun f x) (x′ , p) ⟩
  x′ , p ∎

and then given

univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)

we get

uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → ua f ≡ ua g → equivFun f ≡ equivFun g
uaInj {f = f} {g = g} = cong equivFun ∘ equivInj (invEquiv univalence) f g

The only problem is, univalence is not readily available in the Cubical library. Hopefully that is getting sorted out shortly.

UPDATE: In reaction to the above bug ticket, proof of univalence is now available in the Cubical library.

Upvotes: 1

András Kovács
András Kovács

Reputation: 30103

Sure, ua is an equivalence, so it's injective. In the HoTT book, the inverse of ua is idtoeqv, so by congruence idtoeqv (ua f) ≡ idtoeqv (ua g) and then by inverses f ≡ g. I'm not familiar with the contents of cubical Agda prelude but this should be provable since it follows directly from the statement of univalence.

Upvotes: 1

Related Questions