From c5d31f76d75b2bfe7dd3f2ad00fe185d7967e34c Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 19 Aug 2018 13:51:12 +0200 Subject: [PATCH] move definitions from spectral repository here --- .../algebra/category/constructions/rezk.hlean | 2 +- hott/algebra/group_theory.hlean | 11 +- hott/algebra/homotopy_group.hlean | 42 ++- hott/algebra/inf_group.hlean | 4 + hott/arity.hlean | 29 +- hott/cubical/pathover2.hlean | 34 +- hott/cubical/square.hlean | 10 + hott/cubical/squareover.hlean | 40 ++- hott/eq2.hlean | 121 ++++--- hott/homotopy/circle.hlean | 2 +- hott/homotopy/connectedness.hlean | 25 +- hott/homotopy/homotopy_group.hlean | 41 ++- hott/init/equiv.hlean | 66 ++++ hott/init/nat.hlean | 5 +- hott/init/path.hlean | 12 +- hott/init/pathover.hlean | 4 + hott/types/eq.hlean | 36 +- hott/types/equiv.hlean | 35 +- hott/types/lift.hlean | 30 +- hott/types/nat/basic.hlean | 1 + hott/types/nat/hott.hlean | 60 +++- hott/types/pi.hlean | 33 +- hott/types/pointed.hlean | 118 ++++++- hott/types/pointed2.hlean | 161 +++------ hott/types/sigma.hlean | 16 +- hott/types/trunc.hlean | 320 +++++++++++++++++- 26 files changed, 990 insertions(+), 268 deletions(-) diff --git a/hott/algebra/category/constructions/rezk.hlean b/hott/algebra/category/constructions/rezk.hlean index b0d987668..6efa22df6 100644 --- a/hott/algebra/category/constructions/rezk.hlean +++ b/hott/algebra/category/constructions/rezk.hlean @@ -157,7 +157,7 @@ namespace rezk --induction b using rezk.rec with b' b' b g, --why does this not work if it works below? refine @rezk.rec _ _ _ (rezk_hom_left_pth_1_trunc a a' f) _ _ _ b, intro b, apply equiv_precompose (to_hom f⁻¹ⁱ), --how do i unfold properly at this point? - { intro b b' g, apply equiv_pathover, intro g' g'' H, + { intro b b' g, apply equiv_pathover2, intro g' g'' H, refine !pathover_rezk_hom_left_pt ⬝op _, refine !assoc ⬝ ap (λ x, x ∘ _) _, refine eq_of_parallel_po_right _ H, apply pathover_rezk_hom_left_pt }, diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index 8d1d01c49..778607a57 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -6,7 +6,7 @@ Authors: Floris van Doorn Basic group theory -/ -import algebra.category.category algebra.bundled .homomorphism +import algebra.category.category algebra.bundled .homomorphism types.pointed2 open eq algebra pointed function is_trunc pi equiv is_equiv set_option class.force_new true @@ -590,5 +590,14 @@ namespace group definition trivial_group_of_is_contr' (G : Group) [H : is_contr G] : G = G0 := eq_of_isomorphism (trivial_group_of_is_contr G) + definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) : + pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) := + begin + induction p, + apply pequiv_eq, + fapply phomotopy.mk, + { intro g, reflexivity }, + { apply is_prop.elim } + end end group diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 6a6844d71..80cebd131 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -11,7 +11,6 @@ import .trunc_group types.trunc .group_theory types.nat.hott open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv nat -- TODO: consistently make n an argument before A --- TODO: rename cghomotopy_group to aghomotopy_group -- TODO: rename homotopy_group_functor_compose to homotopy_group_functor_pcompose namespace eq @@ -60,14 +59,14 @@ namespace eq definition ghomotopy_group [constructor] (n : ℕ) [is_succ n] (A : Type*) : Group := Group.mk (π[n] A) _ - definition cghomotopy_group [constructor] (n : ℕ) [is_at_least_two n] (A : Type*) : AbGroup := + definition aghomotopy_group [constructor] (n : ℕ) [is_at_least_two n] (A : Type*) : AbGroup := AbGroup.mk (π[n] A) _ definition fundamental_group [constructor] (A : Type*) : Group := ghomotopy_group 1 A notation `πg[`:95 n:0 `]`:0 := ghomotopy_group n - notation `πag[`:95 n:0 `]`:0 := cghomotopy_group n + notation `πag[`:95 n:0 `]`:0 := aghomotopy_group n notation `π₁` := fundamental_group -- should this be notation for the group or pointed type? @@ -163,7 +162,7 @@ namespace eq [is_equiv f] : is_equiv (π→[n] f) := @(is_equiv_trunc_functor 0 _) !is_equiv_apn - definition homotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) : + definition homotopy_group_succ_in_natural (n : ℕ) {A B : Type*} (f : A →* B) : homotopy_group_succ_in B n ∘* π→[n + 1] f ~* π→[n] (Ω→ f) ∘* homotopy_group_succ_in A n := begin @@ -171,11 +170,15 @@ namespace eq exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f) end + definition homotopy_group_succ_in_natural_unpointed (n : ℕ) {A B : Type*} (f : A →* B) : + hsquare (homotopy_group_succ_in A n) (homotopy_group_succ_in B n) (π→[n+1] f) (π→[n] (Ω→ f)) := + (homotopy_group_succ_in_natural n f)⁻¹* + definition is_equiv_homotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B) [is_equiv (π→[n + 1] f)] : is_equiv (π→[n] (Ω→ f)) := have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in A n), from is_equiv_of_equiv_of_homotopy (equiv.mk (π→[n+1] f) _ ⬝e homotopy_group_succ_in B n) - (homotopy_group_functor_succ_phomotopy_in n f), + (homotopy_group_succ_in_natural n f), is_equiv.cancel_right (homotopy_group_succ_in A n) _ definition tinverse [constructor] {X : Type*} : π[1] X →* π[1] X := @@ -275,10 +278,39 @@ namespace eq apply homotopy_group_pequiv_loop_ptrunc_con} end + lemma ghomotopy_group_isomorphism_of_ptrunc_pequiv {A B : Type*} + (n k : ℕ) (H : n+1 ≤[ℕ] k) (f : ptrunc k A ≃* ptrunc k B) : πg[n+1] A ≃g πg[n+1] B := + (ghomotopy_group_ptrunc_of_le H A)⁻¹ᵍ ⬝g + homotopy_group_isomorphism_of_pequiv n f ⬝g + ghomotopy_group_ptrunc_of_le H B + + definition fundamental_group_isomorphism {X : Type*} {G : Group} + (e : Ω X ≃ G) (hom_e : Πp q, e (p ⬝ q) = e p * e q) : π₁ X ≃g G := + isomorphism_of_equiv (trunc_equiv_trunc 0 e ⬝e (trunc_equiv 0 G)) + begin intro p q, induction p with p, induction q with q, exact hom_e p q end + definition ghomotopy_group_ptrunc [constructor] (k : ℕ) [is_succ k] (A : Type*) : πg[k] (ptrunc k A) ≃g πg[k] A := ghomotopy_group_ptrunc_of_le (le.refl k) A + section psquare + variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*} + {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂} + {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} + + definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) := + !homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝* + !homotopy_group_functor_compose + + definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n] + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) := + begin + induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p)) + end + + end psquare + /- some homomorphisms -/ -- definition is_homomorphism_cast_loopn_succ_eq_in {A : Type*} (n : ℕ) : diff --git a/hott/algebra/inf_group.hlean b/hott/algebra/inf_group.hlean index 1340bd75e..3b54e86cd 100644 --- a/hott/algebra/inf_group.hlean +++ b/hott/algebra/inf_group.hlean @@ -582,6 +582,10 @@ section add_ab_inf_group theorem neg_neg_sub_neg (a b : A) : - (-a - -b) = a - b := by rewrite [neg_sub, sub_neg_eq_add, neg_add_eq_sub] + + definition add_sub_cancel_middle (a b : A) : a + (b - a) = b := + !add.comm ⬝ !sub_add_cancel + end add_ab_inf_group definition inf_group_of_add_inf_group (A : Type) [G : add_inf_group A] : inf_group A := diff --git a/hott/arity.hlean b/hott/arity.hlean index 946b8e88a..1c69dc047 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -51,6 +51,22 @@ namespace eq infix ` ~2 `:50 := homotopy2 infix ` ~3 `:50 := homotopy3 + definition homotopy2.refl {A} {B : A → Type} {C : Π⦃a⦄, B a → Type} (f : Πa (b : B a), C b) : + f ~2 f := + λa b, idp + + definition homotopy2.rfl [refl] {A} {B : A → Type} {C : Π⦃a⦄, B a → Type} + {f : Πa (b : B a), C b} : f ~2 f := + λa b, idp + + definition homotopy3.refl {A} {B : A → Type} {C : Πa, B a → Type} + {D : Π⦃a⦄ ⦃b : B a⦄, C a b → Type} (f : Πa b (c : C a b), D c) : f ~3 f := + λa b c, idp + + definition homotopy3.rfl {A} {B : A → Type} {C : Πa, B a → Type} + {D : Π⦃a⦄ ⦃b : B a⦄, C a b → Type} {f : Πa b (c : C a b), D c} : f ~3 f := + λa b c, idp + definition ap0111 (f : U → V → W → X) (Hu : u = u') (Hv : v = v') (Hw : w = w') : f u v w = f u' v' w' := by cases Hu; congruence; repeat assumption @@ -70,13 +86,13 @@ namespace eq : f u v w x y z = f u' v' w' x' y' z' := by cases Hu; congruence; repeat assumption - definition ap010 (f : X → Πa, B a) (Hx : x = x') : f x ~ f x' := + definition ap010 [unfold 7] (f : X → Πa, B a) (Hx : x = x') : f x ~ f x' := by intros; cases Hx; reflexivity - definition ap0100 (f : X → Πa b, C a b) (Hx : x = x') : f x ~2 f x' := + definition ap0100 [unfold 8] (f : X → Πa b, C a b) (Hx : x = x') : f x ~2 f x' := by intros; cases Hx; reflexivity - definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ~3 f x' := + definition ap01000 [unfold 9] (f : X → Πa b c, D a b c) (Hx : x = x') : f x ~3 f x' := by intros; cases Hx; reflexivity definition apdt011 (f : Πa, B a → Z) (Ha : a = a') (Hb : transport B Ha b = b') @@ -189,6 +205,13 @@ namespace eq : eq_of_homotopy3 (λa b c, H1 a b c ⬝ H2 a b c) = eq_of_homotopy3 H1 ⬝ eq_of_homotopy3 H2 := ap eq_of_homotopy (eq_of_homotopy (λa, !eq_of_homotopy2_con)) ⬝ !eq_of_homotopy_con + definition ap_apd0111 {A₁ A₂ A₃ : Type} {B : A₁ → Type} {C : Π⦃a⦄, B a → Type} {a a₂ : A₁} + {b : B a} {b₂ : B a₂} {c : C b} {c₂ : C b₂} + (g : A₂ → A₃) (f : Πa b, C b → A₂) (Ha : a = a₂) (Hb : b =[Ha] b₂) + (Hc : c =[apd011 C Ha Hb] c₂) : + ap g (apd0111 f Ha Hb Hc) = apd0111 (λa b c, (g (f a b c))) Ha Hb Hc := + by induction Hb; induction Hc using idp_rec_on; reflexivity + end eq open eq equiv is_equiv diff --git a/hott/cubical/pathover2.hlean b/hott/cubical/pathover2.hlean index 96c703819..5546aa6c7 100644 --- a/hott/cubical/pathover2.hlean +++ b/hott/cubical/pathover2.hlean @@ -30,7 +30,7 @@ namespace eq = change_path (ap_compose g f p) (pathover_ap B (g ∘ f) q) := by induction q; reflexivity - definition pathover_of_tr_eq_idp (r : b = b') : pathover_of_tr_eq r = pathover_idp_of_eq r := + definition pathover_idp_of_eq_def (r : b = b') : pathover_of_tr_eq r = pathover_idp_of_eq r := idp definition pathover_of_tr_eq_eq_concato (r : p ▸ b = b₂) @@ -134,4 +134,36 @@ namespace eq tr_eq_of_pathover (q ⬝op r) = tr_eq_of_pathover q ⬝ r := by induction r; reflexivity + definition pathover_tr_pathover_idp_of_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} {p : a = a'} + (q : b =[p] b') : + pathover_tr p b ⬝o pathover_idp_of_eq (tr_eq_of_pathover q) = q := + begin induction q; reflexivity end + + definition pathover_of_tr_eq_idp' {A : Type} {B : A → Type} {a a₂ : A} (p : a = a₂) (b : B a) : + pathover_of_tr_eq idp = pathover_tr p b := + by induction p; constructor + + definition eq_of_pathover_apo {A C : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} + {p : a = a'} (g : Πa, B a → C) (q : b =[p] b') : + eq_of_pathover (apo g q) = apd011 g p q := + by induction q; reflexivity + + definition pathover_ap_cono {A A' : Type} {a₁ a₂ a₃ : A} + {p₁ : a₁ = a₂} {p₂ : a₂ = a₃} (B' : A' → Type) (f : A → A') + {b₁ : B' (f a₁)} {b₂ : B' (f a₂)} {b₃ : B' (f a₃)} + (q₁ : b₁ =[p₁] b₂) (q₂ : b₂ =[p₂] b₃) : + pathover_ap B' f (q₁ ⬝o q₂) = + change_path !ap_con⁻¹ (pathover_ap B' f q₁ ⬝o pathover_ap B' f q₂) := + by induction q₁; induction q₂; reflexivity + + definition concato_eq_eq {A : Type} {B : A → Type} {a₁ a₂ : A} {p₁ : a₁ = a₂} + {b₁ : B a₁} {b₂ b₂' : B a₂} (r : b₁ =[p₁] b₂) (q : b₂ = b₂') : + r ⬝op q = r ⬝o pathover_idp_of_eq q := + by induction q; reflexivity + + definition eq_tr_of_pathover_con_tr_eq_of_pathover {A : Type} {B : A → Type} + {a₁ a₂ : A} (p : a₁ = a₂) {b₁ : B a₁} {b₂ : B a₂} (q : b₁ =[p] b₂) : + eq_tr_of_pathover q ⬝ tr_eq_of_pathover q⁻¹ᵒ = idp := + by induction q; reflexivity + end eq diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 643801194..dbe0724dc 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -722,4 +722,14 @@ namespace eq (r : p₂₁' = p₂₁) : aps f (q ⬝ph s₁₁ ⬝hp r⁻¹) = ap02 f q ⬝ph aps f s₁₁ ⬝hp (ap02 f r)⁻¹ := by induction q; induction r; reflexivity + definition eq_hconcat_equiv [constructor] {p : a₀₀ = a₀₂} (r : p = p₀₁) : + square p₁₀ p₁₂ p p₂₁ ≃ square p₁₀ p₁₂ p₀₁ p₂₁ := + equiv.MK (eq_hconcat r⁻¹) (eq_hconcat r) + begin intro s, induction r, reflexivity end begin intro s, induction r, reflexivity end + + definition hconcat_eq_equiv [constructor] {p : a₂₀ = a₂₂} (r : p₂₁ = p) : + square p₁₀ p₁₂ p₀₁ p₂₁ ≃ square p₁₀ p₁₂ p₀₁ p := + equiv.MK (λs, hconcat_eq s r) (λs, hconcat_eq s r⁻¹) + begin intro s, induction r, reflexivity end begin intro s, induction r, reflexivity end + end eq diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean index c3607ef9d..3513536be 100644 --- a/hott/cubical/squareover.hlean +++ b/hott/cubical/squareover.hlean @@ -35,6 +35,7 @@ namespace eq {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁} {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃} + {b : B a} {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₄₀ : B a₄₀} {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂} {b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄} @@ -117,9 +118,9 @@ namespace eq squareover B (sp ⬝ph s₁₁) q₁₀ q₁₂ q q₂₁ := by induction sp; induction r; exact t₁₁ - definition hconcato_pathover {p : a₂₀ = a₂₂} {sp : p₂₁ = p} {q : b₂₀ =[p] b₂₂} - (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : change_path sp q₂₁ = q) : - squareover B (s₁₁ ⬝hp sp) q₁₀ q₁₂ q₀₁ q := + definition hconcato_pathover {p : a₂₀ = a₂₂} {sp : p = p₂₁} {s : square p₁₀ p₁₂ p₀₁ p} + {q : b₂₀ =[p] b₂₂} (t₁₁ : squareover B (s ⬝hp sp) q₁₀ q₁₂ q₀₁ q₂₁) + (r : change_path sp q = q₂₁) : squareover B s q₁₀ q₁₂ q₀₁ q := by induction sp; induction r; exact t₁₁ infix ` ⬝ho `:69 := hconcato --type using \tr @@ -304,4 +305,37 @@ namespace eq exact square_dpair_eq_dpair s₁₁ t₁₁ end + definition move_right_of_top_over {p : a₀₀ = a} {p' : a = a₂₀} + {s : square p p₁₂ p₀₁ (p' ⬝ p₂₁)} {q : b₀₀ =[p] b} {q' : b =[p'] b₂₀} + (t : squareover B (move_top_of_right s) (q ⬝o q') q₁₂ q₀₁ q₂₁) : + squareover B s q q₁₂ q₀₁ (q' ⬝o q₂₁) := + begin induction q', induction q, induction q₂₁, exact t end + + /- TODO: replace the version in the library by this -/ + + variables (s₁₁ q₀₁ q₁₀ q₂₁ q₁₂) + definition squareover_fill_t : Σ (q : b₀₀ =[p₁₀] b₂₀), squareover B s₁₁ q q₁₂ q₀₁ q₂₁ := + begin + induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on, + induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ + end + + definition squareover_fill_b : Σ (q : b₀₂ =[p₁₂] b₂₂), squareover B s₁₁ q₁₀ q q₀₁ q₂₁ := + begin + induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on, + induction q₁₀ using idp_rec_on, exact ⟨idpo, idso⟩ + end + + definition squareover_fill_l : Σ (q : b₀₀ =[p₀₁] b₀₂), squareover B s₁₁ q₁₀ q₁₂ q q₂₁ := + begin + induction s₁₁, induction q₁₀ using idp_rec_on, induction q₂₁ using idp_rec_on, + induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ + end + + definition squareover_fill_r : Σ (q : b₂₀ =[p₂₁] b₂₂) , squareover B s₁₁ q₁₀ q₁₂ q₀₁ q := + begin + induction s₁₁, induction q₀₁ using idp_rec_on, induction q₁₀ using idp_rec_on, + induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ + end + end eq diff --git a/hott/eq2.hlean b/hott/eq2.hlean index 8bbf07af5..9ff14ca58 100644 --- a/hott/eq2.hlean +++ b/hott/eq2.hlean @@ -7,7 +7,7 @@ Theorems about 2-dimensional paths -/ import .cubical.square .function -open function is_equiv equiv +open function is_equiv equiv sigma trunc namespace eq variables {A B C : Type} {f : A → B} {a a' a₁ a₂ a₃ a₄ : A} {b b' : B} @@ -141,6 +141,10 @@ namespace eq : whisker_left p q⁻² ⬝ q = con.right_inv p := by cases q; reflexivity + definition whisker_left_idp_square {A : Type} {a a' : A} {p q : a = a'} (r : p = q) : + square (whisker_left idp r) r (idp_con p) (idp_con q) := + begin induction r, exact hrfl end + definition cast_fn_cast_square {A : Type} {B C : A → Type} (f : Π⦃a⦄, B a → C a) {a₁ a₂ : A} (p : a₁ = a₂) (q : a₂ = a₁) (r : p ⬝ q = idp) (b : B a₁) : cast (ap C q) (f (cast (ap B p) b)) = f b := @@ -206,53 +210,94 @@ namespace eq (q : p = p') : square (ap_constant p b) (ap_constant p' b) (ap02 (λx, b) q) idp := by induction q; exact vrfl - section hsquare - variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type} - {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀} - {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} {f₄₁ : A₄₀ → A₄₂} - {f₁₂ : A₀₂ → A₂₂} {f₃₂ : A₂₂ → A₄₂} - {f₀₃ : A₀₂ → A₀₄} {f₂₃ : A₂₂ → A₂₄} {f₄₃ : A₄₂ → A₄₄} - {f₁₄ : A₀₄ → A₂₄} {f₃₄ : A₂₄ → A₄₄} + definition ap_con_idp_left {A B : Type} (f : A → B) {a a' : A} (p : a = a') : + square (ap_con f idp p) idp (ap02 f (idp_con p)) (idp_con (ap f p)) := + begin induction p, exact ids end - definition hsquare [reducible] (f₁₀ : A₀₀ → A₂₀) (f₁₂ : A₀₂ → A₂₂) - (f₀₁ : A₀₀ → A₀₂) (f₂₁ : A₂₀ → A₂₂) : Type := - f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ + definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g') + (f : A → B) (a : A) : apd10 (ap (λg a, h (g (f a))) p) a = ap h (apd10 p (f a)) := + begin induction p, reflexivity end - definition hsquare_of_homotopy (p : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ := - p + definition apd10_prepostcompose {A B : Type} {C : B → Type} {D : A → Type} + (f : A → B) (h : Πa, C (f a) → D a) {g g' : Πb, C b} + (p : g = g') (a : A) : + apd10 (ap (λg a, h a (g (f a))) p) a = ap (h a) (apd10 p (f a)) := + begin induction p, reflexivity end - definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ := - p + /- alternative induction principles -/ + definition eq.rec_to {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₀ = a₁ → Type} + {a₁ : A} (p₀ : a₀ = a₁) (H : P p₀) ⦃a₂ : A⦄ (p : a₀ = a₂) : P p := + begin + induction p₀, induction p, exact H + end - definition homotopy_top_of_hsquare {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := - homotopy_inv_of_homotopy_post _ _ _ p + definition eq.rec_to2 {A : Type} {P : Π⦃a₀ a₁⦄, a₀ = a₁ → Type} + {a₀ a₀' a₁' : A} (p' : a₀' = a₁') (p₀ : a₀ = a₀') (H : P p') ⦃a₁ : A⦄ (p : a₀ = a₁) : P p := + begin + induction p₀, induction p', induction p, exact H + end - definition homotopy_top_of_hsquare' [is_equiv f₂₁] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := - homotopy_inv_of_homotopy_post _ _ _ p + definition eq.rec_right_inv {A : Type} (f : A ≃ A) {P : Π⦃a₀ a₁⦄, f a₀ = a₁ → Type} + (H : Πa, P (right_inv f a)) ⦃a₀ a₁ : A⦄ (p : f a₀ = a₁) : P p := + begin + revert a₀ p, refine equiv_rect f⁻¹ᵉ _ _, + intro a₀ p, exact eq.rec_to (right_inv f a₀) (H a₀) p, + end - definition hhconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : - hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ := - hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ p + definition eq.rec_equiv {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type} + (H : P (idpath (f a₀))) ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p := + begin + assert qr : Σ(q : a₀ = a₁), ap f q = p, + { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ }, + cases qr with q r, apply transport P r, induction q, exact H + end - definition hvconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) : - hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) := - hwhisker_left f₂₃ p ⬝hty hwhisker_right f₀₁ q + definition eq.rec_equiv_symm {A B : Type} {a₁ : A} (f : A ≃ B) {P : Π{a₀}, f a₀ = f a₁ → Type} + (H : P (idpath (f a₁))) ⦃a₀ : A⦄ (p : f a₀ = f a₁) : P p := + begin + assert qr : Σ(q : a₀ = a₁), ap f q = p, + { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ }, + cases qr with q r, apply transport P r, induction q, exact H + end - definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ := - λb, eq_inv_of_eq ((p (f₁₀⁻¹ᵉ b))⁻¹ ⬝ ap f₂₁ (to_right_inv f₁₀ b)) + definition eq.rec_equiv_to_same {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type} + ⦃a₁' : A⦄ (p' : f a₀ = f a₁') (H : P p') ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p := + begin + revert a₁' p' H a₁ p, + refine eq.rec_equiv f _, + exact eq.rec_equiv f + end - definition hvinverse {f₀₁ : A₀₀ ≃ A₀₂} {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ := - λa, inv_eq_of_eq (p (f₀₁⁻¹ᵉ a) ⬝ ap f₁₂ (to_right_inv f₀₁ a))⁻¹ + definition eq.rec_equiv_to {A A' B : Type} {a₀ : A} (f : A ≃ B) (g : A' ≃ B) + {P : Π{a₁}, f a₀ = g a₁ → Type} + ⦃a₁' : A'⦄ (p' : f a₀ = g a₁') (H : P p') ⦃a₁ : A'⦄ (p : f a₀ = g a₁) : P p := + begin + assert qr : Σ(q : g⁻¹ (f a₀) = a₁), (right_inv g (f a₀))⁻¹ ⬝ ap g q = p, + { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p), + whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ }, + assert q'r' : Σ(q' : g⁻¹ (f a₀) = a₁'), (right_inv g (f a₀))⁻¹ ⬝ ap g q' = p', + { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p'), + whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ }, + induction qr with q r, induction q'r' with q' r', + induction q, induction q', + induction r, induction r', + exact H + end - infix ` ⬝htyh `:73 := hhconcat - infix ` ⬝htyv `:73 := hvconcat - postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse - postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse + definition eq.rec_grading {A A' B : Type} {a : A} (f : A ≃ B) (g : A' ≃ B) + {P : Π{b}, f a = b → Type} + {a' : A'} (p' : f a = g a') (H : P p') ⦃b : B⦄ (p : f a = b) : P p := + begin + revert b p, refine equiv_rect g _ _, + exact eq.rec_equiv_to f g p' H + end - end hsquare + definition eq.rec_grading_unbased {A B B' C : Type} (f : A ≃ B) (g : B ≃ C) (h : B' ≃ C) + {P : Π{b c}, g b = c → Type} + {a' : A} {b' : B'} (p' : g (f a') = h b') (H : P p') ⦃b : B⦄ ⦃c : C⦄ (q : f a' = b) + (p : g b = c) : P p := + begin + induction q, exact eq.rec_grading (f ⬝e g) h p' H p + end end eq diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index 990806035..c36f7cc97 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -316,7 +316,7 @@ namespace circle begin induction x, { apply base_eq_base_equiv}, - { apply equiv_pathover, intro p p' q, apply pathover_of_eq, + { apply equiv_pathover2, intro p p' q, apply pathover_of_eq, note H := eq_of_square (square_of_pathover q), rewrite con_comm_base at H, note H' := cancel_left _ H, diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index 3fff7d6ef..cc6c20f15 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -458,11 +458,34 @@ namespace is_conn { intro f', reflexivity } end - definition is_contr_of_is_conn_of_is_trunc {n : ℕ₋₂} {A : Type} (H : is_trunc n A) (K : is_conn n A) : is_contr A := is_contr_equiv_closed (trunc_equiv n A) + definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A)) + (H2 : is_conn 0 A) : is_trunc (n.+2) A := + begin + apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ, + refine is_conn.elim -1 _ _, exact H + end + + lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A)) + (H2 : is_conn (m.-1) A) : is_trunc (m + n) A := + begin + revert A H H2; induction m with m IH: intro A H H2, + { rewrite [nat.zero_add], exact H }, + rewrite [succ_add], + apply is_trunc_succ_succ_of_is_trunc_loop, + { apply IH, + { apply is_trunc_equiv_closed _ !loopn_succ_in }, + apply is_conn_loop }, + exact is_conn_of_le _ (zero_le_of_nat m) + end + + lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A)) + (H2 : is_conn (m.-1) A) : is_trunc m A := + is_trunc_of_is_trunc_loopn m 0 A H H2 + end is_conn /- diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index 9d1acd6a4..4a9ae23f9 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -32,7 +32,7 @@ namespace is_trunc : is_contr (π[k] A) := begin have H3 : is_contr (ptrunc k A), from is_conn_of_le A (of_nat_le_of_nat H), - have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loop_of_is_trunc, + have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loopn_of_is_trunc, apply is_trunc_equiv_closed_rev, { apply equiv_of_pequiv (homotopy_group_pequiv_loop_ptrunc k A)} end @@ -206,6 +206,45 @@ namespace is_trunc cases A with A a, exact H k H' end + definition is_trunc_of_trivial_homotopy {n : ℕ} {m : ℕ₋₂} {A : Type} (H : is_trunc m A) + (H2 : Πk a, k > n → is_contr (π[k] (pointed.MK A a))) : is_trunc n A := + begin + fapply is_trunc_is_equiv_closed_rev, { exact @tr n A }, + apply whitehead_principle m, + { apply is_equiv_trunc_functor_of_is_conn_fun, + note z := is_conn_fun_tr n A, + apply is_conn_fun_of_le _ (of_nat_le_of_nat (zero_le n)), }, + intro a k, + apply @nat.lt_ge_by_cases n (k+1), + { intro H3, apply @is_equiv_of_is_contr, exact H2 _ _ H3, + refine @trivial_homotopy_group_of_is_trunc _ _ _ _ H3 }, + { intro H3, apply @(is_equiv_π_of_is_connected _ H3), apply is_conn_fun_tr } + end + + definition is_trunc_of_trivial_homotopy_pointed {n : ℕ} {m : ℕ₋₂} {A : Type*} (H : is_trunc m A) + (Hconn : is_conn 0 A) (H2 : Πk, k > n → is_contr (π[k] A)) : is_trunc n A := + begin + apply is_trunc_of_trivial_homotopy H, + intro k a H3, revert a, apply is_conn.elim -1, + cases A with A a₀, exact H2 k H3 + end + + definition is_trunc_of_is_trunc_succ {n : ℕ} {A : Type} (H : is_trunc (n.+1) A) + (H2 : Πa, is_contr (π[n+1] (pointed.MK A a))) : is_trunc n A := + begin + apply is_trunc_of_trivial_homotopy H, + intro k a H3, induction H3 with k H3 IH, exact H2 a, + apply @trivial_homotopy_group_of_is_trunc _ (n+1) _ H, exact succ_le_succ H3 + end + + definition is_trunc_of_is_trunc_succ_pointed {n : ℕ} {A : Type*} (H : is_trunc (n.+1) A) + (Hconn : is_conn 0 A) (H2 : is_contr (π[n+1] A)) : is_trunc n A := + begin + apply is_trunc_of_trivial_homotopy_pointed H Hconn, + intro k H3, induction H3 with k H3 IH, exact H2, + apply @trivial_homotopy_group_of_is_trunc _ (n+1) _ H, exact succ_le_succ H3 + end + definition ab_group_homotopy_group_of_is_conn (n : ℕ) (A : Type*) [H : is_conn 1 A] : ab_group (π[n] A) := begin diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 48f936cf8..b28bb959b 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -462,3 +462,69 @@ end is_equiv export [unfold] equiv export [unfold] is_equiv + +/- properties about squares of functions -/ +namespace eq + + section hsquare + variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type} + {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀} + {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} {f₄₁ : A₄₀ → A₄₂} + {f₁₂ : A₀₂ → A₂₂} {f₃₂ : A₂₂ → A₄₂} + {f₀₃ : A₀₂ → A₀₄} {f₂₃ : A₂₂ → A₂₄} {f₄₃ : A₄₂ → A₄₄} + {f₁₄ : A₀₄ → A₂₄} {f₃₄ : A₂₄ → A₄₄} + + definition hsquare [reducible] (f₁₀ : A₀₀ → A₂₀) (f₁₂ : A₀₂ → A₂₂) + (f₀₁ : A₀₀ → A₀₂) (f₂₁ : A₂₀ → A₂₂) : Type := + f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ + + definition hsquare_of_homotopy (p : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ := + p + + definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ := + p + + definition homotopy_top_of_hsquare {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := + homotopy_inv_of_homotopy_post _ _ _ p + + definition homotopy_top_of_hsquare' [is_equiv f₂₁] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := + homotopy_inv_of_homotopy_post _ _ _ p + + definition hhconcat [unfold_full] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : + hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ := + hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ p + + definition hvconcat [unfold_full] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) : + hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) := + hwhisker_left f₂₃ p ⬝hty hwhisker_right f₀₁ q + + definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ := + λb, eq_inv_of_eq ((p (f₁₀⁻¹ᵉ b))⁻¹ ⬝ ap f₂₁ (to_right_inv f₁₀ b)) + + definition hvinverse {f₀₁ : A₀₀ ≃ A₀₂} {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ := + λa, inv_eq_of_eq (p (f₀₁⁻¹ᵉ a) ⬝ ap f₁₂ (to_right_inv f₀₁ a))⁻¹ + + infix ` ⬝htyh `:73 := hhconcat + infix ` ⬝htyv `:73 := hvconcat + postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse + postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse + + definition rfl_hhconcat (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : homotopy.rfl ⬝htyh q ~ q := + homotopy.rfl + + definition hhconcat_rfl (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : q ⬝htyh homotopy.rfl ~ q := + λx, !idp_con ⬝ ap_id (q x) + + definition rfl_hvconcat (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : homotopy.rfl ⬝htyv q ~ q := + λx, !idp_con + + definition hvconcat_rfl (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : q ⬝htyv homotopy.rfl ~ q := + λx, !ap_id + + end hsquare + +end eq diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index be8aff41a..d6b63d941 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -102,9 +102,10 @@ namespace nat protected definition le_trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k := le.rec H1 (λp H2, le.step) - definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := nat.le_trans H !le_succ + definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.step H - definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := nat.le_trans !le_succ H + definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := + by induction H with H m H'; exact le_succ n; exact le.step H' protected definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H diff --git a/hott/init/path.hlean b/hott/init/path.hlean index e80308050..39f9650d2 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -275,20 +275,20 @@ namespace eq definition hassoc {A B C D : Type} (h : C → D) (g : B → C) (f : A → B) : (h ∘ g) ∘ f ~ h ∘ (g ∘ f) := λa, idp - definition homotopy_of_eq {f g : Πx, P x} (H1 : f = g) : f ~ g := - H1 ▸ homotopy.refl f + definition homotopy_of_eq [unfold 5] {f g : Πx, P x} (H : f = g) : f ~ g := + λa, ap (λh, h a) H definition apd10 [unfold 5] {f g : Πx, P x} (H : f = g) : f ~ g := - λx, by induction H; reflexivity + λa, ap (λh, h a) H --the next theorem is useful if you want to write "apply (apd10' a)" definition apd10' [unfold 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a := - by induction H; reflexivity + apd10 H a - --apd10 is also ap evaluation + --apd10 is a special case of ap definition apd10_eq_ap_eval {f g : Πx, P x} (H : f = g) (a : A) : apd10 H a = ap (λs : Πx, P x, s a) H := - by induction H; reflexivity + by reflexivity definition ap10 [reducible] [unfold 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index f27c7417b..c389bc86b 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -314,6 +314,10 @@ namespace eq (q : f =[p] g) (r : b =[p] b₂) : f b = g b₂ := eq_of_pathover (apo11 q r) + definition apd02 [unfold 8] (f : Πa, B a) {a a' : A} {p q : a = a'} + (r : p = q) : change_path r (apd f p) = apd f q := + by induction r; reflexivity + /- properties about these "ap"s, transporto and pathover_ap -/ definition apd_con (f : Πa, B a) (p : a = a₂) (q : a₂ = a₃) : apd f (p ⬝ q) = apd f p ⬝o apd f q := diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index c995f6d52..77bf5cb7f 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -83,6 +83,7 @@ namespace eq !idp_con⁻¹ ⬝ whisker_left idp r = r ⬝ !idp_con⁻¹ := by induction r;induction q;reflexivity + -- this should maybe replace whisker_left_idp and whisker_left_idp_con definition whisker_left_idp_con {q q' : a₂ = a₃} (r : q = q') : whisker_left idp r ⬝ !idp_con = !idp_con ⬝ r := by induction r;induction q;reflexivity @@ -461,31 +462,36 @@ namespace eq section parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a)) - (p : (center (Σa, code a)).1 = a₀) - include p + (c₀ : code a₀) + include H c₀ protected definition encode {a : A} (q : a₀ = a) : code a := - (p ⬝ q) ▸ (center (Σa, code a)).2 + transport code q c₀ protected definition decode' {a : A} (c : code a) : a₀ = a := - (is_prop.elim ⟨a₀, encode idp⟩ ⟨a, c⟩)..1 + have ⟨a₀, c₀⟩ = ⟨a, c⟩ :> Σa, code a, from !is_prop.elim, + this..1 protected definition decode {a : A} (c : code a) : a₀ = a := - (decode' (encode idp))⁻¹ ⬝ decode' c + (decode' c₀)⁻¹ ⬝ decode' c + open sigma.ops definition total_space_method (a : A) : (a₀ = a) ≃ code a := begin fapply equiv.MK, - { exact encode}, - { exact decode}, - { intro c, - unfold [encode, decode, decode'], - induction p, esimp, rewrite [is_prop_elim_self,▸*,+idp_con], - apply tr_eq_of_pathover, - eapply @sigma.rec_on _ _ (λx, x.2 =[(is_prop.elim ⟨x.1, x.2⟩ ⟨a, c⟩)..1] c) - (center (sigma code)), - intro a c, apply eq_pr2}, + { exact encode }, + { exact decode }, + { intro c, unfold [encode, decode, decode'], + rewrite [is_prop_elim_self, ▸*, idp_con], + apply tr_eq_of_pathover, apply eq_pr2 }, { intro q, induction q, esimp, apply con.left_inv, }, end + + end + + definition total_space_method2_refl {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a)) + (c₀ : code a₀) : total_space_method a₀ code H c₀ a₀ idp = c₀ := + begin + reflexivity end definition encode_decode_method {A : Type} (a₀ a : A) (code : A → Type) (c₀ : code a₀) @@ -498,7 +504,7 @@ namespace eq { intro p, fapply sigma_eq, apply decode, exact p.2, apply encode_decode}}, - { reflexivity} + { exact c₀ } end end eq diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index e36a4181a..10a584987 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -228,6 +228,14 @@ namespace equiv definition equiv_eq {f f' : A ≃ B} (p : to_fun f ~ to_fun f') : f = f' := by apply equiv_eq'; apply eq_of_homotopy p + definition ap_equiv_eq {X Y : Type} {e e' : X ≃ Y} (p : e ~ e') (x : X) : + ap (λ(e : X ≃ Y), e x) (equiv_eq p) = p x := + begin + cases e with e He, cases e' with e' He', esimp at *, esimp [equiv_eq], + refine homotopy.rec_on' p _, intro q, induction q, esimp [equiv_eq', equiv_mk_eq], + assert H : He = He', apply is_prop.elim, induction H, rewrite [is_prop_elimo_self] + end + definition trans_symm (f : A ≃ B) (g : B ≃ C) : (f ⬝e g)⁻¹ᵉ = g⁻¹ᵉ ⬝e f⁻¹ᵉ :> (C ≃ A) := equiv_eq' idp @@ -264,13 +272,30 @@ namespace equiv definition equiv_pathover {A : Type} {a a' : A} (p : a = a') {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') - (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g := + (r : to_fun f =[p] to_fun g) : f =[p] g := begin fapply pathover_of_fn_pathover_fn, - { intro a, apply equiv.sigma_char}, - { fapply sigma_pathover, - esimp, apply arrow_pathover, exact r, - apply is_prop.elimo} + { intro a, apply equiv.sigma_char }, + { apply sigma_pathover _ _ _ r, apply is_prop.elimo } + end + + definition equiv_pathover2 {A : Type} {a a' : A} (p : a = a') + {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') + (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g := + begin + apply equiv_pathover, apply arrow_pathover, exact r + end + + definition equiv_pathover_inv {A : Type} {a a' : A} (p : a = a') + {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') + (r : to_inv f =[p] to_inv g) : f =[p] g := + begin + /- this proof is a bit weird, but it works -/ + apply equiv_pathover, + change f⁻¹ᶠ⁻¹ᶠ =[p] g⁻¹ᶠ⁻¹ᶠ, + apply apo (λ(a: A) (h : C a ≃ B a), h⁻¹ᶠ), + apply equiv_pathover, + exact r end definition is_contr_equiv (A B : Type) [HA : is_contr A] [HB : is_contr B] : is_contr (A ≃ B) := diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean index 123f976ee..a6b603d81 100644 --- a/hott/types/lift.hlean +++ b/hott/types/lift.hlean @@ -138,14 +138,27 @@ namespace lift apply ua_refl} end + definition fiber_lift_functor {A B : Type} (f : A → B) (b : B) : + fiber (lift_functor f) (up b) ≃ fiber f b := + begin + fapply equiv.MK: intro v; cases v with a p, + { cases a with a, exact fiber.mk a (eq_of_fn_eq_fn' up p) }, + { exact fiber.mk (up a) (ap up p) }, + { apply ap (fiber.mk a), apply eq_of_fn_eq_fn'_ap }, + { cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_eq_of_fn_eq_fn' } + end + + definition lift_functor2 {A B C : Type} (f : A → B → C) (x : lift A) (y : lift B) : lift C := + up (f (down x) (down y)) + + -- is_trunc_lift is defined in init.trunc + definition plift [constructor] (A : pType.{u}) : pType.{max u v} := pointed.MK (lift A) (up pt) definition plift_functor [constructor] {A B : Type*} (f : A →* B) : plift A →* plift B := pmap.mk (lift_functor f) (ap up (respect_pt f)) - -- is_trunc_lift is defined in init.trunc - definition pup [constructor] {A : Type*} : A →* plift A := pmap.mk up idp @@ -164,15 +177,8 @@ namespace lift definition pequiv_plift [constructor] (A : Type*) : A ≃* plift A := pequiv_of_equiv (equiv_lift A) idp - definition fiber_lift_functor {A B : Type} (f : A → B) (b : B) : - fiber (lift_functor f) (up b) ≃ fiber f b := - begin - fapply equiv.MK: intro v; cases v with a p, - { cases a with a, exact fiber.mk a (eq_of_fn_eq_fn' up p) }, - { exact fiber.mk (up a) (ap up p) }, - { apply ap (fiber.mk a), apply eq_of_fn_eq_fn'_ap }, - { cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_eq_of_fn_eq_fn' } - end - + definition is_trunc_plift [instance] [priority 1450] (A : Type*) (n : ℕ₋₂) + [H : is_trunc n A] : is_trunc n (plift A) := + is_trunc_lift A n end lift diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean index 32f508782..210c0c384 100644 --- a/hott/types/nat/basic.hlean +++ b/hott/types/nat/basic.hlean @@ -315,4 +315,5 @@ definition iterate {A : Type} (op : A → A) : ℕ → A → A | (succ k) := λ a, op (iterate k a) notation f `^[`:80 n:0 `]`:0 := iterate f n + end diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean index 4cc9ac044..45ce90e11 100644 --- a/hott/types/nat/hott.hlean +++ b/hott/types/nat/hott.hlean @@ -137,6 +137,46 @@ namespace nat { exact H2 k} end + protected definition rec_down (P : ℕ → Type) (s : ℕ) (H0 : P s) (Hs : Πn, P (n+1) → P n) : P 0 := + begin + induction s with s IH, + { exact H0 }, + { exact IH (Hs s H0) } + end + + definition rec_down_le (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n) (Hs : Πn, P (n+1) → P n) + : Πn, P n := + begin + induction s with s IH: intro n, + { exact H0 n (zero_le n) }, + { apply IH, intro n' H, induction H with n' H IH2, apply Hs, exact H0 _ !le.refl, + exact H0 _ (succ_le_succ H) } + end + + definition rec_down_le_univ {P : ℕ → Type} {s : ℕ} {H0 : Π⦃n⦄, s ≤ n → P n} + {Hs : Π⦃n⦄, P (n+1) → P n} (Q : Π⦃n⦄, P n → P (n + 1) → Type) + (HQ0 : Πn (H : s ≤ n), Q (H0 H) (H0 (le.step H))) (HQs : Πn (p : P (n+1)), Q (Hs p) p) : + Πn, Q (rec_down_le P s H0 Hs n) (rec_down_le P s H0 Hs (n + 1)) := + begin + induction s with s IH: intro n, + { apply HQ0 }, + { apply IH, intro n' H, induction H with n' H IH2, + { esimp, apply HQs }, + { apply HQ0 }} + end + + definition rec_down_le_beta_ge (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n) + (Hs : Πn, P (n+1) → P n) (n : ℕ) (Hn : s ≤ n) : rec_down_le P s H0 Hs n = H0 n Hn := + begin + revert n Hn, induction s with s IH: intro n Hn, + { exact ap (H0 n) !is_prop.elim }, + { have Hn' : s ≤ n, from le.trans !self_le_succ Hn, + refine IH _ _ Hn' ⬝ _, + induction Hn' with n Hn' IH', + { exfalso, exact not_succ_le_self Hn }, + { exact ap (H0 (succ n)) !is_prop.elim }} + end + /- this inequality comes up a couple of times when using the freudenthal suspension theorem -/ definition add_mul_le_mul_add (n m k : ℕ) : n + (succ m) * k ≤ (succ m) * (n + k) := calc @@ -213,14 +253,26 @@ namespace nat refine ap (f^[n]) _ ⬝ !iterate_succ⁻¹, exact !to_right_inv⁻¹ } end + definition iterate_hsquare {A B : Type} {f : A → A} {g : B → B} + (h : A → B) (p : hsquare f g h h) (n : ℕ) : hsquare (f^[n]) (g^[n]) h h := + begin + induction n with n q, + exact homotopy.rfl, + exact q ⬝htyh p + end + definition iterate_commute {A : Type} {f g : A → A} (n : ℕ) (h : f ∘ g ~ g ∘ f) : - iterate f n ∘ g ~ g ∘ iterate f n := - by induction n with n IH; reflexivity; exact λx, ap f (IH x) ⬝ !h + f^[n] ∘ g ~ g ∘ f^[n] := + (iterate_hsquare g h⁻¹ʰᵗʸ n)⁻¹ʰᵗʸ definition iterate_equiv {A : Type} (f : A ≃ A) (n : ℕ) : A ≃ A := equiv.mk (iterate f n) (by induction n with n IH; apply is_equiv_id; exact is_equiv_compose f (iterate f n)) + definition iterate_equiv2 {A : Type} {C : A → Type} (f : A → A) (h : Πa, C a ≃ C (f a)) + (k : ℕ) (a : A) : C a ≃ C (f^[k] a) := + begin induction k with k IH, reflexivity, exact IH ⬝e h (f^[k] a) end + definition iterate_inv {A : Type} (f : A ≃ A) (n : ℕ) : (iterate_equiv f n)⁻¹ ~ iterate f⁻¹ n := begin @@ -235,6 +287,10 @@ namespace nat definition iterate_right_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f^[n] (f⁻¹ᵉ^[n] a) = a := ap (f^[n]) (iterate_inv f n a)⁻¹ ⬝ to_right_inv (iterate_equiv f n) a + /- the same theorem add_le_add_left but with a proof by structural induction -/ + definition nat.add_le_add_left2 {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m := + by induction H with m H H₂; reflexivity; exact le.step H₂ + end nat diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index cdf1aa77d..4bb6d0cf4 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -16,36 +16,15 @@ namespace pi {D : Πa b, C a b → Type} {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {f g : Πa, B a} - /- Paths -/ - - /- - Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values - in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ~ g]. - - This equivalence, however, is just the combination of [apd10] and function extensionality - [funext], and as such, [eq_of_homotopy] - - Now we show how these things compute. - -/ - - definition apd10_eq_of_homotopy (h : f ~ g) : apd10 (eq_of_homotopy h) ~ h := - apd10 (right_inv apd10 h) - - definition eq_of_homotopy_eta (p : f = g) : eq_of_homotopy (apd10 p) = p := - left_inv apd10 p - - definition eq_of_homotopy_idp (f : Πa, B a) : eq_of_homotopy (λx : A, refl (f x)) = refl f := - !eq_of_homotopy_eta + /- Paths are charactirized in [init/funext] -/ /- homotopy.symm is an equivalence -/ + definition homotopy.symm_symm {A : Type} {P : A → Type} {f g : Πx, P x} (H : f ~ g) : + H⁻¹ʰᵗʸ⁻¹ʰᵗʸ = H := + begin apply eq_of_homotopy, intro x, apply inv_inv end + definition is_equiv_homotopy_symm : is_equiv (homotopy.symm : f ~ g → g ~ f) := - begin - fapply adjointify homotopy.symm homotopy.symm, - { intro p, apply eq_of_homotopy, intro a, - unfold homotopy.symm, apply inv_inv }, - { intro p, apply eq_of_homotopy, intro a, - unfold homotopy.symm, apply inv_inv } - end + adjointify homotopy.symm homotopy.symm homotopy.symm_symm homotopy.symm_symm /- The identification of the path space of a dependent function space, diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 08ad9c7c3..c757843c6 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -70,13 +70,13 @@ namespace pointed : Σ(p : carrier A = carrier B :> Type), Point A =[p] Point B := by induction p; exact ⟨idp, idpo⟩ - protected definition pType.sigma_char.{u} : pType.{u} ≃ Σ(X : Type.{u}), X := + definition pType.sigma_char.{u} [constructor] : pType.{u} ≃ Σ(X : Type.{u}), X := begin fapply equiv.MK, - { intro x, induction x with X x, exact ⟨X, x⟩}, - { intro x, induction x with X x, exact pointed.MK X x}, - { intro x, induction x with X x, reflexivity}, - { intro x, induction x with X x, reflexivity}, + { intro X, exact ⟨X, pt⟩ }, + { intro X, exact pointed.MK X.1 X.2 }, + { intro x, induction x with X x, reflexivity }, + { intro x, induction x with X x, reflexivity }, end definition pType.eta_expand [constructor] (A : Type*) : Type* := @@ -168,6 +168,16 @@ namespace pointed definition pmap.eta_expand [constructor] {A B : Type*} (f : A →* B) : A →* B := pmap.mk f (respect_pt f) + definition pmap_eta [constructor] {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) := + begin + fapply phomotopy.mk, + reflexivity, + esimp, exact !idp_con + end + + definition pmap_eta_eq {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f := + begin induction f, reflexivity end + definition pmap_equiv_right (A : Type*) (B : Type) : (Σ(b : B), A →* (pointed.Mk b)) ≃ (A → B) := begin @@ -201,7 +211,7 @@ namespace pointed we generalize the definition of ap1 to arbitrary paths, so that we can prove properties about it using path induction (see for example ap1_gen_con and ap1_gen_con_natural) -/ - definition ap1_gen [reducible] [unfold 6 9 10] {A B : Type} (f : A → B) {a a' : A} + definition ap1_gen [reducible] [unfold 8 9 10] {A B : Type} (f : A → B) {a a' : A} {b b' : B} (q : f a = b) (q' : f a' = b') (p : a = a') : b = b' := q⁻¹ ⬝ ap f p ⬝ q' @@ -1189,4 +1199,100 @@ namespace pointed apply apn_succ_phomotopy_in end + section psquare + /- + Squares of pointed maps + + We treat expressions of the form + psquare f g h k :≡ k ∘* f ~* g ∘* h + as squares, where f is the top, g is the bottom, h is the left face and k is the right face. + Then the following are operations on squares + -/ + + variables {A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} + {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀} + {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂} + {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂} + {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} + {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} + + definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) + (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type := + f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ + + definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ := + p + + definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ := + p + + definition phdeg_square {f f' : A →* A'} (p : f ~* f') : psquare !pid !pid f f' := + !pcompose_pid ⬝* p⁻¹* ⬝* !pid_pcompose⁻¹* + definition pvdeg_square {f f' : A →* A'} (p : f ~* f') : psquare f f' !pid !pid := + !pid_pcompose ⬝* p ⬝* !pcompose_pid⁻¹* + + variables (f₀₁ f₁₀) + definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl + definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl + variables {f₀₁ f₁₀} + definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁ + definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀ + + definition phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) : + psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ := + !passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹* + + definition pvconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : + psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) := + !passoc ⬝* pwhisker_left _ p ⬝* !passoc⁻¹* ⬝* pwhisker_right _ q ⬝* !passoc + + definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ := + !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝* + pwhisker_left _ + (!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid) + + definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* := + (phinverse p⁻¹*)⁻¹* + + definition phomotopy_hconcat (q : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₀ f₁₂ f₀₁' f₂₁ := + p ⬝* pwhisker_left f₁₂ q⁻¹* + + definition hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) : + psquare f₁₀ f₁₂ f₀₁ f₂₁' := + pwhisker_right f₁₀ q ⬝* p + + definition phomotopy_vconcat (q : f₁₀' ~* f₁₀) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₀' f₁₂ f₀₁ f₂₁ := + pwhisker_left f₂₁ q ⬝* p + + definition vconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₁₂' ~* f₁₂) : + psquare f₁₀ f₁₂' f₀₁ f₂₁ := + p ⬝* pwhisker_right f₀₁ q⁻¹* + + infix ` ⬝h* `:73 := phconcat + infix ` ⬝v* `:73 := pvconcat + infixl ` ⬝hp* `:72 := hconcat_phomotopy + infixr ` ⬝ph* `:72 := phomotopy_hconcat + infixl ` ⬝vp* `:72 := vconcat_phomotopy + infixr ` ⬝pv* `:72 := phomotopy_vconcat + postfix `⁻¹ʰ*`:(max+1) := phinverse + postfix `⁻¹ᵛ*`:(max+1) := pvinverse + + definition pwhisker_tl (f : A →* A₀₀) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (f₁₀ ∘* f) f₁₂ (f₀₁ ∘* f) f₂₁ := + !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc + + definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) := + !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose + + definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) := + !apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose + + end psquare + end pointed diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index 8e2d145d5..0c664de1d 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -13,125 +13,13 @@ Contains -/ -import algebra.homotopy_group eq2 +import eq2 .unit -open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function bool +open pointed eq unit is_trunc trunc nat is_equiv equiv sigma function bool sigma.ops namespace pointed variables {A B C : Type*} {P : A → Type} {p₀ : P pt} {k k' l m n : ppi P p₀} - section psquare - /- - Squares of pointed maps - - We treat expressions of the form - psquare f g h k :≡ k ∘* f ~* g ∘* h - as squares, where f is the top, g is the bottom, h is the left face and k is the right face. - Then the following are operations on squares - -/ - - variables {A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} - {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀} - {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂} - {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂} - {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} - {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} - - definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) - (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type := - f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ - - definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ := - p - - definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ := - p - - definition phdeg_square {f f' : A →* A'} (p : f ~* f') : psquare !pid !pid f f' := - !pcompose_pid ⬝* p⁻¹* ⬝* !pid_pcompose⁻¹* - definition pvdeg_square {f f' : A →* A'} (p : f ~* f') : psquare f f' !pid !pid := - !pid_pcompose ⬝* p ⬝* !pcompose_pid⁻¹* - - variables (f₀₁ f₁₀) - definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl - definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl - variables {f₀₁ f₁₀} - definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁ - definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀ - - definition phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) : - psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ := - !passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹* - - definition pvconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : - psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) := - !passoc ⬝* pwhisker_left _ p ⬝* !passoc⁻¹* ⬝* pwhisker_right _ q ⬝* !passoc - - definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ := - !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝* - pwhisker_left _ - (!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid) - - definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* := - (phinverse p⁻¹*)⁻¹* - - definition phomotopy_hconcat (q : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare f₁₀ f₁₂ f₀₁' f₂₁ := - p ⬝* pwhisker_left f₁₂ q⁻¹* - - definition hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) : - psquare f₁₀ f₁₂ f₀₁ f₂₁' := - pwhisker_right f₁₀ q ⬝* p - - definition phomotopy_vconcat (q : f₁₀' ~* f₁₀) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare f₁₀' f₁₂ f₀₁ f₂₁ := - pwhisker_left f₂₁ q ⬝* p - - definition vconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₁₂' ~* f₁₂) : - psquare f₁₀ f₁₂' f₀₁ f₂₁ := - p ⬝* pwhisker_right f₀₁ q⁻¹* - - infix ` ⬝h* `:73 := phconcat - infix ` ⬝v* `:73 := pvconcat - infixl ` ⬝hp* `:72 := hconcat_phomotopy - infixr ` ⬝ph* `:72 := phomotopy_hconcat - infixl ` ⬝vp* `:72 := vconcat_phomotopy - infixr ` ⬝pv* `:72 := phomotopy_vconcat - postfix `⁻¹ʰ*`:(max+1) := phinverse - postfix `⁻¹ᵛ*`:(max+1) := pvinverse - - definition pwhisker_tl (f : A →* A₀₀) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (f₁₀ ∘* f) f₁₂ (f₀₁ ∘* f) f₂₁ := - !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc - - definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) := - !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose - - definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) := - !apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose - - definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂) - (ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) := - !ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose - - definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) := - !homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝* - !homotopy_group_functor_compose - - definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n] - (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) := - begin - induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p)) - end - - end psquare - definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A := !phomotopy_of_is_contr_dom @@ -181,7 +69,7 @@ namespace pointed : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) ... ≃ Σ(p : to_homotopy h = to_homotopy k), whisker_right (respect_pt g) (apd10 p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h - : sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ !whisker_right_ap⁻¹)) + : by exact sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ (!whisker_right_ap⁻¹ᵖ))) ... ≃ Σ(p : to_homotopy h ~ to_homotopy k), whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h : sigma_equiv_sigma_left' eq_equiv_homotopy @@ -974,15 +862,42 @@ namespace pointed definition pequiv_eq {f g : A ≃* B} (H : f ~* g) : f = g := (pequiv_eq_equiv f g)⁻¹ᵉ H - open algebra - definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) : - pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) := + definition pequiv.sigma_char_equiv [constructor] (X Y : Type*) : + (X ≃* Y) ≃ Σ(e : X ≃ Y), e pt = pt := begin - induction p, - apply pequiv_eq, - fapply phomotopy.mk, - { intro g, reflexivity }, - { apply is_prop.elim } + fapply equiv.MK, + { intro e, exact ⟨equiv_of_pequiv e, respect_pt e⟩ }, + { intro e, exact pequiv_of_equiv e.1 e.2 }, + { intro e, induction e with e p, fapply sigma_eq, + apply equiv_eq, reflexivity, esimp, + apply eq_pathover_constant_right, esimp, + refine _ ⬝ph vrfl, + apply ap_equiv_eq }, + { intro e, apply pequiv_eq, fapply phomotopy.mk, intro x, reflexivity, + refine !idp_con ⬝ _, reflexivity }, + end + + definition pequiv.sigma_char_pmap [constructor] (X Y : Type*) : + (X ≃* Y) ≃ Σ(f : X →* Y), is_equiv f := + begin + fapply equiv.MK, + { intro e, exact ⟨ pequiv.to_pmap e , pequiv.to_is_equiv e ⟩ }, + { intro w, exact pequiv_of_pmap w.1 w.2 }, + { intro w, induction w with f p, fapply sigma_eq, + { reflexivity }, { apply is_prop.elimo } }, + { intro e, apply pequiv_eq, fapply phomotopy.mk, + { intro x, reflexivity }, + { refine !idp_con ⬝ _, reflexivity } } + end + + definition pType_eq_equiv (X Y : Type*) : (X = Y) ≃ (X ≃* Y) := + begin + refine eq_equiv_fn_eq pType.sigma_char X Y ⬝e !sigma_eq_equiv ⬝e _, esimp, + transitivity Σ(p : X = Y), cast p pt = pt, + apply sigma_equiv_sigma_right, intro p, apply pathover_equiv_tr_eq, + transitivity Σ(e : X ≃ Y), e pt = pt, + refine sigma_equiv_sigma (eq_equiv_equiv X Y) (λp, equiv.rfl), + exact (pequiv.sigma_char_equiv X Y)⁻¹ᵉ end end pointed diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index a5f52a8fc..452093ce7 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -120,6 +120,10 @@ namespace sigma sigma_eq (p1 ⬝ p2) (q1 ⬝o q2) = sigma_eq p1 q1 ⬝ sigma_eq p2 q2 := by induction u; induction v; induction w; apply dpair_eq_dpair_con + definition dpair_eq_dpair_inv {A : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} (p : a = a') + (q : b =[p] b') : (dpair_eq_dpair p q)⁻¹ = dpair_eq_dpair p⁻¹ q⁻¹ᵒ := + begin induction q, reflexivity end + local attribute dpair_eq_dpair [reducible] definition dpair_eq_dpair_con_idp (p : a = a') (q : b =[p] b') : dpair_eq_dpair p q = dpair_eq_dpair p !pathover_tr ⬝ @@ -466,23 +470,21 @@ namespace sigma /- *** The negative universal property. -/ - protected definition coind_unc (fg : Σ(f : Πa, B a), Πa, C a (f a)) (a : A) + protected definition coind_unc [constructor] (fg : Σ(f : Πa, B a), Πa, C a (f a)) (a : A) : Σ(b : B a), C a b := ⟨fg.1 a, fg.2 a⟩ - protected definition coind (f : Π a, B a) (g : Π a, C a (f a)) (a : A) : Σ(b : B a), C a b := + protected definition coind [constructor] (f : Π a, B a) (g : Π a, C a (f a)) (a : A) : Σ(b : B a), C a b := sigma.coind_unc ⟨f, g⟩ a - --is the instance below dangerous? - --in Coq this can be done without function extensionality - definition is_equiv_coind [instance] (C : Πa, B a → Type) + definition is_equiv_coind [constructor] (C : Πa, B a → Type) : is_equiv (@sigma.coind_unc _ _ C) := adjointify _ (λ h, ⟨λa, (h a).1, λa, (h a).2⟩) (λ h, proof eq_of_homotopy (λu, !sigma.eta) qed) (λfg, destruct fg (λ(f : Π (a : A), B a) (g : Π (x : A), C x (f x)), proof idp qed)) - definition sigma_pi_equiv_pi_sigma : (Σ(f : Πa, B a), Πa, C a (f a)) ≃ (Πa, Σb, C a b) := - equiv.mk sigma.coind_unc _ + definition sigma_pi_equiv_pi_sigma [constructor] : (Σ(f : Πa, B a), Πa, C a (f a)) ≃ (Πa, Σb, C a b) := + equiv.mk sigma.coind_unc !is_equiv_coind end /- Subtypes (sigma types whose second components are props) -/ diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index e83e76c86..c69d96308 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -8,10 +8,10 @@ Properties of trunc_index, is_trunc, trunctype, trunc, and the pointed versions -- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .prop_trunc -import .pointed ..function algebra.order types.nat.order types.unit +import .pointed2 ..function algebra.order types.nat.order types.unit types.int.hott open eq sigma sigma.ops pi function equiv trunctype - is_equiv prod pointed nat is_trunc algebra sum unit + is_equiv prod pointed nat is_trunc algebra unit /- basic computation with ℕ₋₂, its operations and its order -/ namespace trunc_index @@ -71,6 +71,7 @@ namespace trunc_index le.step (trunc_index.le.tr_refl n) -- the order is total + open sum protected theorem le_sum_le (n m : ℕ₋₂) : n ≤ m ⊎ m ≤ n := begin induction m with m IH, @@ -185,6 +186,23 @@ namespace trunc_index definition of_nat_add_two (n : ℕ₋₂) : of_nat (add_two n) = n.+2 := begin induction n with n IH, reflexivity, exact ap succ IH end + lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n := + by induction n with n p; reflexivity; exact ap succ p + + lemma add_plus_two_comm (n k : ℕ₋₂) : n +2+ k = k +2+ n := + begin + induction n with n IH, + { exact minus_two_add_plus_two k }, + { exact !succ_add_plus_two ⬝ ap succ IH} + end + + lemma sub_one_add_plus_two_sub_one (n m : ℕ) : n.-1 +2+ m.-1 = of_nat (n + m) := + begin + induction m with m IH, + { reflexivity }, + { exact ap succ IH } + end + definition of_nat_le_of_nat {n m : ℕ} (H : n ≤ m) : (of_nat n ≤ of_nat m) := begin induction H with m H IH, @@ -218,6 +236,13 @@ namespace trunc_index exact le_of_succ_le_succ (le_of_succ_le_succ H) end + protected definition of_nat_monotone {n k : ℕ} : n ≤ k → of_nat n ≤ of_nat k := + begin + intro H, induction H with k H K, + { apply le.tr_refl }, + { apply le.step K } + end + protected theorem succ_le_of_not_le {n m : ℕ₋₂} (H : ¬ n ≤ m) : m.+1 ≤ n := begin cases (le.total n m) with H2 H2, @@ -238,6 +263,15 @@ namespace trunc_index right, intro H2, apply H, exact le_of_succ_le_succ H2 end + protected definition pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ := + begin cases n with n, exact -2, exact n end + + definition trunc_index_equiv_nat [constructor] : ℕ₋₂ ≃ ℕ := + equiv.MK add_two sub_two add_two_sub_two sub_two_add_two + + definition is_set_trunc_index [instance] : is_set ℕ₋₂ := + is_trunc_equiv_closed_rev 0 trunc_index_equiv_nat + end trunc_index open trunc_index namespace is_trunc @@ -447,8 +481,7 @@ namespace is_trunc apply iff.mp !is_trunc_iff_is_contr_loop H end - -- rename to is_trunc_loopn_of_is_trunc - theorem is_trunc_loop_of_is_trunc (n : ℕ₋₂) (k : ℕ) (A : Type*) [H : is_trunc n A] : + theorem is_trunc_loopn_of_is_trunc (n : ℕ₋₂) (k : ℕ) (A : Type*) [H : is_trunc n A] : is_trunc n (Ω[k] A) := begin induction k with k IH, @@ -463,9 +496,20 @@ namespace is_trunc apply is_trunc_eq, apply IH, rewrite [succ_add_nat, add_nat_succ at H], exact H end + lemma is_trunc_loopn_nat (n m : ℕ) (A : Type*) [H : is_trunc (n + m) A] : + is_trunc n (Ω[m] A) := + @is_trunc_loopn n m A (transport (λk, is_trunc k _) (of_nat_add_of_nat n m)⁻¹ H) + definition is_set_loopn (n : ℕ) (A : Type*) [is_trunc n A] : is_set (Ω[n] A) := - have is_trunc (0+[ℕ₋₂]n) A, by rewrite [trunc_index.zero_add]; exact _, - is_trunc_loopn 0 n A + have is_trunc (0+n) A, by rewrite [zero_add]; exact _, + is_trunc_loopn_nat 0 n A + + lemma is_trunc_loop_nat (n : ℕ) (A : Type*) [H : is_trunc (n + 1) A] : + is_trunc n (Ω A) := + is_trunc_loop A n + + definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A := + transport (λk, is_trunc k A) p H definition pequiv_punit_of_is_contr [constructor] (A : Type*) (H : is_contr A) : A ≃* punit := pequiv_of_equiv (equiv_unit_of_is_contr A) (@is_prop.elim unit _ _ _) @@ -623,8 +667,8 @@ namespace trunc begin note H2 := is_trunc_of_le (trunc n A) H, fapply equiv.MK, - { intro x, induction x with x, induction x with x, exact tr x}, - { intro x, induction x with x, exact tr (tr x)}, + { intro x, induction x with x, induction x with x, exact tr x }, + { exact trunc_functor n tr }, { intro x, induction x with x, reflexivity}, { intro x, induction x with x, induction x with x, reflexivity} end @@ -663,6 +707,17 @@ namespace trunc induction x with x, esimp, exact ap tr (p x) end + section hsquare + variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type} + {f₁₀ : A₀₀ → A₂₀} {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} {f₁₂ : A₀₂ → A₂₂} + + definition trunc_functor_hsquare (n : ℕ₋₂) (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare (trunc_functor n f₁₀) (trunc_functor n f₁₂) + (trunc_functor n f₀₁) (trunc_functor n f₂₁) := + λa, !trunc_functor_compose⁻¹ ⬝ trunc_functor_homotopy n h a ⬝ !trunc_functor_compose + + end hsquare + definition trunc_functor_homotopy_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : n ≤ k) : to_fun (trunc_trunc_equiv_left B H) ∘ trunc_functor n (trunc_functor k f) ∘ @@ -693,6 +748,13 @@ namespace trunc definition ptrunc [constructor] (n : ℕ₋₂) (X : Type*) : n-Type* := ptrunctype.mk (trunc n X) _ (tr pt) + definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*) + (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) := + is_trunc_trunc_of_is_trunc A n m + + definition is_contr_ptrunc_minus_one (A : Type*) : is_contr (ptrunc -1 A) := + is_contr_of_inhabited_prop pt + /- pointed maps involving ptrunc -/ definition ptrunc_functor [constructor] {X Y : Type*} (n : ℕ₋₂) (f : X →* Y) : ptrunc n X →* ptrunc n Y := @@ -708,6 +770,11 @@ namespace trunc ptrunc n X →* Y := pmap.mk (trunc.elim f) (respect_pt f) + definition ptrunc_functor_le {k l : ℕ₋₂} (p : l ≤ k) (X : Type*) + : ptrunc k X →* ptrunc l X := + have is_trunc k (ptrunc l X), from is_trunc_of_le _ p, + ptrunc.elim _ (ptr l X) + /- pointed equivalences involving ptrunc -/ definition ptrunc_pequiv_ptrunc [constructor] (n : ℕ₋₂) {X Y : Type*} (H : X ≃* Y) : ptrunc n X ≃* ptrunc n Y := @@ -735,6 +802,10 @@ namespace trunc : ptrunc n (ptrunc m A) ≃* ptrunc m (ptrunc n A) := pequiv_of_equiv (trunc_trunc_equiv_trunc_trunc n m A) idp + definition ptrunc_change_index {k l : ℕ₋₂} (p : k = l) (X : Type*) + : ptrunc k X ≃* ptrunc l X := + pequiv_ap (λ n, ptrunc n X) p + definition loop_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A : Type*) : Ω (ptrunc (n+1) A) ≃* ptrunc n (Ω A) := pequiv_of_equiv !tr_eq_tr_equiv idp @@ -756,6 +827,10 @@ namespace trunc exact loopn_pequiv_loopn k (pequiv_of_eq (ap (λn, ptrunc n A) !succ_add_nat⁻¹)) } end + definition loopn_ptrunc_pequiv_nat (n k : ℕ) (A : Type*) : + Ω[k] (ptrunc (n + k) A) ≃* ptrunc n (Ω[k] A) := + loopn_pequiv_loopn k (ptrunc_change_index (of_nat_add_of_nat n k)⁻¹ A) ⬝e* loopn_ptrunc_pequiv n k A + definition loopn_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*} (p q : Ω[succ k] (ptrunc (n+succ k) A)) : loopn_ptrunc_pequiv n (succ k) A (p ⬝ q) = @@ -870,6 +945,114 @@ namespace trunc { esimp, exact !idp_con ⬝ whisker_right _ !ap_compose }, end + definition ptrunc_pequiv_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) [is_trunc n A] + [is_trunc n B] : f ∘* ptrunc_pequiv n A ~* ptrunc_pequiv n B ∘* ptrunc_functor n f := + begin + fapply phomotopy.mk, + { intro a, induction a with a, reflexivity }, + { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, refine !ap_compose'⁻¹ ⬝ _, apply ap_id } + end + + definition ptr_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) : + ptrunc_functor n f ∘* ptr n A ~* ptr n B ∘* f := + begin + fapply phomotopy.mk, + { intro a, reflexivity }, + { reflexivity } + end + + definition ptrunc_elim_pcompose (n : ℕ₋₂) {A B C : Type*} (g : B →* C) (f : A →* B) [is_trunc n B] + [is_trunc n C] : ptrunc.elim n (g ∘* f) ~* g ∘* ptrunc.elim n f := + begin + fapply phomotopy.mk, + { intro a, induction a with a, reflexivity }, + { apply idp_con } + end + + definition ptrunc_elim_ptr_phomotopy_pid (n : ℕ₋₂) (A : Type*): + ptrunc.elim n (ptr n A) ~* pid (ptrunc n A) := + begin + fapply phomotopy.mk, + { intro a, induction a with a, reflexivity }, + { apply idp_con } + end + + section psquare + variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*} + {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂} + {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} + + definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂) + (ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) := + !ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose + + end psquare + + definition is_equiv_ptrunc_functor_ptr [constructor] (A : Type*) {n m : ℕ₋₂} (H : n ≤ m) + : is_equiv (ptrunc_functor n (ptr m A)) := + to_is_equiv (trunc_trunc_equiv_left A H)⁻¹ᵉ + + -- The following pointed equivalence can be defined more easily, but now we get the right maps definitionally + definition ptrunc_pequiv_ptrunc_of_is_trunc {n m k : ℕ₋₂} {A : Type*} + (H1 : n ≤ m) (H2 : n ≤ k) (H : is_trunc n A) : ptrunc m A ≃* ptrunc k A := + have is_trunc m A, from is_trunc_of_le A H1, + have is_trunc k A, from is_trunc_of_le A H2, + pequiv.MK (ptrunc.elim _ (ptr k A)) (ptrunc.elim _ (ptr m A)) + abstract begin + refine !ptrunc_elim_pcompose⁻¹* ⬝* _, + exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid, + end end + abstract begin + refine !ptrunc_elim_pcompose⁻¹* ⬝* _, + exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid, + end end + + /- A more general version of ptrunc_elim_phomotopy, where the proofs of truncatedness might be different -/ + definition ptrunc_elim_phomotopy2 [constructor] (k : ℕ₋₂) {A B : Type*} {f g : A →* B} (H₁ : is_trunc k B) + (H₂ : is_trunc k B) (p : f ~* g) : @ptrunc.elim k A B H₁ f ~* @ptrunc.elim k A B H₂ g := + begin + fapply phomotopy.mk, + { intro x, induction x with a, exact p a }, + { exact to_homotopy_pt p } + end + + definition pmap_ptrunc_equiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] : + (ptrunc n A →* B) ≃ (A →* B) := + begin + fapply equiv.MK, + { intro g, exact g ∘* ptr n A }, + { exact ptrunc.elim n }, + { intro f, apply eq_of_phomotopy, apply ptrunc_elim_ptr }, + { intro g, apply eq_of_phomotopy, + exact ptrunc_elim_pcompose n g (ptr n A) ⬝* pwhisker_left g (ptrunc_elim_ptr_phomotopy_pid n A) ⬝* + pcompose_pid g } + end + + definition pmap_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] : + ppmap (ptrunc n A) B ≃* ppmap A B := + pequiv_of_equiv (pmap_ptrunc_equiv n A B) (eq_of_phomotopy (pconst_pcompose (ptr n A))) + + definition ptrunctype.sigma_char [constructor] (n : ℕ₋₂) : + n-Type* ≃ Σ(X : Type*), is_trunc n X := + equiv.MK (λX, ⟨ptrunctype.to_pType X, _⟩) + (λX, ptrunctype.mk (carrier X.1) X.2 pt) + begin intro X, induction X with X HX, induction X, reflexivity end + begin intro X, induction X, reflexivity end + + definition is_embedding_ptrunctype_to_pType (n : ℕ₋₂) : is_embedding (@ptrunctype.to_pType n) := + begin + intro X Y, fapply is_equiv_of_equiv_of_homotopy, + { exact eq_equiv_fn_eq (ptrunctype.sigma_char n) _ _ ⬝e subtype_eq_equiv _ _ }, + intro p, induction p, reflexivity + end + + definition ptrunctype_eq_equiv {n : ℕ₋₂} (X Y : n-Type*) : (X = Y) ≃ (X ≃* Y) := + equiv.mk _ (is_embedding_ptrunctype_to_pType n X Y) ⬝e pType_eq_equiv X Y + + definition Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q := + tua (equiv_of_is_prop (iff.mp H) (iff.mpr H)) + end trunc open trunc /- The truncated encode-decode method -/ @@ -950,3 +1133,124 @@ namespace function -- a homotopy group. end function + +/- functions between ℤ and ℕ₋₂ -/ +namespace int + + private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n := + le.intro ( + calc n + 1 + -[1+ k] + k + = n + 1 + (-(k + 1)) + k : by reflexivity + ... = n + 1 + (- 1 - k) + k : by krewrite (neg_add_rev k 1) + ... = n + 1 + (- 1 - k + k) : add.assoc + ... = n + 1 + (- 1 + -k + k) : by reflexivity + ... = n + 1 + (- 1 + (-k + k)) : add.assoc + ... = n + 1 + (- 1 + 0) : add.left_inv + ... = n + (1 + (- 1 + 0)) : add.assoc + ... = n : int.add_zero) + + private definition maxm2_le.lemma₂ {n : ℕ} {k : ℤ} : -[1+ n] + 1 + k ≤ k := + le.intro ( + calc -[1+ n] + 1 + k + n + = - (n + 1) + 1 + k + n : by reflexivity + ... = -n - 1 + 1 + k + n : by rewrite (neg_add n 1) + ... = -n + (- 1 + 1) + k + n : by krewrite (int.add_assoc (-n) (- 1) 1) + ... = -n + 0 + k + n : add.left_inv 1 + ... = -n + k + n : int.add_zero + ... = k + -n + n : int.add_comm + ... = k + (-n + n) : int.add_assoc + ... = k + 0 : add.left_inv n + ... = k : int.add_zero) + + open trunc_index + /- + The function from integers to truncation indices which sends + positive numbers to themselves, and negative numbers to negative + 2. In particular -1 is sent to -2, but since we only work with + pointed types, that doesn't matter for us -/ + definition maxm2 [unfold 1] : ℤ → ℕ₋₂ := + λ n, int.cases_on n trunc_index.of_nat (λk, -2) + + -- we also need the max -1 - function + definition maxm1 [unfold 1] : ℤ → ℕ₋₂ := + λ n, int.cases_on n trunc_index.of_nat (λk, -1) + + definition maxm2_le_maxm1 (n : ℤ) : maxm2 n ≤ maxm1 n := + begin + induction n with n n, + { exact le.tr_refl n }, + { exact minus_two_le -1 } + end + + -- the is maxm1 minus 1 + definition maxm1m1 [unfold 1] : ℤ → ℕ₋₂ := + λ n, int.cases_on n (λ k, k.-1) (λ k, -2) + + definition maxm1_eq_succ (n : ℤ) : maxm1 n = (maxm1m1 n).+1 := + begin + induction n with n n, + { reflexivity }, + { reflexivity } + end + + definition maxm2_le_maxm0 (n : ℤ) : maxm2 n ≤ max0 n := + begin + induction n with n n, + { exact le.tr_refl n }, + { exact minus_two_le 0 } + end + + definition max0_le_of_le {n : ℤ} {m : ℕ} (H : n ≤ of_nat m) + : nat.le (max0 n) m := + begin + induction n with n n, + { exact le_of_of_nat_le_of_nat H }, + { exact nat.zero_le m } + end + + definition not_neg_succ_le_of_nat {n m : ℕ} : ¬m ≤ -[1+n] := + by cases m: exact id + + definition maxm2_monotone {n m : ℤ} (H : n ≤ m) : maxm2 n ≤ maxm2 m := + begin + induction n with n n, + { induction m with m m, + { apply of_nat_le_of_nat, exact le_of_of_nat_le_of_nat H }, + { exfalso, exact not_neg_succ_le_of_nat H }}, + { apply minus_two_le } + end + + definition sub_nat_le (n : ℤ) (m : ℕ) : n - m ≤ n := + le.intro !sub_add_cancel + + definition sub_nat_lt (n : ℤ) (m : ℕ) : n - m < n + 1 := + add_le_add_right (sub_nat_le n m) 1 + + definition sub_one_le (n : ℤ) : n - 1 ≤ n := + sub_nat_le n 1 + + definition le_add_nat (n : ℤ) (m : ℕ) : n ≤ n + m := + le.intro rfl + + definition le_add_one (n : ℤ) : n ≤ n + 1:= + le_add_nat n 1 + + open trunc_index + + definition maxm2_le (n k : ℤ) : maxm2 (n+1+k) ≤ (maxm1m1 n).+1+2+(maxm1m1 k) := + begin + rewrite [-(maxm1_eq_succ n)], + induction n with n n, + { induction k with k k, + { induction k with k IH, + { apply le.tr_refl }, + { exact succ_le_succ IH } }, + { exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₁) + (maxm2_le_maxm1 n) } }, + { krewrite (add_plus_two_comm -1 (maxm1m1 k)), + rewrite [-(maxm1_eq_succ k)], + exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₂) + (maxm2_le_maxm1 k) } + end + +end int open int