From fd47a162def31f41a8ac232f100330f17f6a326c Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Wed, 19 Nov 2014 23:54:34 -0500
Subject: [PATCH] chore(library/hott) adapted theories to typeclass axioms

---
 library/hott/axioms/funext.lean    |  4 ++--
 library/hott/funext_from_ua.lean   |  4 +---
 library/hott/funext_varieties.lean | 27 ++++++++++++---------------
 3 files changed, 15 insertions(+), 20 deletions(-)

diff --git a/library/hott/axioms/funext.lean b/library/hott/axioms/funext.lean
index e0c6934dd..a17d79ff5 100644
--- a/library/hott/axioms/funext.lean
+++ b/library/hott/axioms/funext.lean
@@ -23,11 +23,11 @@ namespace funext
     universe l
     parameters [F : funext.{l}] {A : Type.{l+1}} {P : A → Type.{l+2}} (f g : Π x, P x)
 
-    protected definition equiv [instance] : IsEquiv (@apD10 A P f g) :=
+    protected definition apply [instance] : IsEquiv (@apD10 A P f g) :=
       rec_on F (λ H, sorry)
 
     definition path_forall : f ∼ g → f ≈ g :=
-      @IsEquiv.inv _ _ (@apD10 A P f g) equiv
+      @IsEquiv.inv _ _ (@apD10 A P f g) apply
 
   end
 
diff --git a/library/hott/funext_from_ua.lean b/library/hott/funext_from_ua.lean
index efd0cf207..490c200ed 100644
--- a/library/hott/funext_from_ua.lean
+++ b/library/hott/funext_from_ua.lean
@@ -7,8 +7,6 @@ import data.prod data.sigma data.unit
 
 open path function prod sigma truncation Equiv IsEquiv unit
 
-set_option pp.universes true
-
 definition isequiv_path {A B : Type} (H : A ≈ B) :=
   (@IsEquiv.transport Type (λX, X) A B H)
 
@@ -20,7 +18,7 @@ definition equiv_path {A B : Type} (H : A ≈ B) : A ≃ B :=
 definition ua_type := Π (A B : Type), IsEquiv (@equiv_path A B)
 
 context
-  universe variables l k
+  universe variables l
   parameter {ua : ua_type.{l+1}}
 
   protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type}
diff --git a/library/hott/funext_varieties.lean b/library/hott/funext_varieties.lean
index c7df896e1..c593f5934 100644
--- a/library/hott/funext_varieties.lean
+++ b/library/hott/funext_varieties.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Jakob von Raumer
 -- Ported from Coq HoTT
-import hott.path hott.trunc hott.equiv
+import hott.path hott.trunc hott.equiv hott.axioms.funext
 
 open path truncation sigma function
 
@@ -23,15 +23,12 @@ definition naive_funext.{l} :=
 definition weak_funext.{l} :=
   Π {A : Type.{l+1}} (P : A → Type.{l+2}) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
 
--- We define a variant of [Funext] which does not invoke an axiom.
-definition funext_type.{l} :=
-  Π {A : Type.{l+1}} {P : A → Type.{l+2}} (f g : Πx, P x), IsEquiv (@apD10 A P f g)
-
 -- The obvious implications are Funext -> NaiveFunext -> WeakFunext
 -- TODO: Get class inference to work locally
-definition funext_implies_naive_funext : funext_type → naive_funext :=
-  (λ Fe A P f g h,
-    have Fefg: IsEquiv (@apD10 A P f g), from Fe A P f g,
+definition funext_implies_naive_funext [F : funext] : naive_funext :=
+  (λ A P f g h,
+    have Fefg: IsEquiv (@apD10 A P f g),
+      from (@funext.apply F A P f g),
     have eq1 : _, from (@IsEquiv.inv _ _ (@apD10 A P f g) Fefg h),
     eq1
   )
@@ -95,19 +92,19 @@ end
 -- Now the proof is fairly easy; we can just use the same induction principle on both sides.
 universe variable l
 
-theorem weak_funext_implies_funext : weak_funext.{l} → funext_type.{l} :=
-  (λ wf A B f g,
+theorem weak_funext_implies_funext (wf : weak_funext.{l}) : funext.{l} :=
+  funext.mk (λ A B f g,
     let eq_to_f := (λ g' x, f ≈ g') in
-    let sim2path := htpy_ind wf f eq_to_f idp in
+    let sim2path := htpy_ind _ f eq_to_f idp in
     have t1 : sim2path f (idhtpy f) ≈ idp,
-      proof htpy_ind_beta wf f eq_to_f idp qed,
+      proof htpy_ind_beta _ f eq_to_f idp qed,
     have t2 : apD10 (sim2path f (idhtpy f)) ≈ (idhtpy f),
       proof ap apD10 t1 qed,
     have sect : Sect (sim2path g) apD10,
-      proof (htpy_ind wf f (λ g' x, apD10 (sim2path g' x) ≈ x) t2) g qed,
+      proof (htpy_ind _ f (λ g' x, apD10 (sim2path g' x) ≈ x) t2) g qed,
     have retr : Sect apD10 (sim2path g),
-      from (λ h, path.rec_on h (htpy_ind_beta wf f _ idp)),
+      from (λ h, path.rec_on h (htpy_ind_beta _ f _ idp)),
     IsEquiv.adjointify apD10 (sim2path g) sect retr)
 
-definition naive_funext_implies_funext : naive_funext -> funext_type :=
+definition naive_funext_implies_funext : naive_funext -> funext :=
   compose weak_funext_implies_funext naive_funext_implies_weak_funext