feat(library/hott) add universe polymorphism to paths, truncation, etc... get stuck at ua to funext proof anyway

library/hott/funext_from_ua.lean

@@ -7,6 +7,8 @@ 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)
 
@@ -18,12 +20,11 @@ definition equiv_path {A B : Type} (H : A ≈ B) : A ≃ B :=
 definition ua_type := Π (A B : Type), IsEquiv (@equiv_path A B)
 
 context
-  parameters {ua : ua_type.{1}}
+  universe variables l k
+  parameter {ua : ua_type.{l+1}}
 
-  -- TODO base this theorem on UA instead of FunExt.
+  protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type}
-  -- IsEquiv.postcompose relies on FunExt!
+      {w : A → B} {H0 : IsEquiv w} : IsEquiv (@compose C A B w) :=
-  protected theorem ua_isequiv_postcompose {A B C : Type.{1}} {w : A → B} {H0 : IsEquiv w}
-      : IsEquiv (@compose C A B w) :=
     let w' := Equiv.mk w H0 in
     let eqinv : A ≈ B := (equiv_path⁻¹ w') in
     let eq' := equiv_path eqinv in
@@ -36,7 +37,7 @@ context
           from inv_eq eq' w' eqretr,
         have eqfin : (equiv_fun eq') ∘ ((equiv_fun eq')⁻¹ ∘ x) ≈ x,
           from (λ p,
-            (@path.rec_on Type.{1} A
+            (@path.rec_on Type.{l+1} A
               (λ B' p', Π (x' : C → B'), (equiv_fun (equiv_path p'))
                 ∘ ((equiv_fun (equiv_path p'))⁻¹ ∘ x') ≈ x')
               B p (λ x', idp))
@@ -66,7 +67,7 @@ context
   protected definition diagonal [reducible] (B : Type) : Type
     := Σ xy : B × B, pr₁ xy ≈ pr₂ xy
 
-  protected definition isequiv_src_compose {A B C : Type.{1}}
+  protected definition isequiv_src_compose {A B C : Type}
       : @IsEquiv (A → diagonal B)
                  (A → B)
                  (compose (pr₁ ∘ dpr1))
@@ -77,7 +78,7 @@ context
             (λ xy, prod.rec_on xy
               (λ b c p, path.rec_on p idp))))
 
-  protected definition isequiv_tgt_compose {A B C : Type.{1}}
+  protected definition isequiv_tgt_compose {A B C : Type}
       : @IsEquiv (A → diagonal B)
                  (A → B)
                  (compose (pr₂ ∘ dpr1))
@@ -88,7 +89,7 @@ context
             (λ xy, prod.rec_on xy
               (λ b c p, path.rec_on p idp))))
 
-  theorem ua_implies_funext_nondep {A B : Type.{1}}
+  theorem ua_implies_funext_nondep {A B : Type.{l+1}}
       : Π {f g : A → B}, f ∼ g → f ≈ g
     := (λ (f g : A → B) (p : f ∼ g),
           let d := λ (x : A), dpair (f x , f x) idp in
@@ -113,22 +114,30 @@ context
 end
 
 context
-  universe l
+  universe variables l k
-  parameters {ua1 : ua_type.{1}} {ua2 : ua_type.{2}}
+  parameters {ua1 : ua_type.{l+1}} {ua2 : ua_type.{l+2}}
+  --parameters {ua1 ua2 : ua_type}
 
   -- Now we use this to prove weak funext, which as we know
   -- implies (with dependent eta) also the strong dependent funext.
   set_option pp.universes true
+  check @ua_implies_funext_nondep
+  check @weak_funext_implies_funext
+  check @ua_type
+  definition lift : Type.{l+1} → Type.{l+2} := sorry
+
   theorem ua_implies_weak_funext : weak_funext
-    := (λ (A : Type.{1}) (P : A → Type.{1}) allcontr,
+    := (λ (A : Type.{l+1}) (P : A → Type.{l+1}) allcontr,
+          have liftA : Type.{l+2},
+            from lift A,
           let U := (λ (x : A), unit) in
           have pequiv : Πx, P x ≃ U x,
-            from (λ x, @equiv_contr_unit (P x) (allcontr x)),
+            from (λ x, @equiv_contr_unit(P x) (allcontr x)),
           have psim : Πx, P x ≈ U x,
             from (λ x, @IsEquiv.inv _ _
-              (@equiv_path.{1} (P x) (U x)) (ua1 (P x) (U x)) (pequiv x)),
+              (@equiv_path (P x) (U x)) (ua1 (P x) (U x)) (pequiv x)),
           have p : P ≈ U,
-            from sorry, --ua_implies_funext_nondep psim,
+            from @ua_implies_funext_nondep.{l} ua1 A Type.{l+1} P U psim,
           have tU' : is_contr (A → unit),
             from is_contr.mk (λ x, ⋆)
               (λ f, @ua_implies_funext_nondep ua1 _ _ _ _

library/hott/funext_varieties.lean

@@ -16,16 +16,16 @@ 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 :=
+definition naive_funext.{l} :=
-  Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f ≈ g
+  Π {A : Type.{l+1}} {P : A → Type.{l+2}} (f g : Πx, P x), (f ∼ g) → f ≈ g
 
 -- Weak funext says that a product of contractible types is contractible.
-definition weak_funext :=
+definition weak_funext.{l} :=
-  Π {A : Type₁} (P : A → Type₁) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
+  Π {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 :=
+definition funext_type.{l} :=
-  Π {A : Type₁} {P : A → Type₁} (f g : Πx, P x), IsEquiv (@apD10 A P f g)
+  Π {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
@@ -48,18 +48,18 @@ definition naive_funext_implies_weak_funext : naive_funext → weak_funext :=
     )
   )
 
-
 /- The less obvious direction is that WeakFunext implies Funext
   (and hence all three are logically equivalent).  The point is that under weak
   funext, the space of "pointwise homotopies" has the same universal property as
   the space of paths. -/
 
 context
-  parameters (wf : weak_funext) {A : Type₁} {B : A → Type₁} (f : Πx, B x)
+  universe l
+  parameters (wf : weak_funext.{l}) {A : Type.{l+1}} {B : A → Type.{l+2}} (f : Π x, B x)
 
-  protected definition idhtpy : f ∼ f := (λx, idp)
+  protected definition idhtpy : f ∼ f := (λ x, idp)
 
-  definition contr_basedhtpy [instance] : is_contr (Σ (g : Πx, B x), f ∼ g) :=
+  definition contr_basedhtpy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
     is_contr.mk (dpair f idhtpy)
       (λ dp, sigma.rec_on dp
         (λ (g : Π x, B x) (h : f ∼ g),
@@ -93,7 +93,9 @@ context
 end
 
 -- Now the proof is fairly easy; we can just use the same induction principle on both sides.
-theorem weak_funext_implies_funext : weak_funext → funext_type :=
+universe variable l
+
+theorem weak_funext_implies_funext : weak_funext.{l} → funext_type.{l} :=
   (λ wf A B f g,
     let eq_to_f := (λ g' x, f ≈ g') in
     let sim2path := htpy_ind wf f eq_to_f idp in

library/hott/path.lean

@@ -15,7 +15,7 @@ open function
 -- Path
 -- ----
 
-inductive path {A : Type} (a : A) : A → Type :=
+inductive path.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
 idpath : path a a
 
 namespace path

library/hott/trunc.lean

@@ -5,6 +5,7 @@
 
 import .path .logic data.nat.basic data.empty data.unit data.sigma .equiv
 open path nat sigma unit
+set_option pp.universes true
 
 -- Truncation levels
 -- -----------------
@@ -17,7 +18,7 @@ open path nat sigma unit
 
 namespace truncation
 
-  inductive trunc_index : Type :=
+  inductive trunc_index : Type₁ :=
   minus_two : trunc_index,
   trunc_S : trunc_index → trunc_index
 
@@ -58,13 +59,14 @@ namespace truncation
   -/
 
   structure contr_internal (A : Type₊) :=
-  (center : A) (contr : Π(a : A), center ≈ a)
+    (center : A) (contr : Π(a : A), center ≈ a)
 
-  definition is_trunc_internal (n : trunc_index) : Type₁ → Type₁ :=
+  definition is_trunc_internal (n : trunc_index) : Type₊ → Type₊ :=
-  trunc_index.rec_on n (λA, contr_internal A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y)))
+    trunc_index.rec_on n (λA, contr_internal A)
+      (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y)))
 
-  structure is_trunc [class] (n : trunc_index) (A : Type₁) :=
+  structure is_trunc [class] (n : trunc_index) (A : Type₊) :=
-  (to_internal : is_trunc_internal n A)
+    (to_internal : is_trunc_internal n A)
 
   -- should this be notation or definitions?
   notation `is_contr` := is_trunc -2
@@ -74,10 +76,10 @@ namespace truncation
   -- definition is_hprop := is_trunc -1
   -- definition is_hset  := is_trunc 0
 
-  variables {A B : Type₁}
+  variables {A B : Type₊}
 
   -- maybe rename to is_trunc_succ.mk
-  definition is_trunc_succ (A : Type₁) {n : trunc_index} [H : ∀x y : A, is_trunc n (x ≈ y)]
+  definition is_trunc_succ (A : Type₊) {n : trunc_index} [H : ∀x y : A, is_trunc n (x ≈ y)]
     : is_trunc n.+1 A :=
   is_trunc.mk (λ x y, is_trunc.to_internal)
 
@@ -90,7 +92,7 @@ namespace truncation
   definition is_contr.mk (center : A) (contr : Π(a : A), center ≈ a) : is_contr A :=
   is_trunc.mk (contr_internal.mk center contr)
 
-  definition center (A : Type₁) [H : is_contr A] : A :=
+  definition center (A : Type₊) [H : is_contr A] : A :=
   @contr_internal.center A is_trunc.to_internal
 
   definition contr [H : is_contr A] (a : A) : !center ≈ a :=
@@ -99,17 +101,17 @@ namespace truncation
   definition path_contr [H : is_contr A] (x y : A) : x ≈ y :=
   contr x⁻¹ ⬝ (contr y)
 
-  definition path2_contr {A : Type₁} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q :=
+  definition path2_contr {A : Type₊} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q :=
   have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp),
   K p⁻¹ ⬝ K q
 
-  definition contr_paths_contr [instance] {A : Type₁} [H : is_contr A] (x y : A) : is_contr (x ≈ y) :=
+  definition contr_paths_contr [instance] {A : Type₊} [H : is_contr A] (x y : A) : is_contr (x ≈ y) :=
   is_contr.mk !path_contr (λ p, !path2_contr)
 
   /- truncation is upward close -/
 
   -- n-types are also (n+1)-types
-  definition trunc_succ [instance] (A : Type₁) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A :=
+  definition trunc_succ [instance] (A : Type₊) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A :=
   trunc_index.rec_on n
     (λ A (H : is_contr A), !is_trunc_succ)
     (λ n IH A (H : is_trunc (n.+1) A), @is_trunc_succ _ _ (λ x y, IH _ !succ_is_trunc))
@@ -117,15 +119,15 @@ namespace truncation
   --in the proof the type of H is given explicitly to make it available for class inference
 
 
-  definition trunc_leq (A : Type₁) (n m : trunc_index) (Hnm : n ≤ m)
+  definition trunc_leq (A : Type₊) (n m : trunc_index) (Hnm : n ≤ m)
     [Hn : is_trunc n A] : is_trunc m A :=
   have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from
     λ k A, trunc_index.cases_on k
            (λh1 h2, h2)
            (λk h1 h2, empty.elim (is_trunc -2 A) (trunc_index.not_succ_le_minus_two h1)),
   have step : Π (m : trunc_index)
-                (IHm : Π (n : trunc_index) (A : Type₁), n ≤ m → is_trunc n A → is_trunc m A)
+                (IHm : Π (n : trunc_index) (A : Type₊), n ≤ m → is_trunc n A → is_trunc m A)
-                (n : trunc_index) (A : Type₁)
+                (n : trunc_index) (A : Type₊)
                 (Hnm : n ≤ m .+1) (Hn : is_trunc n A), is_trunc m .+1 A, from
     λm IHm n, trunc_index.rec_on n
            (λA Hnm Hn, @trunc_succ A m (IHm -2 A star Hn))
@@ -134,14 +136,14 @@ namespace truncation
   trunc_index.rec_on m base step n A Hnm Hn
 
   -- the following cannot be instances in their current form, because it is looping
-  definition trunc_contr (A : Type₁) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
+  definition trunc_contr (A : Type₊) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
   trunc_index.rec_on n H _
 
-  definition trunc_hprop (A : Type₁) (n : trunc_index) [H : is_hprop A]
+  definition trunc_hprop (A : Type₊) (n : trunc_index) [H : is_hprop A]
       : is_trunc (n.+1) A :=
   trunc_leq A -1 (n.+1) star
 
-  definition trunc_hset (A : Type₁) (n : trunc_index) [H : is_hset A]
+  definition trunc_hset (A : Type₊) (n : trunc_index) [H : is_hset A]
       : is_trunc (n.+2) A :=
   trunc_leq A 0 (n.+2) star
 
@@ -150,22 +152,22 @@ namespace truncation
   definition is_hprop.elim [H : is_hprop A] (x y : A) : x ≈ y :=
   @center _ !succ_is_trunc
 
-  definition contr_inhabited_hprop {A : Type₁} [H : is_hprop A] (x : A) : is_contr A :=
+  definition contr_inhabited_hprop {A : Type₊} [H : is_hprop A] (x : A) : is_contr A :=
   is_contr.mk x (λy, !is_hprop.elim)
 
   --Coq has the following as instance, but doesn't look too useful
-  definition hprop_inhabited_contr {A : Type₁} (H : A → is_contr A) : is_hprop A :=
+  definition hprop_inhabited_contr {A : Type₊} (H : A → is_contr A) : is_hprop A :=
   @is_trunc_succ A -2
     (λx y,
       have H2 [visible] : is_contr A, from H x,
       !contr_paths_contr)
 
-  definition is_hprop.mk {A : Type₁} (H : ∀x y : A, x ≈ y) : is_hprop A :=
+  definition is_hprop.mk {A : Type₊} (H : ∀x y : A, x ≈ y) : is_hprop A :=
   hprop_inhabited_contr (λ x, is_contr.mk x (H x))
 
   /- hsets -/
 
-  definition is_hset.mk (A : Type₁) (H : ∀(x y : A) (p q : x ≈ y), p ≈ q) : is_hset A :=
+  definition is_hset.mk (A : Type₊) (H : ∀(x y : A) (p q : x ≈ y), p ≈ q) : is_hset A :=
   @is_trunc_succ _ _ (λ x y, is_hprop.mk (H x y))
 
   definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x ≈ y) : p ≈ q :=
@@ -173,7 +175,7 @@ namespace truncation
 
   /- instances -/
 
-  definition contr_basedpaths [instance] {A : Type₁} (a : A) : is_contr (Σ(x : A), a ≈ x) :=
+  definition contr_basedpaths [instance] {A : Type₊} (a : A) : is_contr (Σ(x : A), a ≈ x) :=
   is_contr.mk (dpair a idp) (λp, sigma.rec_on p (λ b q, path.rec_on q idp))
 
   definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry