From fa9cbb1f6a6d8e5a5bfae51d50efee8d4a17bcad Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Thu, 6 Nov 2014 18:35:31 -0500
Subject: [PATCH] chore(library/hott) adapted univalence axiom to suit notation
 in book and def in Coq.

---
 library/hott/axioms/ua.lean | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

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