feat(library/hott) funext from ua now with arbitrary universe levels for funext!

library/hott/equiv_precomp.lean

@@ -5,8 +5,6 @@
 import hott.equiv hott.axioms.funext
 open path function funext
 
-set_option pp.universes true
-
 namespace IsEquiv
   context
 
@@ -44,8 +42,7 @@ namespace IsEquiv
 		... ≈ k ∘ (invC h) : !sect,
       eq1⁻¹
 
-  universe variable l
-  definition isequiv_precompose {A B : Type.{l}} (f : A → B) (Aeq : IsEquiv (precomp f A))
+  definition isequiv_precompose {A B : Type} (f : A → B) (Aeq : IsEquiv (precomp f A))
       (Beq : IsEquiv (precomp f B)) : (IsEquiv f) :=
     let invA := inv (precomp f A) in
     let invB := inv (precomp f B) in

library/hott/funext_from_ua.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jakob von Raumer
 -- Ported from Coq HoTT
-import hott.equiv hott.funext_varieties hott.axioms.ua
+import hott.equiv hott.funext_varieties hott.axioms.ua hott.axioms.funext
 import data.prod data.sigma data.unit
 
 open path function prod sigma truncation Equiv IsEquiv unit ua_type
@@ -101,37 +101,30 @@ context
 
 end
 
-context
-  universe variables l
-  parameters {ua2 : ua_type.{l+2}} {ua3 : ua_type.{l+3}}
+-- Now we use this to prove weak funext, which as we know
+-- implies (with dependent eta) also the strong dependent funext.
+universe variables l k
+theorem ua_implies_weak_funext [ua3 : ua_type.{k+1}] [ua4 : ua_type.{k+2}] : weak_funext.{l+1 k+1} :=
+  (λ (A : Type) (P : A → Type) allcontr,
+    let U := (λ (x : A), unit) in
+  have pequiv : Π (x : A), P x ≃ U x,
+    from (λ x, @equiv_contr_unit(P x) (allcontr x)),
+  have psim : Π (x : A), P x ≈ U x,
+    from (λ x, @IsEquiv.inv _ _
+      equiv_path ua_type.inst (pequiv x)),
+  have p : P ≈ U,
+    from @ua_implies_funext_nondep _ A Type P U psim,
+  have tU' : is_contr (A → unit),
+    from is_contr.mk (λ x, ⋆)
+      (λ f, @ua_implies_funext_nondep _ A unit (λ x, ⋆) f
+        (λ x, unit.rec_on (f x) idp)),
+  have tU : is_contr (Π x, U x),
+    from tU',
+  have tlast : is_contr (Πx, P x),
+    from path.transport _ (p⁻¹) tU,
+  tlast
+)
 
-  -- Now we use this to prove weak funext, which as we know
-  -- implies (with dependent eta) also the strong dependent funext.
-  theorem ua_implies_weak_funext : weak_funext.{l} :=
-    (λ (A : Type.{l+1}) (P : A → Type.{l+2}) allcontr,
-      let U := (λ (x : A), unit) in
-      have pequiv : Π (x : A), P x ≃ U x,
-        from (λ x, @equiv_contr_unit(P x) (allcontr x)),
-      have psim : Π (x : A), P x ≈ U x,
-        from (λ x, @IsEquiv.inv _ _
-          equiv_path ua_type.inst (pequiv x)),
-      have p : P ≈ U,
-        from @ua_implies_funext_nondep.{l+2 l+1} ua3 A Type.{l+2} P U psim,
-      have tU' : is_contr (A → unit),
-        from is_contr.mk (λ x, ⋆)
-          (λ f, @ua_implies_funext_nondep ua2 A unit (λ x, ⋆) f
-            (λ x, unit.rec_on (f x) idp)),
-      have tU : is_contr (Π x, U x),
-        from tU',
-      have tlast : is_contr (Πx, P x),
-        from path.transport _ (p⁻¹) tU,
-      tlast
-    )
-
-end
-
-exit
 -- In the following we will proof function extensionality using the univalence axiom
--- TODO: check out why I have to generalize on A and P here
-definition ua_implies_funext_type {ua : ua_type} : @funext_type :=
-  (λ A P, weak_funext_implies_funext (@ua_implies_visible]weak_funext ua))
+definition ua_implies_funext {ua ua2 : ua_type} : funext :=
+  weak_funext_implies_funext (@ua_implies_weak_funext ua ua2)

library/hott/funext_varieties.lean

@@ -16,12 +16,12 @@ open path truncation sigma function
 
 -- Naive funext is the simple assertion that pointwise equal functions are equal.
 -- TODO think about universe levels
-definition naive_funext.{l k} :=
-  Π {A : Type.{l}} {P : A → Type.{k}} (f g : Πx, P x), (f ∼ g) → f ≈ g
+definition naive_funext :=
+  Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f ≈ g
 
 -- Weak funext says that a product of contractible types is contractible.
-definition weak_funext.{l} :=
-  Π {A : Type.{l+1}} (P : A → Type.{l+2}) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
+definition weak_funext.{l k} :=
+  Π {A : Type.{l}} (P : A → Type.{k}) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
 
 -- The obvious implications are Funext -> NaiveFunext -> WeakFunext
 -- TODO: Get class inference to work locally
@@ -51,8 +51,8 @@ definition naive_funext_implies_weak_funext : naive_funext → weak_funext :=
   the space of paths. -/
 
 context
-  universe l
-  parameters (wf : weak_funext.{l}) {A : Type.{l+1}} {B : A → Type.{l+2}} (f : Π x, B x)
+  universes l k
+  parameters (wf : weak_funext.{l+1 k+1}) {A : Type.{l+1}} {B : A → Type.{k+1}} (f : Π x, B x)
 
   protected definition idhtpy : f ∼ f := (λ x, idp)
 
@@ -90,9 +90,9 @@ context
 end
 
 -- Now the proof is fairly easy; we can just use the same induction principle on both sides.
-universe variable l
+universe variables l k
 
-theorem weak_funext_implies_funext (wf : weak_funext.{l}) : funext.{l+1 l+2} :=
+theorem weak_funext_implies_funext (wf : weak_funext.{l+1 k+1}) : funext.{l+1 k+1} :=
   funext.mk (λ A B f g,
     let eq_to_f := (λ g' x, f ≈ g') in
     let sim2path := htpy_ind _ f eq_to_f idp in