From bc33af9f5160bfcb7b8bc071ee43dd054c973d1d Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Tue, 18 Nov 2014 20:51:58 -0500 Subject: [PATCH] feat(library/hott) add universe polymorphism to paths, truncation, etc... get stuck at ua to funext proof anyway --- library/hott/funext_from_ua.lean | 39 ++++++++++++++---------- library/hott/funext_varieties.lean | 24 ++++++++------- library/hott/path.lean | 2 +- library/hott/trunc.lean | 48 ++++++++++++++++-------------- 4 files changed, 63 insertions(+), 50 deletions(-) diff --git a/library/hott/funext_from_ua.lean b/library/hott/funext_from_ua.lean index 012caddf6..7e9b2094e 100644 --- a/library/hott/funext_from_ua.lean +++ b/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. - -- IsEquiv.postcompose relies on FunExt! - protected theorem ua_isequiv_postcompose {A B C : Type.{1}} {w : A → B} {H0 : IsEquiv w} - : IsEquiv (@compose C A B w) := + protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type} + {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 - parameters {ua1 : ua_type.{1}} {ua2 : ua_type.{2}} + universe variables l k + 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 _ _ _ _ diff --git a/library/hott/funext_varieties.lean b/library/hott/funext_varieties.lean index 3a218a44b..c7df896e1 100644 --- a/library/hott/funext_varieties.lean +++ b/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 := - Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f ≈ g +definition naive_funext.{l} := + Π {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 := - Π {A : Type₁} (P : A → Type₁) [H: Πx, is_contr (P x)], is_contr (Πx, P x) +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 := - Π {A : Type₁} {P : A → Type₁} (f g : Πx, P x), IsEquiv (@apD10 A P f g) +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 @@ -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 diff --git a/library/hott/path.lean b/library/hott/path.lean index 149eca7f0..34606e4a4 100644 --- a/library/hott/path.lean +++ b/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 diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index 64b416cc5..19d59958d 100644 --- a/library/hott/trunc.lean +++ b/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₁ := - trunc_index.rec_on n (λA, contr_internal A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) + 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))) - structure is_trunc [class] (n : trunc_index) (A : Type₁) := - (to_internal : is_trunc_internal n A) + structure is_trunc [class] (n : trunc_index) (A : Type₊) := + (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) - (n : trunc_index) (A : Type₁) + (IHm : Π (n : trunc_index) (A : Type₊), n ≤ m → is_trunc n A → is_trunc m A) + (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