Odtnhj

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.

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.

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.