[SOLVED] Is the univalence axiom injective?

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.

Solution

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.