Is the univalence axiom injective?

Question

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.

Answer 1

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.