From f013c631d0ea10bb6352cb4595e38959779a5ada Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 1 Mar 2017 22:58:50 -0500 Subject: [PATCH] Finish the naturality of the smash-pmap adjunction --- algebra/product_group.hlean | 1 + choice.hlean | 6 +- homotopy/cohomology.hlean | 72 +++++--- homotopy/fwedge.hlean | 7 +- homotopy/pushout.hlean | 4 +- homotopy/smash.hlean | 336 +++++++++++++++++++++++++++++------ homotopy/smash_adjoint.hlean | 13 +- move_to_lib.hlean | 181 +++++++++++++++++++ 8 files changed, 528 insertions(+), 92 deletions(-) diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean index a07cb61..c8f86bf 100644 --- a/algebra/product_group.hlean +++ b/algebra/product_group.hlean @@ -59,5 +59,6 @@ namespace group AbGroup.mk _ (ab_group_prod G G') infix ` ×g `:30 := group.product + infix ` ×ag `:30 := group.ab_product end group diff --git a/choice.hlean b/choice.hlean index b873345..c720f33 100644 --- a/choice.hlean +++ b/choice.hlean @@ -64,9 +64,9 @@ end definition has_choice_bool [instance] (n : ℕ₋₂) : has_choice n bool := has_choice_equiv_closed n bool_equiv_unit_sum_unit _ -definition has_choice_lift [instance] (n : ℕ₋₂) (A : Type) [has_choice n A] : - has_choice n (lift A) := -has_choice_equiv_closed n !equiv_lift⁻¹ᵉ _ +definition has_choice_lift.{u v} [instance] (n : ℕ₋₂) (A : Type) [has_choice n A] : + has_choice n (lift.{u v} A) := +sorry --has_choice_equiv_closed n !equiv_lift⁻¹ᵉ _ definition has_choice_punit [instance] (n : ℕ₋₂) : has_choice n punit := has_choice_unit n definition has_choice_pbool [instance] (n : ℕ₋₂) : has_choice n pbool := has_choice_bool n diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index 94d5691..a9a4806 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -6,36 +6,36 @@ Authors: Floris van Doorn Reduced cohomology of spectra and cohomology theories -/ -import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_lib +import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_lib ..algebra.product_group open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc - function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit + function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi -- TODO: move -structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) := +structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) := ( im_in_ker : Π(a:A), g (f a) = pt) ( ker_in_im : Π(b:B), (g b = pt) → image f b) -definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) := -is_exact f g +definition is_short_exact_g {A B C : Group} (f : A →g B) (g : B →g C) := +is_short_exact f g -definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C} - (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g := -is_exact.mk H₁ H₂ +definition is_short_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C} + (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_short_exact_g f g := +is_short_exact.mk H₁ H₂ -definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C} - (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) := +definition is_short_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C} + (H : is_short_exact_t f g) : @is_short_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) := begin constructor, { intro a, esimp, induction a with a, - exact ap tr (is_exact_t.im_in_ker H a) }, + exact ap tr (is_short_exact_t.im_in_ker H a) }, { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q, - induction is_exact_t.ker_in_im H b q with a r, + induction is_short_exact_t.ker_in_im H b q with a r, exact image.mk (tr a) (ap tr r) } end -definition is_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C} - (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' := +definition is_short_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C} + (p : f ~ f') (q : g ~ g') (H : is_short_exact f g) : is_short_exact f' g' := begin induction p using homotopy.rec_on_idp, induction q using homotopy.rec_on_idp, @@ -199,8 +199,8 @@ end /- exactness -/ definition cohomology_exact {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) : - is_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) := -is_exact_trunc_functor (cofiber_exact f) + is_short_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) := +is_short_exact_trunc_functor (cofiber_exact f) /- additivity -/ @@ -253,7 +253,7 @@ structure cohomology_theory.{u} : Type.{u+1} := (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X) (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y), Hsusp n X ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n Y) - (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f)) + (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_short_exact_g (Hh n (pcod f)) (Hh n f)) (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I → is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i))) @@ -264,6 +264,9 @@ attribute cohomology_theory.HH [coercion] postfix `^→`:90 := cohomology_theory.Hh open cohomology_theory +definition Hequiv (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X ≃* Y) : H n Y ≃ H n X := +equiv_of_isomorphism (Hiso H n f) + definition Hsusp_neg (H : cohomology_theory) (n : ℤ) (X : Type*) : H n (psusp X) ≃g H (pred n) X := isomorphism_of_eq (ap (λn, H n _) proof (sub_add_cancel n 1)⁻¹ qed) ⬝g cohomology_theory.Hsusp H (pred n) X @@ -279,23 +282,41 @@ definition Hsusp_neg_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} H ^→ n (psusp_functor f) ∘g (Hsusp_neg H n Y)⁻¹ᵍ ~ (Hsusp_neg H n X)⁻¹ᵍ ∘ H ^→ (pred n) f := sorry -definition Hadditive0 (H : cohomology_theory) (n : ℤ) : +definition Hadditive_equiv (H : cohomology_theory) (n : ℤ) {I : Type} (X : I → Type*) (H2 : has_choice 0 I) + : H n (⋁ X) ≃g Πᵍ i, H n (X i) := +isomorphism.mk _ (Hadditive H n X H2) + +definition Hlift_empty.{u} (H : cohomology_theory.{u}) (n : ℤ) : is_contr (H n (plift punit)) := let P : lift empty → Type* := lift.rec empty.elim in let x := Hadditive H n P _ in begin note z := equiv.mk _ x, refine @(is_trunc_equiv_closed_rev -2 (_ ⬝e z ⬝e _)) !is_contr_unit, - repeat exact sorry --- refine equiv_of_isomorphism (Hiso H n (_ ⬝e* _)), + refine Hequiv H n (pequiv_punit_of_is_contr _ _ ⬝e* !pequiv_plift), + apply is_contr_fwedge_of_neg, intro y, induction y with y, exact y, + apply equiv_unit_of_is_contr, apply is_contr_pi_of_neg, intro y, induction y with y, exact y end +definition Hempty (H : cohomology_theory.{0}) (n : ℤ) : + is_contr (H n punit) := +@(is_trunc_equiv_closed _ (Hequiv H n !pequiv_plift)) (Hlift_empty H n) + definition Hconst (H : cohomology_theory) (n : ℤ) {X Y : Type*} (y : H n Y) : H ^→ n (pconst X Y) y = 1 := begin - refine !one_mul⁻¹ ⬝ _, exact sorry + refine Hhomotopy H n (pconst_pcompose (pconst X (plift punit)))⁻¹* y ⬝ _, + refine Hcompose H n _ _ y ⬝ _, + refine ap (H ^→ n _) (@eq_of_is_contr _ (Hlift_empty H n) _ 1) ⬝ _, + apply respect_one end -definition cohomology_theory_spectrum [constructor] (Y : spectrum) : cohomology_theory := +-- definition Hwedge (H : cohomology_theory) (n : ℤ) (A B : Type*) : H n (A ∨ B) ≃g H n A ×ag H n B := +-- begin +-- refine Hiso H n (pwedge_pequiv_fwedge A B)⁻¹ᵉ* ⬝g _, +-- refine Hadditive_equiv H n _ _ ⬝g _ +-- end + +definition cohomology_theory_spectrum.{u} [constructor] (Y : spectrum.{u}) : cohomology_theory.{u} := cohomology_theory.mk (λn A, H^n[A, Y]) (λn A B f, cohomology_isomorphism f Y n) @@ -310,6 +331,13 @@ cohomology_theory.mk (λn A B f, cohomology_exact f Y n) (λn I A H, spectrum_additive H A Y n) +-- set_option pp.universes true +-- set_option pp.abbreviations false +-- print cohomology_theory_spectrum +-- print EM_spectrum +-- print has_choice_lift +-- print equiv_lift +-- print has_choice_equiv_closed definition ordinary_theory_EM [constructor] (G : AbGroup) : ordinary_theory := ⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄ diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean index 54864a5..9409062 100644 --- a/homotopy/fwedge.hlean +++ b/homotopy/fwedge.hlean @@ -86,11 +86,14 @@ namespace fwedge { exact glue ff } end - definition is_contr_fwedge_empty : is_contr (⋁(empty.rec _)) := + definition is_contr_fwedge_of_neg {I : Type} (P : I → Type*) (H : ¬ I) : is_contr (⋁P) := begin apply is_contr.mk pt, intro x, induction x, contradiction, reflexivity, contradiction end + definition is_contr_fwedge_empty [instance] : is_contr (⋁empty.elim) := + is_contr_fwedge_of_neg _ id + definition fwedge_pmap [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) : ⋁F →* X := begin fconstructor, @@ -132,6 +135,6 @@ namespace fwedge definition trunc_fwedge_pmap_equiv.{u} {n : ℕ₋₂} {I : Type.{u}} (H : has_choice n I) (F : I → pType.{u}) (X : pType.{u}) : trunc n (⋁F →* X) ≃ Πi, trunc n (F i →* X) := - trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv H (λi, F i →* X) + trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv (λi, F i →* X) end fwedge diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean index af83bc4..a30a4f5 100644 --- a/homotopy/pushout.hlean +++ b/homotopy/pushout.hlean @@ -464,7 +464,7 @@ namespace pushout /- universal property of cofiber -/ - structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := + structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := ( im_in_ker : Π(a:A), g (f a) = pt) ( ker_in_im : Π(b:B), (g b = pt) → fiber f b) @@ -491,7 +491,7 @@ namespace pushout end definition cofiber_exact {X Y Z : Type*} (f : X →* Y) : - is_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) := + is_short_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) := begin constructor, { intro g, apply eq_of_phomotopy, apply cofiber_exact_1 }, diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 52c651d..fee624e 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -9,14 +9,51 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/ - /- To prove: associative, A ∧ S¹ ≃ ΣA -/ + /- To prove: A ∧ S¹ ≃ ΣA -/ + /- associativity is mostly proven in smash_adjoint, the only hole in the proof is in this file -/ variables {A B C D E F : Type*} namespace smash open pushout + protected definition rec_eq {A B : Type*} {C : Type} {f g : smash A B → C} + (Pmk : Πa b, f (smash.mk a b) = g (smash.mk a b)) + (Pl : f auxl = g auxl) (Pr : f auxr = g auxr) + (Pgl : Πa, square (Pmk a pt) Pl (ap f (gluel a)) (ap g (gluel a))) + (Pgr : Πb, square (Pmk pt b) Pr (ap f (gluer b)) (ap g (gluer b))) (x : smash' A B) : f x = g x := + begin + induction x with a b a b, + { exact Pmk a b }, + { exact Pl }, + { exact Pr }, + { apply eq_pathover, apply Pgl }, + { apply eq_pathover, apply Pgr } + end + + definition rec_eq_gluel {A B : Type*} {C : Type} {f g : smash A B → C} + {Pmk : Πa b, f (smash.mk a b) = g (smash.mk a b)} + {Pl : f auxl = g auxl} {Pr : f auxr = g auxr} + (Pgl : Πa, square (Pmk a pt) Pl (ap f (gluel a)) (ap g (gluel a))) + (Pgr : Πb, square (Pmk pt b) Pr (ap f (gluer b)) (ap g (gluer b))) (a : A) : + natural_square (smash.rec_eq Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a := + begin + refine ap square_of_pathover !rec_gluel ⬝ _, + apply to_right_inv !eq_pathover_equiv_square + end + + definition rec_eq_gluer {A B : Type*} {C : Type} {f g : smash A B → C} + {Pmk : Πa b, f (smash.mk a b) = g (smash.mk a b)} + {Pl : f auxl = g auxl} {Pr : f auxr = g auxr} + (Pgl : Πa, square (Pmk a pt) Pl (ap f (gluel a)) (ap g (gluel a))) + (Pgr : Πb, square (Pmk pt b) Pr (ap f (gluer b)) (ap g (gluer b))) (b : B) : + natural_square (smash.rec_eq Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b := + begin + refine ap square_of_pathover !rec_gluer ⬝ _, + apply to_right_inv !eq_pathover_equiv_square + end + definition smash_functor' [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D := begin fapply pushout.functor, @@ -50,6 +87,18 @@ namespace smash induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity end + definition functor_gluel2 {C D : Type} (f : A → C) (g : B → D) (a : A) : + ap (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (gluel a) = gluel (f a) := + begin + refine !pushout.elim_glue ⬝ !idp_con + end + + definition functor_gluer2 {C D : Type} (f : A → C) (g : B → D) (b : B) : + ap (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (gluer b) = gluer (g b) := + begin + refine !pushout.elim_glue ⬝ !idp_con + end + definition functor_gluel' (f : A →* C) (g : B →* D) (a a' : A) : ap (smash_functor f g) (gluel' a a') = ap (smash.mk (f a)) (respect_pt g) ⬝ gluel' (f a) (f a') ⬝ (ap (smash.mk (f a')) (respect_pt g))⁻¹ := @@ -73,23 +122,31 @@ namespace smash /- the statements of the above rules becomes easier if one of the functions respects the basepoint by reflexivity -/ - definition functor_gluel'2 {D : Type} (f : A →* C) (g : B → D) (a a' : A) : - ap (smash_functor f (pmap_of_map g pt)) (gluel' a a') = gluel' (f a) (f a') := - begin - refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _, - refine (!functor_gluel ⬝ !idp_con) ◾ (!functor_gluel ⬝ !idp_con)⁻² - end + -- definition functor_gluel'2 {D : Type} (f : A →* C) (g : B → D) (a a' : A) : + -- ap (smash_functor f (pmap_of_map g pt)) (gluel' a a') = gluel' (f a) (f a') := + -- begin + -- refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _, + -- refine (!functor_gluel ⬝ !idp_con) ◾ (!functor_gluel ⬝ !idp_con)⁻² + -- end - definition functor_gluer'2 {C : Type} (f : A → C) (g : B →* D) (b b' : B) : - ap (smash_functor (pmap_of_map f pt) g) (gluer' b b') = gluer' (g b) (g b') := - begin - refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _, - refine (!functor_gluer ⬝ !idp_con) ◾ (!functor_gluer ⬝ !idp_con)⁻² - end + -- definition functor_gluer'2 {C : Type} (f : A → C) (g : B →* D) (b b' : B) : + -- ap (smash_functor (pmap_of_map f pt) g) (gluer' b b') = gluer' (g b) (g b') := + -- begin + -- refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _, + -- refine (!functor_gluer ⬝ !idp_con) ◾ (!functor_gluer ⬝ !idp_con)⁻² + -- end - lemma functor_gluel'2_same {D : Type} (f : A →* C) (g : B → D) (a : A) : + definition functor_gluel'2 {C D : Type} (f : A → C) (g : B → D) (a a' : A) : + ap (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (gluel' a a') = gluel' (f a) (f a') := + !ap_con ⬝ whisker_left _ !ap_inv ⬝ !functor_gluel2 ◾ !functor_gluel2⁻² + + definition functor_gluer'2 {C D : Type} (f : A → C) (g : B → D) (b b' : B) : + ap (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (gluer' b b') = gluer' (g b) (g b') := + !ap_con ⬝ whisker_left _ !ap_inv ⬝ !functor_gluer2 ◾ !functor_gluer2⁻² + + lemma functor_gluel'2_same {C D : Type} (f : A → C) (g : B → D) (a : A) : functor_gluel'2 f (pmap_of_map g pt) a a = - ap02 (smash_functor f (pmap_of_map g pt)) (con.right_inv (gluel a)) ⬝ + ap02 (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (con.right_inv (gluel a)) ⬝ (con.right_inv (gluel (f a)))⁻¹ := begin refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹, @@ -100,9 +157,9 @@ namespace smash apply con_right_inv_natural end - lemma functor_gluer'2_same {C : Type} (f : A → C) (g : B →* D) (b : B) : + lemma functor_gluer'2_same {C D : Type} (f : A → C) (g : B → D) (b : B) : functor_gluer'2 (pmap_of_map f pt) g b b = - ap02 (smash_functor (pmap_of_map f pt) g) (con.right_inv (gluer b)) ⬝ + ap02 (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (con.right_inv (gluer b)) ⬝ (con.right_inv (gluer (g b)))⁻¹ := begin refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹, @@ -113,56 +170,108 @@ namespace smash apply con_right_inv_natural end - definition smash_functor_pcompose_homotopy (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) : - smash_functor (f' ∘* f) (g' ∘* g) ~ smash_functor f' g' ∘* smash_functor f g := + -- definition smash_functor_pcompose_homotopy [unfold 11] (f' : C →* E) (f : A →* C) (g' : D →* F) + -- (g : B →* D) : smash_functor (f' ∘* f) (g' ∘* g) ~ smash_functor f' g' ∘* smash_functor f g := + -- begin + -- intro x, induction x with a b a b, + -- { reflexivity }, + -- { reflexivity }, + -- { reflexivity }, + -- { apply eq_pathover, exact abstract begin apply hdeg_square, + -- refine !functor_gluel ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹, + -- refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluel⁻¹, + -- refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluel⁻¹ qed ⬝ !ap_con⁻¹ end end }, + -- { apply eq_pathover, exact abstract begin apply hdeg_square, + -- refine !functor_gluer ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹, + -- refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluer⁻¹, + -- refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluer⁻¹ qed ⬝ !ap_con⁻¹ end end } + -- end + + -- definition smash_functor_pcompose [constructor] (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) : + -- smash_functor (f' ∘* f) (g' ∘* g) ~* smash_functor f' g' ∘* smash_functor f g := + -- begin + -- fapply phomotopy.mk, + -- { exact smash_functor_pcompose_homotopy f' f g' g }, + -- { exact abstract begin induction C, induction D, induction E, induction F, + -- induction f with f f₀, induction f' with f' f'₀, induction g with g g₀, + -- induction g' with g' g'₀, esimp at *, + -- induction f₀, induction f'₀, induction g₀, induction g'₀, reflexivity end end } + -- end + + definition smash_functor_pcompose_homotopy [unfold 11] {C D E F : Type} + (f' : C → E) (f : A → C) (g' : D → F) (g : B → D) : + smash_functor (pmap_of_map f' (f pt) ∘* pmap_of_map f pt) + (pmap_of_map g' (g pt) ∘* pmap_of_map g pt) ~ + smash_functor (pmap_of_map f' (f pt)) (pmap_of_map g' (g pt)) ∘* + smash_functor (pmap_of_map f pt) (pmap_of_map g pt) := begin intro x, induction x with a b a b, { reflexivity }, { reflexivity }, { reflexivity }, - { apply eq_pathover, apply hdeg_square, - refine !functor_gluel ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹, - refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluel⁻¹, - refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluel⁻¹ qed ⬝ !ap_con⁻¹, }, - { apply eq_pathover, apply hdeg_square, - refine !functor_gluer ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹, - refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluer⁻¹, - refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluer⁻¹ qed ⬝ !ap_con⁻¹, } + { apply eq_pathover, refine !functor_gluel2 ⬝ph _, esimp, + refine _ ⬝hp (ap_compose (smash_functor _ _) _ _)⁻¹, + refine _ ⬝hp ap02 _ !functor_gluel2⁻¹, refine _ ⬝hp !functor_gluel2⁻¹, exact hrfl }, + { apply eq_pathover, refine !functor_gluer2 ⬝ph _, esimp, + refine _ ⬝hp (ap_compose (smash_functor _ _) _ _)⁻¹, + refine _ ⬝hp ap02 _ !functor_gluer2⁻¹, refine _ ⬝hp !functor_gluer2⁻¹, exact hrfl } end - definition smash_functor_pcompose [constructor] (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) : + definition smash_functor_pcompose (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) : smash_functor (f' ∘* f) (g' ∘* g) ~* smash_functor f' g' ∘* smash_functor f g := begin + induction C with C, induction D with D, induction E with E, induction F with F, + induction f with f f₀, induction f' with f' f'₀, induction g with g g₀, + induction g' with g' g'₀, esimp at *, + induction f₀, induction f'₀, induction g₀, induction g'₀, fapply phomotopy.mk, - { exact smash_functor_pcompose_homotopy f' f g' g }, - { exact abstract begin induction C, induction D, induction E, induction F, - induction f with f f₀, induction f' with f' f'₀, induction g with g g₀, induction g' with g' g'₀, - esimp at *, induction f₀, induction f'₀, induction g₀, induction g'₀, reflexivity end end } + { rexact smash_functor_pcompose_homotopy f' f g' g }, + { reflexivity } end + -- definition smash_functor_homotopy [unfold 11] {f f' : A →* C} {g g' : B →* D} + -- (h₁ : f ~* f') (h₂ : g ~* g') : smash_functor f g ~ smash_functor f' g' := + -- begin + -- intro x, induction x with a b a b, + -- { exact ap011 smash.mk (h₁ a) (h₂ b) }, + -- { reflexivity }, + -- { reflexivity }, + -- { apply eq_pathover, + -- refine !functor_gluel ⬝ph _ ⬝hp !functor_gluel⁻¹, + -- refine _ ⬝v square_of_eq_top (ap_mk_left (h₁ a)), + -- exact ap011_ap_square_right smash.mk (h₁ a) (to_homotopy_pt h₂) }, + -- { apply eq_pathover, + -- refine !functor_gluer ⬝ph _ ⬝hp !functor_gluer⁻¹, + -- refine _ ⬝v square_of_eq_top (ap_mk_right (h₂ b)), + -- exact ap011_ap_square_left smash.mk (h₂ b) (to_homotopy_pt h₁) }, + -- end + + -- definition smash_functor_phomotopy [constructor] {f f' : A →* C} {g g' : B →* D} + -- (h₁ : f ~* f') (h₂ : g ~* g') : smash_functor f g ~* smash_functor f' g' := + -- begin + -- apply phomotopy.mk (smash_functor_homotopy h₁ h₂), + -- induction h₁ with h₁ h₁₀, induction h₂ with h₂ h₂₀, + -- induction f with f f₀, induction g with g g₀, + -- induction f' with f' f'₀, induction g' with g' g'₀, + -- induction C with C c₀, induction D with D d₀, esimp at *, + -- induction h₁₀, induction h₂₀, induction f'₀, induction g'₀, + -- exact !ap_ap011⁻¹ + -- end + definition smash_functor_phomotopy [constructor] {f f' : A →* C} {g g' : B →* D} (h₁ : f ~* f') (h₂ : g ~* g') : smash_functor f g ~* smash_functor f' g' := begin induction h₁ using phomotopy_rec_on_idp, induction h₂ using phomotopy_rec_on_idp, reflexivity - -- fapply phomotopy.mk, - -- { intro x, induction x with a b a b, - -- { exact ap011 smash.mk (h₁ a) (h₂ b) }, - -- { reflexivity }, - -- { reflexivity }, - -- { apply eq_pathover, - -- refine !functor_gluel ⬝ph _ ⬝hp !functor_gluel⁻¹, exact sorry }, - -- { apply eq_pathover, - -- refine !functor_gluer ⬝ph _ ⬝hp !functor_gluer⁻¹, exact sorry }}, - -- { esimp, } end definition smash_functor_phomotopy_refl [constructor] (f : A →* C) (g : B →* D) : smash_functor_phomotopy (phomotopy.refl f) (phomotopy.refl g) = phomotopy.rfl := !phomotopy_rec_on_idp_refl ⬝ !phomotopy_rec_on_idp_refl - definition smash_functor_pid [constructor] (A B : Type*) : smash_functor (pid A) (pid B) ~* pid (A ∧ B) := + definition smash_functor_pid [constructor] (A B : Type*) : + smash_functor (pid A) (pid B) ~* pid (A ∧ B) := begin fapply phomotopy.mk, { intro x, induction x with a b a b, @@ -182,26 +291,133 @@ namespace smash : smash_functor (f' ∘* f) (pid B) ~* smash_functor f' (pid B) ∘* smash_functor f (pid B) := smash_functor_phomotopy phomotopy.rfl !pid_pcompose⁻¹* ⬝* !smash_functor_pcompose - definition smash_functor_pconst_right_homotopy [unfold 6] (f : A →* C) (x : A ∧ B) : - smash_functor f (pconst B D) x = pt := + -- definition smash_functor_pconst_right_homotopy [unfold 6] (f : A →* C) (x : A ∧ B) : + -- smash_functor f (pconst B D) x = pt := + -- begin + -- induction x with a b a b, + -- { exact gluel' (f a) pt }, + -- { exact (gluel pt)⁻¹ }, + -- { exact (gluer pt)⁻¹ }, + -- { apply eq_pathover, refine !functor_gluel ⬝ !idp_con ⬝ph _ ⬝hp !ap_constant⁻¹, + -- apply square_of_eq, reflexivity }, + -- { apply eq_pathover, refine !functor_gluer ⬝ph _ ⬝hp !ap_constant⁻¹, + -- apply whisker_lb, apply square_of_eq, exact !ap_mk_left⁻¹ } + -- end + + -- definition smash_functor_pconst_right [constructor] (f : A →* C) : + -- smash_functor f (pconst B D) ~* pconst (A ∧ B) (C ∧ D) := + -- begin + -- fapply phomotopy.mk, + -- { exact smash_functor_pconst_right_homotopy f }, + -- { refine (ap_mk_left (respect_pt f))⁻¹ ⬝ _, + -- induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity } + -- end + +-- set_option pp.all true + definition smash_functor_pconst_right_homotopy [unfold 6] {C : Type} (f : A → C) (x : A ∧ B) : + smash_functor (pmap_of_map f pt) (pconst B D) x = pt := begin induction x with a b a b, { exact gluel' (f a) pt }, { exact (gluel pt)⁻¹ }, { exact (gluer pt)⁻¹ }, - { apply eq_pathover_constant_right, refine !functor_gluel ⬝ !idp_con ⬝ph _, - apply square_of_eq, reflexivity }, - { apply eq_pathover_constant_right, refine !functor_gluer ⬝ph _, - apply whisker_lb, apply square_of_eq, exact !ap_mk_left⁻¹ } + { apply eq_pathover, note x := functor_gluel2 f (λx : B, Point D) a, esimp [pconst] at *, + refine x ⬝ph _, refine _ ⬝hp !ap_constant⁻¹, apply square_of_eq, reflexivity }, + { apply eq_pathover, note x := functor_gluer2 f (λx : B, Point D) b, esimp [pconst] at *, + refine x ⬝ph _, refine _ ⬝hp !ap_constant⁻¹, apply square_of_eq, + rexact con.right_inv (gluel (f pt)) ⬝ (con.right_inv (gluer pt))⁻¹ } end - definition smash_functor_pconst_right [constructor] (f : A →* C) : + definition smash_functor_pconst_right (f : A →* C) : smash_functor f (pconst B D) ~* pconst (A ∧ B) (C ∧ D) := begin + induction C with C, induction f with f f₀, esimp at *, induction f₀, fapply phomotopy.mk, { exact smash_functor_pconst_right_homotopy f }, - { refine (ap_mk_left (respect_pt f))⁻¹ ⬝ _, - induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity } + { rexact con.right_inv (gluel (f pt)) } + end + + -- example {X : Type*} {A B : Type} {a : A} (f : A → B) : + -- pmap_of_map f a ∘* pconst X _ = pconst X _ := + -- idp + + -- example {X : Type*} {A B : Type} {a : A} (f : A → B) : + -- @pcompose_pconst X _ _ (pmap_of_map f a) = sorry := + -- begin unfold [pcompose_pconst] end + + + /- we need a coherence rule for smash_functor_pconst_right for the naturality of the + smash-pmap adjunction -/ + private definition my_squarel {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₂ = a₃) : + square (p₁ ⬝ p₂⁻¹) p₂⁻¹ p₁ idp := + proof square_of_eq idp qed + + private definition my_squarer {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₁ = a₂) : + square (p₁ ⬝ p₁⁻¹) p₂⁻¹ p₂ idp := + proof square_of_eq (con.right_inv p₁ ⬝ (con.right_inv p₂)⁻¹) qed + + private definition my_cube_fillerl {A B C : Type} {g : B → C} {f : A → B} {a₁ a₂ : A} {b₀ : B} + {p : f ~ λa, b₀} {q : Πa, g (f a) = g b₀} (r : (λa, ap g (p a)) ~ q) : + cube (hrfl ⬝hp (r a₁)⁻¹) hrfl + (my_squarel (q a₁) (q a₂)) (aps g (my_squarel (p a₁) (p a₂))) + (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (r a₁) ◾ (r a₂)⁻²)⁻¹) + (hrfl ⬝hp (r a₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) := + begin + induction r using homotopy.rec_on_idp, + induction p using homotopy.rec_on_idp_left, + exact idc + end + + private definition my_cube_fillerr {B C : Type} {g : B → C} {b₀ bl br : B} + {pl : b₀ = bl} {pr : b₀ = br} {ql : g b₀ = g bl} {qr : g b₀ = g br} + (sl : ap g pl = ql) (sr : ap g pr = qr) : + cube (hrfl ⬝hp sr⁻¹) hrfl + (my_squarer ql qr) (aps g (my_squarer pl pr)) + (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ sl ◾ sl⁻²)⁻¹) + (hrfl ⬝hp sr⁻²⁻¹ ⬝hp !ap_inv⁻¹) := + begin + induction sr, + induction sl, + induction pr, + induction pl, + exact idc + end + + definition smash_functor_pconst_right_pcompose_homotopy {A B C D E F : Type} + (a₀ : A) (b₀ : B) (d₀ : D) (f' : C → E) (f : A → C) (g : D → F) + (x : pointed.MK A a₀ ∧ pointed.MK B b₀) : + square (smash_functor_pcompose_homotopy f' f g (λ a, d₀) x) + idp + (smash_functor_pconst_right_homotopy (λ a, f' (f a)) x) + (ap (smash_functor' (pmap.mk f' (refl (f' (f a₀)))) (pmap.mk g (refl (g d₀)))) + (smash_functor_pconst_right_homotopy f x)) := + begin + induction x with a b a b, + { refine _ ⬝hp (functor_gluel'2 f' g (f a) (f a₀))⁻¹, exact hrfl }, + { refine _ ⬝hp !ap_inv⁻¹, refine _ ⬝hp !functor_gluel2⁻²⁻¹, exact hrfl }, + { refine _ ⬝hp !ap_inv⁻¹, refine _ ⬝hp !functor_gluer2⁻²⁻¹, exact hrfl }, + { exact abstract begin apply square_pathover, + refine !rec_eq_gluel ⬝p1 _ ⬝1p !natural_square_refl⁻¹, + refine !rec_eq_gluel ⬝p2 _ ⬝2p !natural_square_ap_fn⁻¹, + apply whisker001, apply whisker021, + apply move201, refine _ ⬝1p !eq_hconcat_hdeg_square⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine ap (hconcat_eq _) !ap_inv ⬝p1 _ ⬝2p (ap (aps _) !rec_eq_gluel ⬝ !aps_eq_hconcat)⁻¹, + apply whisker021, refine _ ⬝2p !aps_hconcat_eq⁻¹, apply move221, + refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_ap_constant)), + apply my_cube_fillerl end end }, + { exact abstract begin apply square_pathover, + refine !rec_eq_gluer ⬝p1 _ ⬝1p !natural_square_refl⁻¹, + refine !rec_eq_gluer ⬝p2 _ ⬝2p !natural_square_ap_fn⁻¹, + apply whisker001, apply whisker021, + apply move201, refine _ ⬝1p !eq_hconcat_hdeg_square⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine ap (hconcat_eq _) !ap_inv ⬝p1 _ ⬝2p (ap (aps _) !rec_eq_gluer ⬝ !aps_eq_hconcat)⁻¹, + apply whisker021, refine _ ⬝2p !aps_hconcat_eq⁻¹, apply move221, + refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_ap_constant)), esimp, + apply my_cube_fillerr end end } end definition smash_functor_pconst_right_pcompose (f' : C →* E) (f : A →* C) (g : D →* F) : @@ -211,7 +427,21 @@ namespace smash (pwhisker_left (smash_functor f' g) (smash_functor_pconst_right f) ⬝* pcompose_pconst (smash_functor f' g)) := begin - exact sorry + induction A with A a₀, induction B with B b₀, + induction E with E e₀, induction C with C c₀, induction F with F x₀, induction D with D d₀, + induction f' with f' f'₀, induction f with f f₀, induction g with g g₀, + esimp at *, induction f'₀, induction f₀, induction g₀, + refine !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, + fapply phomotopy_eq, + { intro x, refine eq_of_square _ ⬝ !con_idp, + exact smash_functor_pconst_right_pcompose_homotopy a₀ b₀ d₀ f' f g x, }, + { refine _ ⬝ !idp_con⁻¹, + refine whisker_right _ (!whisker_right_idp ⬝ !eq_of_square_hrfl_hconcat_eq) ⬝ _, + refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con, esimp, + refine whisker_right _ !functor_gluel'2_same ⬝ _, + refine !inv_con_cancel_right ⬝ _, + refine _ ⬝ idp ◾ ap (whisker_left _) (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹, + symmetry, apply whisker_left_idp } end definition smash_functor_pconst_right_pid_pcompose (g : D →* F) : diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index b3fceea..da2c596 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -48,12 +48,6 @@ namespace smash { apply eq_of_phomotopy, exact smash_pmap_unit_pt A B } end - definition smash_functor_pid_gluer' (A : Type*) {B C : Type*} (b : B) (f : B →* C) : - ap (smash_functor (pid A) f) (gluer' b pt) = gluer' (f b) (f pt) := - begin - rexact functor_gluer'2 (@id A) f b pt - end - definition smash_functor_pid_pinl' [constructor] {A B C : Type*} (b : B) (f : B →* C) : pinl A (f b) ~* smash_functor (pid A) f ∘* pinl A b := begin @@ -61,7 +55,7 @@ namespace smash { intro a, reflexivity }, { refine !idp_con ⬝ _, induction C with C c₀, induction f with f f₀, esimp at *, - induction f₀, rexact smash_functor_pid_gluer' A b (pmap_of_map f pt) } + induction f₀, rexact functor_gluer'2 (@id A) f b pt } end definition smash_pmap_unit_pt_natural [constructor] (f : B →* C) : @@ -79,7 +73,6 @@ namespace smash { refine whisker_right_idp _ ⬝ph _, refine ap (λx, _ ⬝ x) _ ⬝ph _, rotate 1, rexact (functor_gluel'2_same (pid A) f pt), - -- refine whisker_left _ (!con.assoc ⬝ whisker_left _ !con.left_inv ⬝ !con_idp) ⬝ph _, refine whisker_right _ !idp_con ⬝pv _, refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, refine !con.assoc⁻¹ ⬝ whisker_right _ _ ⬝pv _, @@ -91,7 +84,6 @@ namespace smash apply whisker_tl, apply vdeg_square, refine whisker_right _ !ap_inv ⬝ _, apply inv_con_eq_of_eq_con, - unfold [smash_functor_pid_gluer'], rexact functor_gluer'2_same (pmap_of_map id (Point A)) (pmap_of_map f pt) pt } end @@ -481,5 +473,6 @@ namespace smash apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_equiv } end -print axioms smash_assoc + print axioms smash_assoc + end smash diff --git a/move_to_lib.hlean b/move_to_lib.hlean index efb8931..4ae0e6f 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -26,6 +26,145 @@ end algebra namespace eq +section -- squares + variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A} + /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ + {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} + /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ + {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} + /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/ + + variables {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁} + {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃} + + definition natural_square_eq {A B : Type} {a a' : A} {f g : A → B} (p : f ~ g) (q : a = a') + : natural_square p q = square_of_pathover (apd p q) := + idp + + definition eq_of_square_hrfl_hconcat_eq {A : Type} {a a' : A} {p p' : a = a'} (q : p = p') + : eq_of_square (hrfl ⬝hp q⁻¹) = !idp_con ⬝ q := + by induction q; induction p; reflexivity + + definition aps_vrfl {A B : Type} {a a' : A} (f : A → B) (p : a = a') : + aps f (vrefl p) = vrefl (ap f p) := + by induction p; reflexivity + + definition aps_hrfl {A B : Type} {a a' : A} (f : A → B) (p : a = a') : + aps f (hrefl p) = hrefl (ap f p) := + by induction p; reflexivity + + definition natural_square_ap_fn {A B C : Type} {a a' : A} {g h : A → B} (f : B → C) (p : g ~ h) (q : a = a') : + natural_square (λa, ap f (p a)) q = + ap_compose f g q ⬝ph (aps f (natural_square p q) ⬝hp (ap_compose f h q)⁻¹) := + begin + induction q, exact !aps_vrfl⁻¹ + end + + definition natural_square_refl {A B : Type} {a a' : A} (f : A → B) (q : a = a') + : natural_square (homotopy.refl f) q = hrfl := + by induction q; reflexivity + + definition aps_eq_hconcat {p₀₁'} (f : A → B) (q : p₀₁' = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : + aps f (q ⬝ph s₁₁) = ap02 f q ⬝ph aps f s₁₁ := + by induction q; reflexivity + + definition aps_hconcat_eq {p₂₁'} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁' = p₂₁) : + aps f (s₁₁ ⬝hp r⁻¹) = aps f s₁₁ ⬝hp (ap02 f r)⁻¹ := + by induction r; reflexivity + + definition aps_hconcat_eq' {p₂₁'} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p₂₁') : + aps f (s₁₁ ⬝hp r) = aps f s₁₁ ⬝hp ap02 f r := + by induction r; reflexivity + + definition aps_square_of_eq (f : A → B) (s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : + aps f (square_of_eq s) = square_of_eq ((ap_con f p₁₀ p₂₁)⁻¹ ⬝ ap02 f s ⬝ ap_con f p₀₁ p₁₂) := + by induction p₁₂; esimp at *; induction s; induction p₂₁; induction p₁₀; reflexivity + + definition aps_eq_hconcat_eq {p₀₁' p₂₁'} (f : A → B) (q : p₀₁' = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + (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 + +end + +infix ` ⬝p2 `:75 := eq_concat2 +section -- cubes + + variables {A B : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ a a' : A} + {p₁₀₀ : a₀₀₀ = a₂₀₀} {p₀₁₀ : a₀₀₀ = a₀₂₀} {p₀₀₁ : a₀₀₀ = a₀₀₂} + {p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂} + {p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂} + {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂} + {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} + {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁} + {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₂ b₃ b₄ : B} + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) + + definition whisker001 {p₀₀₁' : a₀₀₀ = a₀₀₂} (q : p₀₀₁' = p₀₀₁) + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube (q ⬝ph s₀₁₁) s₂₁₁ (q ⬝ph s₁₀₁) s₁₂₁ s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker021 {p₀₂₁' : a₀₂₀ = a₀₂₂} (q : p₀₂₁' = p₀₂₁) + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube (s₀₁₁ ⬝hp q⁻¹) s₂₁₁ s₁₀₁ (q ⬝ph s₁₂₁) s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker021' {p₀₂₁' : a₀₂₀ = a₀₂₂} (q : p₀₂₁ = p₀₂₁') + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube (s₀₁₁ ⬝hp q) s₂₁₁ s₁₀₁ (q⁻¹ ⬝ph s₁₂₁) s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker201 {p₂₀₁' : a₂₀₀ = a₂₀₂} (q : p₂₀₁' = p₂₀₁) + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube s₀₁₁ (q ⬝ph s₂₁₁) (s₁₀₁ ⬝hp q⁻¹) s₁₂₁ s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker201' {p₂₀₁' : a₂₀₀ = a₂₀₂} (q : p₂₀₁ = p₂₀₁') + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube s₀₁₁ (q⁻¹ ⬝ph s₂₁₁) (s₁₀₁ ⬝hp q) s₁₂₁ s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker221 {p₂₂₁' : a₂₂₀ = a₂₂₂} (q : p₂₂₁ = p₂₂₁') + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ (s₂₁₁ ⬝hp q) s₁₀₁ (s₁₂₁ ⬝hp q) s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition move221 {p₂₂₁' : a₂₂₀ = a₂₂₂} {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁'} (q : p₂₂₁ = p₂₂₁') + (c : cube s₀₁₁ (s₂₁₁ ⬝hp q) s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube s₀₁₁ s₂₁₁ s₁₀₁ (s₁₂₁ ⬝hp q⁻¹) s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition move201 {p₂₀₁' : a₂₀₀ = a₂₀₂} {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁'} (q : p₂₀₁' = p₂₀₁) + (c : cube s₀₁₁ (q ⬝ph s₂₁₁) s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube s₀₁₁ s₂₁₁ (s₁₀₁ ⬝hp q) s₁₂₁ s₁₁₀ s₁₁₂ := + by induction q; exact c + +end + + + definition apo011 {A : Type} {B C D : A → Type} {a a' : A} {p : a = a'} {b : B a} {b' : B a'} + {c : C a} {c' : C a'} (f : Π⦃a⦄, B a → C a → D a) (q : b =[p] b') (r : c =[p] c') : + f b c =[p] f b' c' := + begin induction q, induction r using idp_rec_on, exact idpo end + + definition ap011_ap_square_right {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') + {b₁ b₂ b₃ : B} {q₁₂ : b₁ = b₂} {q₂₃ : b₂ = b₃} {q₁₃ : b₁ = b₃} (r : q₁₂ ⬝ q₂₃ = q₁₃) : + square (ap011 f p q₁₂) (ap (λx, f x b₃) p) (ap (f a) q₁₃) (ap (f a') q₂₃) := + by induction r; induction q₂₃; induction q₁₂; induction p; exact ids + + definition ap011_ap_square_left {A B C : Type} (f : B → A → C) {a a' : A} (p : a = a') + {b₁ b₂ b₃ : B} {q₁₂ : b₁ = b₂} {q₂₃ : b₂ = b₃} {q₁₃ : b₁ = b₃} (r : q₁₂ ⬝ q₂₃ = q₁₃) : + square (ap011 f q₁₂ p) (ap (f b₃) p) (ap (λx, f x a) q₁₃) (ap (λx, f x a') q₂₃) := + by induction r; induction q₂₃; induction q₁₂; induction p; exact ids + + definition ap_ap011 {A B C D : Type} (g : C → D) (f : A → B → C) {a a' : A} {b b' : B} + (p : a = a') (q : b = b') : ap g (ap011 f p q) = ap011 (λa b, g (f a b)) p q := + begin + induction p, exact (ap_compose g (f a) q)⁻¹ + end + definition con2_assoc {A : Type} {x y z t : A} {p p' : x = y} {q q' : y = z} {r r' : z = t} (h : p = p') (h' : q = q') (h'' : r = r') : square ((h ◾ h') ◾ h'') (h ◾ (h' ◾ h'')) (con.assoc p q r) (con.assoc p' q' r') := @@ -144,6 +283,18 @@ namespace eq postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse end hsquare + -- move to init.funext + protected definition homotopy.rec_on_idp_left [recursor] {A : Type} {P : A → Type} {g : Πa, P a} + {Q : Πf, (f ~ g) → Type} {f : Π x, P x} + (p : f ~ g) (H : Q g (homotopy.refl g)) : Q f p := + begin + induction p using homotopy.rec_on, induction q, exact H + end + + --eq2 + definition ap02_ap_constant {A B C : Type} {a a' : A} (f : B → C) (b : B) (p : a = a') : + square (ap_constant p (f b)) (ap02 f (ap_constant p b)) (ap_compose f (λx, b) p) idp := + by induction p; exact ids end eq open eq @@ -154,14 +305,44 @@ namespace wedge end wedge +namespace pi + + definition is_contr_pi_of_neg {A : Type} (B : A → Type) (H : ¬ A) : is_contr (Πa, B a) := + begin + apply is_contr.mk (λa, empty.elim (H a)), intro f, apply eq_of_homotopy, intro x, contradiction + end +end pi + namespace pointed + -- FALSE + -- definition phomotopy_pconst {A B : Type*} {f : A →* B} (p q : f ~* pconst A B) : p = q := + -- begin + -- induction f with f f₀, + -- induction p with p p₀, induction q with q q₀, + -- esimp at *, induction q₀, + -- end + + definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A := + begin + fapply phomotopy.mk, + { intro u, induction u, exact respect_pt f }, + { reflexivity } + end + + definition is_contr_punit_pmap (A : Type*) : is_contr (punit →* A) := + is_contr.mk (pconst punit A) (λf, eq_of_phomotopy (punit_pmap_phomotopy f)⁻¹*) + definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) : phomotopy_of_eq idp = phomotopy.refl f := idp definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f := λx, idp + definition pr1_phomotopy_eq {A B : Type*} {f g : A →* B} {p q : f ~* g} (r : p = q) (a : A) : + p a = q a := + ap010 to_homotopy r a + -- replace pcompose2 with this definition pcompose2' {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (q : g ~* g') (p : f ~* f') : g ∘* f ~* g' ∘* f' :=