feat(library/hott) change axioms to Leo's axioms-as-typeclass proposal

library/hott/axioms/funext.lean

@@ -7,18 +7,32 @@
 import hott.path hott.equiv
 open path
 
+set_option pp.universes true
+
 -- Funext
 -- ------
 
-axiom funext {A : Type} {P : A → Type} (f g : Πx, P x) : IsEquiv (@apD10 A P f g)
+-- Define function extensionality as a type class
+inductive funext.{l} [class] : Type.{l+3} :=
+  mk : (Π {A : Type.{l+1}} {P : A → Type.{l+2}} (f g : Π x, P x), IsEquiv (@apD10 A P f g))
+         → funext.{l}
 
-theorem funext_instance [instance] {A : Type} {P : A → Type} (f g : Πx, P x) :
-    IsEquiv (@apD10 A P f g) :=
-  @funext A P f g
+namespace funext
 
-definition path_forall {A : Type} {P : A → Type} (f g : Πx, P x) : f ∼ g → f ≈ g :=
-  IsEquiv.inv !apD10
+  context
+    universe l
+    parameters [F : funext.{l}] {A : Type.{l+1}} {P : A → Type.{l+2}} (f g : Π x, P x)
 
-definition path_forall2 {A B : Type} {P : A → B → Type} (f g : Πx y, P x y) :
-    (Πx y, f x y ≈ g x y) → f ≈ g :=
-  λE, path_forall f g (λx, path_forall (f x) (g x) (E x))
+    protected definition equiv [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
+
+  end
+
+  definition path_forall2 [F : funext] {A B : Type} {P : A → B → Type}
+      (f g : Πx y, P x y) : (Πx y, f x y ≈ g x y) → f ≈ g :=
+    λ E, path_forall f g (λx, path_forall (f x) (g x) (E x))
+
+end funext

library/hott/axioms/ua.lean

@@ -5,31 +5,48 @@
 import hott.path hott.equiv
 open path Equiv
 
+set_option pp.universes true
 --Ensure that the types compared are in the same universe
-universe variable l
-variables (A B : Type.{l})
+section
+  universe variable l
+  variables (A B : Type.{l})
 
-private definition isequiv_path (H : A ≈ B) :=
-  (@IsEquiv.transport Type (λX, X) A B H)
+  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)
+  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)
+end
 
--- Make the Equivalence given by the axiom an instance
-definition ua_inst [instance] {A B : Type} := (@ua_equiv A B)
+inductive ua_type [class] : Type :=
+  mk : (Π (A B : Type), IsEquiv (equiv_path A B)) → ua_type
 
--- This is the version of univalence axiom we will probably use most often
-definition ua {A B : Type} : A ≃ B →  A ≈ B :=
-  IsEquiv.inv (@equiv_path A B)
+namespace ua_type
+
+  context
+    universe k
+    parameters [F : ua_type.{k}] {A B: Type.{k}}
+
+    -- Make the Equivalence given by the axiom an instance
+    protected definition inst [instance] : IsEquiv (equiv_path A B) :=
+      rec_on F (λ H, sorry)
+
+    -- This is the version of univalence axiom we will probably use most often
+    definition ua : A ≃ B →  A ≈ B :=
+      @IsEquiv.inv _ _ (@equiv_path A B) inst
+
+  end
+
+end ua_type
 
 -- One consequence of UA is that we can transport along equivalencies of types
 namespace Equiv
+  universe variable l
 
-  protected definition subst (P : Type → Type) {A B : Type.{l}} (H : A ≃ B)
+  protected definition subst [UA : ua_type] (P : Type → Type) {A B : Type.{l}} (H : A ≃ B)
       : P A → P B :=
-    path.transport P (ua H)
+    path.transport P (ua_type.ua H)
 
   -- We can use this for calculation evironments
   calc_subst subst