diff --git a/library/hott/axioms/ua.lean b/library/hott/axioms/ua.lean
index aadaefd92..cd31e8eb8 100644
--- a/library/hott/axioms/ua.lean
+++ b/library/hott/axioms/ua.lean
@@ -5,4 +5,18 @@
 import hott.path hott.equiv
 open path Equiv
 
-axiom ua {A B : Type} [H : A ≃ B] : A ≈ B
+universe l
+variables (A B : Type.{l})
+
+private definition isequiv_path (H : A ≈ B) :=
+  (@IsEquiv.transport Type (λX, X) A B H)
+
+definition equiv_path (H : A ≈ B) : A ≃ B :=
+  Equiv_mk _ (isequiv_path A B H)
+
+axiom ua_equiv (A B : Type) : IsEquiv (equiv_path A B)
+
+definition ua_inst [instance] {A B : Type} := (@ua_equiv A B)
+
+definition ua {A B : Type} (H : A ≃ B) : A ≈ B :=
+  IsEquiv.inv (@equiv_path A B) H