From 47532e431553d3d5c1db7df986b8dcf2856cb131 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 6 Mar 2017 01:01:36 -0500 Subject: [PATCH] Prove the naturality of the smash-pmap adjunction, and hence of the associativity of the smash product --- algebra/arrow_group.hlean | 2 +- homotopy/EM.hlean | 8 +- homotopy/cohomology.hlean | 30 +- homotopy/pushout.hlean | 4 +- homotopy/smash.hlean | 1371 +++++++++++++++++----------------- homotopy/smash_adjoint.hlean | 226 ++++-- homotopy/spectrum.hlean | 2 +- homotopy/temp2.hlean | 123 +++ move_to_lib.hlean | 603 ++------------- pointed.hlean | 828 ++++++++++++++++++++ pointed_pi.hlean | 4 +- 11 files changed, 1876 insertions(+), 1325 deletions(-) create mode 100644 homotopy/temp2.hlean create mode 100644 pointed.hlean diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index 6a8b5e6..e73784a 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -1,4 +1,4 @@ -import algebra.group_theory ..move_to_lib eq2 +import algebra.group_theory ..pointed eq2 open pi pointed algebra group eq equiv is_trunc trunc namespace group diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 0161ab0..766e73b 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -1,6 +1,6 @@ -- Authors: Floris van Doorn -import homotopy.EM ..move_to_lib algebra.category.functor.equivalence ..pointed_pi +import homotopy.EM algebra.category.functor.equivalence ..pointed ..pointed_pi open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn @@ -233,7 +233,7 @@ namespace EM begin assert p' : ptrunc_functor 0 (Ω→ f) ∘* pequiv_of_isomorphism eX ~* pequiv_of_isomorphism eY ∘* pmap_of_homomorphism φ, exact phomotopy_of_homotopy p, - exact phcompose p' (ptrunc_pequiv_natural 0 (Ω→ f)), + exact p' ⬝h* (ptrunc_pequiv_natural 0 (Ω→ f)), end definition EM1_pequiv_type_natural {X Y : Type*} (f : X →* Y) [H1 : is_conn 0 X] [H2 : is_trunc 1 X] @@ -286,7 +286,7 @@ namespace EM EMadd1_pequiv'_natural f n ((ptrunc_pequiv 0 (Ω[succ n] X))⁻¹ᵉ* ⬝e* pequiv_of_isomorphism eX) ((ptrunc_pequiv 0 (Ω[succ n] Y))⁻¹ᵉ* ⬝e* pequiv_of_isomorphism eY) - _ _ φ (hhcompose (to_homotopy (phinverse (ptrunc_pequiv_natural 0 (Ω→[succ n] f)))) p) + _ _ φ (hhconcat (to_homotopy (phinverse (ptrunc_pequiv_natural 0 (Ω→[succ n] f)))) p) definition EMadd1_pequiv_succ_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : πag[n+2] X ≃g G) (eY : πag[n+2] Y ≃g H) [is_conn (n.+1) X] [is_trunc (n.+2) X] @@ -383,7 +383,7 @@ namespace EM begin cases n with n, { exact _ }, cases Y with Y H1 H2, cases Y with Y y₀, - exact is_trunc_pmap X n -1 (ptrunctype.mk Y _ y₀), + exact is_trunc_pmap_of_is_conn X n -1 (ptrunctype.mk Y _ y₀), end open category diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index a9a4806..d062ac0 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -12,30 +12,30 @@ open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equ function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi -- TODO: move -structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) := +structure is_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_short_exact_g {A B C : Group} (f : A →g B) (g : B →g C) := -is_short_exact f g +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.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_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_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) := +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) := begin constructor, { intro a, esimp, induction a with a, - exact ap tr (is_short_exact_t.im_in_ker H a) }, + exact ap tr (is_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_short_exact_t.ker_in_im H b q with a r, + induction is_exact_t.ker_in_im H b q with a r, exact image.mk (tr a) (ap tr r) } end -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' := +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' := 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_short_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) := -is_short_exact_trunc_functor (cofiber_exact f) + is_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) := +is_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_short_exact_g (Hh n (pcod f)) (Hh n f)) + (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_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))) diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean index a30a4f5..af83bc4 100644 --- a/homotopy/pushout.hlean +++ b/homotopy/pushout.hlean @@ -464,7 +464,7 @@ namespace pushout /- universal property of cofiber -/ - structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := + structure is_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_short_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) := + is_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 fee624e..cbe1dcc 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -1,6 +1,6 @@ -- Authors: Floris van Doorn -import homotopy.smash ..move_to_lib .pushout homotopy.red_susp +import homotopy.smash ..pointed .pushout homotopy.red_susp open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc function red_susp unit @@ -11,476 +11,11 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w /- 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*} + /- associativity is proven in smash_adjoint -/ +variables {A A' B B' C 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, - { exact sum_functor f g }, - { exact prod_functor f g }, - { exact id }, - { intro v, induction v with a b, - exact prod_eq idp (respect_pt g), - exact prod_eq (respect_pt f) idp }, - { intro v, induction v with a b: reflexivity } - end - - definition smash_functor [constructor] (f : A →* C) (g : B →* D) : A ∧ B →* C ∧ D := - begin - fapply pmap.mk, - { exact smash_functor' f g }, - { exact ap inl (prod_eq (respect_pt f) (respect_pt g)) }, - end - - definition functor_gluel (f : A →* C) (g : B →* D) (a : A) : - ap (smash_functor f g) (gluel a) = ap (smash.mk (f a)) (respect_pt g) ⬝ gluel (f a) := - begin - refine !pushout.elim_glue ⬝ _, esimp, apply whisker_right, - induction D with D d₀, induction g with g g₀, esimp at *, induction g₀, reflexivity - end - - definition functor_gluer (f : A →* C) (g : B →* D) (b : B) : - ap (smash_functor f g) (gluer b) = ap (λc, smash.mk c (g b)) (respect_pt f) ⬝ gluer (g b) := - begin - refine !pushout.elim_glue ⬝ _, esimp, apply whisker_right, - 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))⁻¹ := - begin - refine !ap_con ⬝ !functor_gluel ◾ (!ap_inv ⬝ !functor_gluel⁻²) ⬝ _, - refine whisker_left _ !con_inv ⬝ _, - refine !con.assoc⁻¹ ⬝ _, apply whisker_right, - apply con.assoc - end - - definition functor_gluer' (f : A →* C) (g : B →* D) (b b' : B) : - ap (smash_functor f g) (gluer' b b') = ap (λc, smash.mk c (g b)) (respect_pt f) ⬝ - gluer' (g b) (g b') ⬝ (ap (λc, smash.mk c (g b')) (respect_pt f))⁻¹ := - begin - refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _, - refine !functor_gluer ◾ !functor_gluer⁻² ⬝ _, - refine whisker_left _ !con_inv ⬝ _, - refine !con.assoc⁻¹ ⬝ _, apply whisker_right, - apply con.assoc - end - - /- 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_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_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 (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))⁻¹, - refine _ ⬝ whisker_right _ !con_idp⁻¹, - refine _ ⬝ !con.assoc⁻¹, - apply whisker_left, - apply eq_con_inv_of_con_eq, symmetry, - apply con_right_inv_natural - end - - 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) (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))⁻¹, - refine _ ⬝ whisker_right _ !con_idp⁻¹, - refine _ ⬝ !con.assoc⁻¹, - apply whisker_left, - apply eq_con_inv_of_con_eq, symmetry, - apply con_right_inv_natural - end - - -- 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, 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 (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, - { 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 - 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) := - begin - fapply phomotopy.mk, - { intro x, induction x with a b a b, - { reflexivity }, - { reflexivity }, - { reflexivity }, - { apply eq_pathover_id_right, apply hdeg_square, exact !functor_gluel ⬝ !idp_con }, - { apply eq_pathover_id_right, apply hdeg_square, exact !functor_gluer ⬝ !idp_con }}, - { reflexivity } - end - - definition smash_functor_pid_pcompose [constructor] (A : Type*) (g' : C →* D) (g : B →* C) - : smash_functor (pid A) (g' ∘* g) ~* smash_functor (pid A) g' ∘* smash_functor (pid A) g := - smash_functor_phomotopy !pid_pcompose⁻¹* phomotopy.rfl ⬝* !smash_functor_pcompose - - definition smash_functor_pcompose_pid [constructor] (B : Type*) (f' : C →* D) (f : A →* C) - : 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 := - -- 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, 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 (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 }, - { 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) : - phsquare (smash_functor_pcompose f' f g (pconst B D)) - (smash_functor_pconst_right (f' ∘* f)) - (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g)) - (pwhisker_left (smash_functor f' g) (smash_functor_pconst_right f) ⬝* - pcompose_pconst (smash_functor f' g)) := - begin - 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) : - phsquare (smash_functor_pid_pcompose A g (pconst B D)) - (smash_functor_pconst_right (pid A)) - (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g)) - (pwhisker_left (smash_functor (pid A) g) (smash_functor_pconst_right (pid A)) ⬝* - pcompose_pconst (smash_functor (pid A) g)) := - begin - refine (_ ◾** idp ⬝ !refl_trans) ⬝pv** smash_functor_pconst_right_pcompose (pid A) (pid A) g, - apply smash_functor_phomotopy_refl, - end - - definition smash_functor_pconst_right_pid_pcompose' (g : D →* F) : - pwhisker_left (smash_functor (pid A) g) (smash_functor_pconst_right (pid A)) ⬝* - pcompose_pconst (smash_functor (pid A) g) = - (smash_functor_pid_pcompose A g (pconst B D))⁻¹* ⬝* - (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g) ⬝* - smash_functor_pconst_right (pid A)) := - begin - apply eq_symm_trans_of_trans_eq, - exact smash_functor_pconst_right_pid_pcompose g - end - - definition smash_pequiv_smash [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D := - begin - fapply pequiv_of_pmap (smash_functor f g), - apply pushout.is_equiv_functor, - exact to_is_equiv (sum_equiv_sum f g) - end - - definition smash_pequiv_smash_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B := - smash_pequiv_smash f pequiv.rfl - - definition smash_pequiv_smash_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D := - smash_pequiv_smash pequiv.rfl g - - /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/ - definition elim_gluel' {P : Type} {Pmk : Πa b, P} {Pl Pr : P} (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a a' : A) : ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel' a a') = Pgl a ⬝ (Pgl a')⁻¹ := @@ -529,6 +64,649 @@ namespace smash ap (smash.elim' Pmk Pgl Pgr ql qr) (gluer' b pt) = Pgr b := !elim_gluer' ⬝ whisker_left _ qr⁻² + 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 + + /- the functorial action of the smash product -/ + definition smash_functor' [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D := + begin + intro x, induction x, + { exact smash.mk (f a) (g b) }, + { exact auxl }, + { exact auxr }, + { exact ap (smash.mk (f a)) (respect_pt g) ⬝ gluel (f a) }, + { exact ap (λa, smash.mk a (g b)) (respect_pt f) ⬝ gluer (g b) } + end + + definition smash_functor [constructor] (f : A →* C) (g : B →* D) : A ∧ B →* C ∧ D := + begin + fapply pmap.mk, + { exact smash_functor' f g }, + { exact ap011 smash.mk (respect_pt f) (respect_pt g) }, + end + + infixr ` ∧→ `:65 := smash_functor + + definition functor_gluel (f : A →* C) (g : B →* D) (a : A) : + ap (f ∧→ g) (gluel a) = ap (smash.mk (f a)) (respect_pt g) ⬝ gluel (f a) := + !elim_gluel + + definition functor_gluer (f : A →* C) (g : B →* D) (b : B) : + ap (f ∧→ g) (gluer b) = ap (λc, smash.mk c (g b)) (respect_pt f) ⬝ gluer (g b) := + !elim_gluer + + definition functor_gluel2 {C D : Type} (f : A → C) (g : B → D) (a : A) : + ap (pmap_of_map f pt ∧→ pmap_of_map g pt) (gluel a) = gluel (f a) := + begin + refine !elim_gluel ⬝ !idp_con + end + + definition functor_gluer2 {C D : Type} (f : A → C) (g : B → D) (b : B) : + ap (pmap_of_map f pt ∧→ pmap_of_map g pt) (gluer b) = gluer (g b) := + begin + refine !elim_gluer ⬝ !idp_con + end + + definition functor_gluel' (f : A →* C) (g : B →* D) (a a' : A) : + ap (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))⁻¹ := + begin + refine !elim_gluel' ⬝ _, + refine whisker_left _ !con_inv ⬝ _, + refine !con.assoc⁻¹ ⬝ _, apply whisker_right, + apply con.assoc + end + + definition functor_gluer' (f : A →* C) (g : B →* D) (b b' : B) : + ap (f ∧→ g) (gluer' b b') = ap (λc, smash.mk c (g b)) (respect_pt f) ⬝ + gluer' (g b) (g b') ⬝ (ap (λc, smash.mk c (g b')) (respect_pt f))⁻¹ := + begin + refine !elim_gluer' ⬝ _, + refine whisker_left _ !con_inv ⬝ _, + refine !con.assoc⁻¹ ⬝ _, apply whisker_right, + apply con.assoc + end + + /- 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 (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 (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_gluel'2 {C D : Type} (f : A → C) (g : B → D) (a a' : A) : + ap (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 (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 (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))⁻¹, + refine _ ⬝ whisker_right _ !con_idp⁻¹, + refine _ ⬝ !con.assoc⁻¹, + apply whisker_left, + apply eq_con_inv_of_con_eq, symmetry, + apply con_right_inv_natural + end + + 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 (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))⁻¹, + refine _ ⬝ whisker_right _ !con_idp⁻¹, + refine _ ⬝ !con.assoc⁻¹, + apply whisker_left, + apply eq_con_inv_of_con_eq, symmetry, + apply con_right_inv_natural + end + + definition smash_functor_pid [constructor] (A B : Type*) : + pid A ∧→ pid B ~* pid (A ∧ B) := + begin + fapply phomotopy.mk, + { intro x, induction x with a b a b, + { reflexivity }, + { reflexivity }, + { reflexivity }, + { apply eq_pathover_id_right, apply hdeg_square, exact !functor_gluel ⬝ !idp_con }, + { apply eq_pathover_id_right, apply hdeg_square, exact !functor_gluer ⬝ !idp_con }}, + { reflexivity } + end + + /- the functorial action of the smash product respects pointed homotopies, and some computation + rules for this pointed homotopy -/ + definition smash_functor_phomotopy {f f' : A →* C} {g g' : B →* D} + (h₁ : f ~* f') (h₂ : g ~* g') : f ∧→ g ~* f' ∧→ g' := + begin + induction h₁ using phomotopy_rec_on_idp, + induction h₂ using phomotopy_rec_on_idp, + reflexivity + end + + /- a more explicit proof, if we ever need it -/ + -- definition smash_functor_homotopy [unfold 11] {f f' : A →* C} {g g' : B →* D} + -- (h₁ : f ~* f') (h₂ : g ~* g') : f ∧→ g ~ 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') : f ∧→ g ~* 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_refl (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_phomotopy_symm {f₁ f₂ : A →* C} {g₁ g₂ : B →* D} + (h : f₁ ~* f₂) (k : g₁ ~* g₂) : + smash_functor_phomotopy h⁻¹* k⁻¹* = (smash_functor_phomotopy h k)⁻¹* := + begin + induction h using phomotopy_rec_on_idp, induction k using phomotopy_rec_on_idp, + exact ap011 smash_functor_phomotopy !refl_symm !refl_symm ⬝ !smash_functor_phomotopy_refl ⬝ + !refl_symm⁻¹ ⬝ !smash_functor_phomotopy_refl⁻¹⁻²** + end + + definition smash_functor_phomotopy_trans {f₁ f₂ f₃ : A →* C} {g₁ g₂ g₃ : B →* D} + (h₁ : f₁ ~* f₂) (h₂ : f₂ ~* f₃) (k₁ : g₁ ~* g₂) (k₂ : g₂ ~* g₃) : + smash_functor_phomotopy (h₁ ⬝* h₂) (k₁ ⬝* k₂) = + smash_functor_phomotopy h₁ k₁ ⬝* smash_functor_phomotopy h₂ k₂ := + begin + induction h₁ using phomotopy_rec_on_idp, induction h₂ using phomotopy_rec_on_idp, + induction k₁ using phomotopy_rec_on_idp, induction k₂ using phomotopy_rec_on_idp, + refine ap011 smash_functor_phomotopy !trans_refl !trans_refl ⬝ !trans_refl⁻¹ ⬝ idp ◾** _, + exact !smash_functor_phomotopy_refl⁻¹ + end + + definition smash_functor_phomotopy_trans_right {f₁ f₂ : A →* C} {g₁ g₂ g₃ : B →* D} + (h₁ : f₁ ~* f₂) (k₁ : g₁ ~* g₂) (k₂ : g₂ ~* g₃) : + smash_functor_phomotopy h₁ (k₁ ⬝* k₂) = + smash_functor_phomotopy h₁ k₁ ⬝* smash_functor_phomotopy phomotopy.rfl k₂ := + begin + refine ap (λx, smash_functor_phomotopy x _) !trans_refl⁻¹ ⬝ !smash_functor_phomotopy_trans, + end + + definition smash_functor_phomotopy_phsquare {f₁ f₂ f₃ f₄ : A →* C} {g₁ g₂ g₃ g₄ : B →* D} + {h₁ : f₁ ~* f₂} {h₂ : f₃ ~* f₄} {h₃ : f₁ ~* f₃} {h₄ : f₂ ~* f₄} + {k₁ : g₁ ~* g₂} {k₂ : g₃ ~* g₄} {k₃ : g₁ ~* g₃} {k₄ : g₂ ~* g₄} + (p : phsquare h₁ h₂ h₃ h₄) (q : phsquare k₁ k₂ k₃ k₄) : + phsquare (smash_functor_phomotopy h₁ k₁) + (smash_functor_phomotopy h₂ k₂) + (smash_functor_phomotopy h₃ k₃) + (smash_functor_phomotopy h₄ k₄) := + !smash_functor_phomotopy_trans⁻¹ ⬝ ap011 smash_functor_phomotopy p q ⬝ + !smash_functor_phomotopy_trans + + /- the functorial action preserves compositions, the interchange law -/ + definition smash_functor_pcompose_homotopy [unfold 11] {C D E F : Type} + (f' : C → E) (f : A → C) (g' : D → F) (g : B → D) : + (pmap_of_map f' (f pt) ∘* pmap_of_map f pt) ∧→ (pmap_of_map g' (g pt) ∘* pmap_of_map g pt) ~ + (pmap_of_map f' (f pt) ∧→ pmap_of_map g' (g pt)) ∘* (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, refine !functor_gluel2 ⬝ph _, esimp, + refine _ ⬝hp (ap_compose (_ ∧→ _) _ _)⁻¹, + refine _ ⬝hp ap02 _ !functor_gluel2⁻¹, refine _ ⬝hp !functor_gluel2⁻¹, exact hrfl }, + { apply eq_pathover, refine !functor_gluer2 ⬝ph _, esimp, + refine _ ⬝hp (ap_compose (_ ∧→ _) _ _)⁻¹, + refine _ ⬝hp ap02 _ !functor_gluer2⁻¹, refine _ ⬝hp !functor_gluer2⁻¹, exact hrfl } + end + + definition smash_functor_pcompose (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) : + (f' ∘* f) ∧→ (g' ∘* g) ~* f' ∧→ g' ∘* 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, + { rexact smash_functor_pcompose_homotopy f' f g' g }, + { reflexivity } + end + + /- An alternative proof which doesn't start by applying inductions, so which is more explicit -/ + -- definition smash_functor_pcompose_homotopy [unfold 11] (f' : C →* E) (f : A →* C) (g' : D →* F) + -- (g : B →* D) : (f' ∘* f) ∧→ (g' ∘* g) ~ (f' ∧→ g') ∘* (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 (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 (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) : + -- (f' ∘* f) ∧→ (g' ∘* g) ~* f' ∧→ g' ∘* 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_pid_pcompose [constructor] (A : Type*) (g' : C →* D) (g : B →* C) + : pid A ∧→ (g' ∘* g) ~* pid A ∧→ g' ∘* pid A ∧→ g := + smash_functor_phomotopy !pid_pcompose⁻¹* phomotopy.rfl ⬝* !smash_functor_pcompose + + definition smash_functor_pcompose_pid [constructor] (B : Type*) (f' : C →* D) (f : A →* C) + : (f' ∘* f) ∧→ pid B ~* f' ∧→ (pid B) ∘* f ∧→ (pid B) := + smash_functor_phomotopy phomotopy.rfl !pid_pcompose⁻¹* ⬝* !smash_functor_pcompose + + /- composing commutes with applying homotopies -/ + definition smash_functor_pcompose_phomotopy {f₂ f₂' : C →* E} {f f' : A →* C} {g₂ g₂' : D →* F} + {g g' : B →* D} (h₂ : f₂ ~* f₂') (h₁ : f ~* f') (k₂ : g₂ ~* g₂') (k₁ : g ~* g') : + phsquare (smash_functor_pcompose f₂ f g₂ g) + (smash_functor_pcompose f₂' f' g₂' g') + (smash_functor_phomotopy (h₂ ◾* h₁) (k₂ ◾* k₁)) + (smash_functor_phomotopy h₂ k₂ ◾* smash_functor_phomotopy h₁ k₁) := + begin + induction h₁ using phomotopy_rec_on_idp, induction h₂ using phomotopy_rec_on_idp, + induction k₁ using phomotopy_rec_on_idp, induction k₂ using phomotopy_rec_on_idp, + refine (ap011 smash_functor_phomotopy !pcompose2_refl !pcompose2_refl ⬝ + !smash_functor_phomotopy_refl) ⬝ph** phvrfl ⬝hp** + (ap011 pcompose2 !smash_functor_phomotopy_refl !smash_functor_phomotopy_refl ⬝ + !pcompose2_refl)⁻¹, + end + + definition smash_functor_pid_pcompose_phomotopy_right (g₂ : D →* E) {g g' : B →* D} + (k : g ~* g') : + phsquare (smash_functor_pid_pcompose A g₂ g) + (smash_functor_pid_pcompose A g₂ g') + (smash_functor_phomotopy phomotopy.rfl (pwhisker_left g₂ k)) + (pwhisker_left (pid A ∧→ g₂) (smash_functor_phomotopy phomotopy.rfl k)) := + begin + refine smash_functor_phomotopy_phsquare _ _ ⬝h** !smash_functor_pcompose_phomotopy ⬝hp** + ((ap (pwhisker_right _) !smash_functor_phomotopy_refl) ◾** idp ⬝ !pcompose2_refl_left), + exact (!pcompose2_refl ⬝ph** phvrfl)⁻¹ʰ**, + exact (phhrfl ⬝hp** !pcompose2_refl_left⁻¹) + end + + section + variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*} {B₀₀ B₂₀ B₀₂ B₂₂ : Type*} + {f₁₀ : A₀₀ →* A₂₀} {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} {f₁₂ : A₀₂ →* A₂₂} + {g₁₀ : B₀₀ →* B₂₀} {g₀₁ : B₀₀ →* B₀₂} {g₂₁ : B₂₀ →* B₂₂} {g₁₂ : B₀₂ →* B₂₂} + + /- applying the functorial action of smash to squares of pointed maps -/ + definition smash_functor_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare g₁₀ g₁₂ g₀₁ g₂₁) : + psquare (f₁₀ ∧→ g₁₀) (f₁₂ ∧→ g₁₂) (f₀₁ ∧→ g₀₁) (f₂₁ ∧→ g₂₁) := + !smash_functor_pcompose⁻¹* ⬝* smash_functor_phomotopy p q ⬝* !smash_functor_pcompose + end + + /- f ∧ g is constant if g is constant -/ + definition smash_functor_pconst_right_homotopy [unfold 6] {C : Type} (f : A → C) (x : A ∧ B) : + (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, 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 (f : A →* C) : + 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 }, + { rexact con.right_inv (gluel (f pt)) } + end + + definition smash_functor_pconst_right_phomotopy {f f' : A →* C} (p : f ~* f') : + smash_functor_phomotopy p (phomotopy.refl (pconst B D)) ⬝* smash_functor_pconst_right f' = + smash_functor_pconst_right f := + begin + induction p using phomotopy_rec_on_idp, + exact !smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans + end + + /- We need two coherence rules for the naturality of the smash-pmap adjunction. Given the function + h := (f' ∘ f) ∧→ (g' ∘ g) and suppose that either g' or g is constant. There are two ways to + show that h is constant: either by using exchange, or directly. We need to show that these two + proofs result in the same pointed homotopy. First we do the case where g is constant -/ + + 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_pcompose_pconst_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)), + apply my_cube_fillerr end end } + end + + definition smash_functor_pcompose_pconst (f' : C →* E) (f : A →* C) (g : D →* F) : + phsquare (smash_functor_pcompose f' f g (pconst B D)) + (smash_functor_pconst_right (f' ∘* f)) + (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g)) + (pwhisker_left (f' ∧→ g) (smash_functor_pconst_right f) ⬝* + pcompose_pconst (f' ∧→ g)) := + begin + 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_pcompose_pconst_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 + + /- a version where the left maps are identities -/ + definition smash_functor_pid_pcompose_pconst (g : D →* F) : + phsquare (smash_functor_pid_pcompose A g (pconst B D)) + (smash_functor_pconst_right (pid A)) + (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g)) + (pwhisker_left (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝* + pcompose_pconst (pid A ∧→ g)) := + begin + refine (_ ◾** idp ⬝ !refl_trans) ⬝pv** smash_functor_pcompose_pconst (pid A) (pid A) g, + apply smash_functor_phomotopy_refl, + end + + /- a small rewrite of the previous -/ + definition smash_functor_pid_pcompose_pconst' (g : D →* F) : + pwhisker_left (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝* + pcompose_pconst (pid A ∧→ g) = + (smash_functor_pid_pcompose A g (pconst B D))⁻¹* ⬝* + (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g) ⬝* + smash_functor_pconst_right (pid A)) := + begin + apply eq_symm_trans_of_trans_eq, + exact smash_functor_pid_pcompose_pconst g + end + + /- if g' is constant -/ + definition smash_functor_pconst_pcompose_homotopy [unfold 13] {A B C D E F : Type} + (a₀ : A) (b₀ : B) (x₀ : F) (f' : C → E) (f : A → C) (g : B → D) + (x : pointed.MK A a₀ ∧ pointed.MK B b₀) : + square (smash_functor_pcompose_homotopy f' f (λ a, x₀) g x) + idp + (smash_functor_pconst_right_homotopy (λ a, f' (f a)) x) + (smash_functor_pconst_right_homotopy f' + (smash_functor (pmap_of_map f a₀) (pmap_of_map g b₀) x)) := + begin + induction x with a b a b, + { exact hrfl }, + { exact hrfl }, + { 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_compose (smash_functor_pconst_right_homotopy f') _ _)⁻¹ᵖ, + 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 (natural_square_eq2 _ !functor_gluel2)⁻¹ᵖ, + apply whisker021, + refine _ ⬝1p ap hdeg_square (eq_of_square (!ap_constant_compose⁻¹ʰ) ⬝ !idp_con)⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝2p !rec_eq_gluel⁻¹, apply whisker021, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_constant)), + exact rfl2 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_compose (smash_functor_pconst_right_homotopy f') _ _)⁻¹ᵖ, + 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 (natural_square_eq2 _ !functor_gluer2)⁻¹ᵖ, + apply whisker021, + refine _ ⬝1p ap hdeg_square (eq_of_square (!ap_constant_compose⁻¹ʰ) ⬝ !idp_con)⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝2p !rec_eq_gluer⁻¹, apply whisker021, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_constant)), + exact rfl2 end end }, + end + + definition smash_functor_pconst_pcompose (f' : C →* E) (f : A →* C) (g : B →* D) : + phsquare (smash_functor_pcompose f' f (pconst D F) g) + (smash_functor_pconst_right (f' ∘* f)) + (smash_functor_phomotopy phomotopy.rfl (pconst_pcompose g)) + (pwhisker_right (f ∧→ g) (smash_functor_pconst_right f') ⬝* + pconst_pcompose (f ∧→ g)) := + begin + 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 (smash_functor_pconst_pcompose_homotopy a₀ b₀ x₀ f' f g x) }, + { refine whisker_right _ (!whisker_right_idp ⬝ !eq_of_square_hrfl) ⬝ _, + have H : Π{A : Type} {a a' : A} (p : a = a'), + idp_con (p ⬝ p⁻¹) ⬝ con.right_inv p = idp ⬝ + whisker_left idp (idp ⬝ (idp ⬝ proof whisker_right idp (idp_con (p ⬝ p⁻¹ᵖ))⁻¹ᵖ qed ⬝ + whisker_left idp (con.right_inv p))), by intros; induction p; reflexivity, + rexact H (gluel (f' (f a₀))) } + end + + /- a lemma using both these rules -/ + + definition smash_psquare_lemma (f : A →* A') (g : B →* B') + : phsquare (smash_functor_psquare (pvrefl g) (pid_pcompose (pconst A' C ∘* f))⁻¹*) + (pconst_pcompose (g ∧→ f)) + (pwhisker_right (g ∧→ f) (smash_functor_pconst_right (pid B'))) + (pwhisker_left (g ∧→ pid C) + (smash_functor_phomotopy phomotopy.rfl (pconst_pcompose f) ⬝* + smash_functor_pconst_right (pid B)) ⬝* + pcompose_pconst (g ∧→ pid C)) := + begin + refine !trans_assoc ⬝pv** _, + apply phmove_top_of_left', + refine _ ⬝ (!trans_assoc ⬝ !smash_functor_pconst_pcompose)⁻¹, + refine !trans_assoc⁻¹ ⬝ trans_eq_of_eq_trans_symm _, + refine _ ⬝hp** !pwhisker_left_trans⁻¹, + refine (smash_functor_phomotopy_phsquare (phvrfl ⬝hp** !pcompose2_refl⁻¹) + (!pcompose2_refl_left ⬝ph** !pid_pconst_pcompose)⁻¹ʰ** ⬝h** + !smash_functor_pcompose_phomotopy ⬝hp** + (!smash_functor_phomotopy_refl ◽* idp ⬝ !pcompose2_refl_left)) ⬝v** _, + refine ((!smash_functor_phomotopy_trans⁻¹ ⬝ + ap011 smash_functor_phomotopy !trans_refl !refl_trans) ◾** idp) ⬝ph** idp ⬝ _, + refine !trans_assoc ⬝ !trans_assoc ⬝ _, + apply trans_eq_of_eq_symm_trans, + refine _ ⬝ !trans_assoc ⬝ (ap (smash_functor_phomotopy _) !refl_symm⁻¹ ⬝ + !smash_functor_phomotopy_symm) ◾** idp, + refine _ ⬝ !smash_functor_pconst_right_phomotopy⁻¹ ◾** idp, + apply trans_eq_of_eq_symm_trans, + refine _ ⬝ !trans_assoc ⬝ (ap011 smash_functor_phomotopy !refl_symm⁻¹ !refl_symm⁻¹ ⬝ + !smash_functor_phomotopy_symm) ◾** idp, + apply eq_trans_symm_of_trans_eq, refine !trans_assoc ⬝ _, + apply smash_functor_pcompose_pconst + end + + + /- f ∧ g is a pointed equivalence if f and g are -/ + definition smash_functor_using_pushout [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D := + begin + fapply pushout.functor (sum_functor f g) (prod_functor f g) id, + { intro v, induction v with a b, + exact prod_eq idp (respect_pt g), + exact prod_eq (respect_pt f) idp }, + { intro v, induction v with a b: reflexivity } + end + + definition smash_functor_homotopy_pushout_functor (f : A →* C) (g : B →* D) : + f ∧→ g ~ smash_functor_using_pushout f g := + begin + intro x, induction x, + { reflexivity }, + { reflexivity }, + { reflexivity }, + { apply eq_pathover, refine !elim_gluel ⬝ph _ ⬝hp !pushout.elim_glue⁻¹, + apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ }, + { apply eq_pathover, refine !elim_gluer ⬝ph _ ⬝hp !pushout.elim_glue⁻¹, + apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ } + end + + local attribute is_equiv_sum_functor [instance] + definition smash_pequiv_smash [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D := + begin + fapply pequiv_of_pmap (f ∧→ g), + refine @homotopy_closed _ _ _ _ _ (smash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ, + apply pushout.is_equiv_functor + end + + definition smash_pequiv_smash_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B := + smash_pequiv_smash f pequiv.rfl + + definition smash_pequiv_smash_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D := + smash_pequiv_smash pequiv.rfl g + + /- A ∧ B ≃* pcofiber (pprod_of_pwedge A B) -/ + definition prod_of_wedge [unfold 3] (v : pwedge A B) : A × B := begin induction v with a b , @@ -544,7 +722,6 @@ namespace smash { exact pushout.inr b } end - definition prod_of_wedge_of_sum [unfold 3] (v : A + B) : prod_of_wedge (wedge_of_sum v) = prod_of_sum v := begin induction v with a b, @@ -609,24 +786,6 @@ namespace smash variables (A B) - definition smash_punit_pequiv [constructor] : smash A punit ≃* punit := - begin - fapply pequiv_of_equiv, - { fapply equiv.MK, - { exact λx, ⋆ }, - { exact λx, pt }, - { intro x, induction x, reflexivity }, - { exact abstract begin intro x, induction x, - { induction b, exact gluel' pt a }, - { exact gluel pt }, - { exact gluer pt }, - { apply eq_pathover_constant_left_id_right, apply square_of_eq_top, - exact whisker_right _ !idp_con⁻¹ }, - { apply eq_pathover_constant_left_id_right, induction b, - refine !con.right_inv ⬝pv _, exact square_of_eq idp } end end }}, - { reflexivity } - end - definition smash_equiv_cofiber : smash A B ≃ cofiber (@prod_of_wedge A B) := begin unfold [smash, cofiber, smash'], symmetry, @@ -636,6 +795,20 @@ namespace smash { apply prod_of_wedge_of_sum } end + definition smash_punit_pequiv [constructor] : smash A punit ≃* punit := + begin + apply pequiv_punit_of_is_contr, + apply is_contr.mk (smash.mk pt ⋆), intro x, + induction x, + { induction b, exact gluel' pt a }, + { exact gluel pt }, + { exact gluer pt }, + { apply eq_pathover_constant_left_id_right, apply square_of_eq_top, + exact whisker_right _ !idp_con⁻¹ }, + { apply eq_pathover_constant_left_id_right, induction b, + refine !con.right_inv ⬝pv _, exact square_of_eq idp }, + end + definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B := begin fconstructor, @@ -653,7 +826,7 @@ namespace smash /- commutativity -/ - definition smash_flip [unfold 3] (x : smash A B) : smash B A := + definition smash_flip' [unfold 3] (x : smash A B) : smash B A := begin induction x, { exact smash.mk b a }, @@ -663,223 +836,57 @@ namespace smash { exact gluel b } end - definition smash_flip_smash_flip [unfold 3] (x : smash A B) : smash_flip (smash_flip x) = x := + definition smash_flip_smash_flip' [unfold 3] (x : smash A B) : smash_flip' (smash_flip' x) = x := begin induction x, { reflexivity }, { reflexivity }, { reflexivity }, { apply eq_pathover_id_right, - refine ap_compose' smash_flip _ _ ⬝ ap02 _ !elim_gluel ⬝ !elim_gluer ⬝ph _, + refine ap_compose' smash_flip' _ _ ⬝ ap02 _ !elim_gluel ⬝ !elim_gluer ⬝ph _, apply hrfl }, { apply eq_pathover_id_right, - refine ap_compose' smash_flip _ _ ⬝ ap02 _ !elim_gluer ⬝ !elim_gluel ⬝ph _, + refine ap_compose' smash_flip' _ _ ⬝ ap02 _ !elim_gluer ⬝ !elim_gluel ⬝ph _, apply hrfl } end variables (A B) + + definition smash_flip [constructor] : smash A B →* smash B A := + pmap.mk smash_flip' idp + + definition smash_flip_smash_flip [constructor] : + smash_flip B A ∘* smash_flip A B ~* pid (A ∧ B) := + phomotopy.mk smash_flip_smash_flip' idp + definition smash_comm [constructor] : smash A B ≃* smash B A := begin - fapply pequiv_of_equiv, - { apply equiv.MK, do 2 exact smash_flip_smash_flip }, - { reflexivity } + apply pequiv.MK2, do 2 apply smash_flip_smash_flip end + variables {A B} - - /- smash A S¹ = red_susp A -/ - - definition circle_elim_constant [unfold 5] {A : Type} {a : A} {p : a = a} (r : p = idp) (x : S¹) : - circle.elim a p x = a := + definition smash_flip_smash_functor' [unfold 7] (f : A →* C) (g : B →* D) : hsquare + smash_flip' smash_flip' (smash_functor' f g) (smash_functor' g f) := begin - induction x, + intro x, induction x, { reflexivity }, - { apply eq_pathover_constant_right, apply hdeg_square, exact !elim_loop ⬝ r } - end - - definition red_susp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : red_susp A := - begin - induction x using smash.elim, - { induction b, exact base, exact equator a }, - { exact base }, - { exact base }, { reflexivity }, - { exact circle_elim_constant equator_pt b } - end - - definition smash_pcircle_of_red_susp [unfold 2] (x : red_susp A) : smash A S¹* := - begin - induction x, - { exact pt }, - { exact gluel' pt a ⬝ ap (smash.mk a) loop ⬝ gluel' a pt }, - { refine !con.right_inv ◾ _ ◾ !con.right_inv, - exact ap_is_constant gluer loop ⬝ !con.right_inv } - end -exit - definition smash_pcircle_of_red_susp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) : - smash_pcircle_of_red_susp (red_susp_of_smash_pcircle (smash.mk a x)) = smash.mk a x := - begin - induction x, - { exact gluel' pt a }, - { exact abstract begin apply eq_pathover, - refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _, - refine ap02 _ (elim_loop pt (equator a)) ⬝ !elim_equator ⬝ph _, - -- make everything below this a lemma defined by path induction? - refine !con_idp⁻¹ ⬝pv _, refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb, - apply whisker_tl, apply hrfl end end } - end - - definition concat2o [unfold 10] {A B : Type} {f g h : A → B} {q : f ~ g} {r : g ~ h} {a a' : A} - {p : a = a'} (s : q a =[p] q a') (t : r a =[p] r a') : q a ⬝ r a =[p] q a' ⬝ r a' := - by induction p; exact idpo - - definition apd_con_fn [unfold 10] {A B : Type} {f g h : A → B} {q : f ~ g} {r : g ~ h} {a a' : A} - (p : a = a') : apd (λa, q a ⬝ r a) p = concat2o (apd q p) (apd r p) := - by induction p; reflexivity - - -- definition apd_con_fn_constant [unfold 10] {A B : Type} {f : A → B} {b b' : B} {q : Πa, f a = b} - -- {r : b = b'} {a a' : A} (p : a = a') : - -- apd (λa, q a ⬝ r) p = concat2o (apd q p) (pathover_of_eq _ idp) := - -- by induction p; reflexivity - - theorem apd_constant' {A A' : Type} {B : A' → Type} {a₁ a₂ : A} {a' : A'} (b : B a') - (p : a₁ = a₂) : apd (λx, b) p = pathover_of_eq p idp := - by induction p; reflexivity - - definition smash_pcircle_pequiv_red [constructor] (A : Type*) : smash A S¹* ≃* red_susp A := - begin - fapply pequiv_of_equiv, - { fapply equiv.MK, - { exact red_susp_of_smash_pcircle }, - { exact smash_pcircle_of_red_susp }, - { exact abstract begin intro x, induction x, - { reflexivity }, - { apply eq_pathover, apply hdeg_square, - refine ap_compose red_susp_of_smash_pcircle _ _ ⬝ ap02 _ !elim_equator ⬝ _ ⬝ !ap_id⁻¹, - refine !ap_con ⬝ (!ap_con ⬝ !elim_gluel' ◾ !ap_compose'⁻¹) ◾ !elim_gluel' ⬝ _, - esimp, exact !idp_con ⬝ !elim_loop }, - { exact sorry } end end }, - { intro x, induction x, - { exact smash_pcircle_of_red_susp_of_smash_pcircle_pt a b }, - { exact gluel pt }, - { exact gluer pt }, - { apply eq_pathover_id_right, - refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _, - unfold [red_susp_of_smash_pcircle], - refine ap02 _ !elim_gluel ⬝ph _, - esimp, apply whisker_rt, exact vrfl }, - { apply eq_pathover_id_right, - refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _, - unfold [red_susp_of_smash_pcircle], - -- not sure why so many implicit arguments are needed here... - refine ap02 _ (@smash.elim_gluer A S¹* _ (λa, circle.elim red_susp.base (equator a)) red_susp.base red_susp.base (λa, refl red_susp.base) (circle_elim_constant equator_pt) b) ⬝ph _, - apply square_of_eq, induction b, - { exact whisker_right _ !con.right_inv }, - { apply eq_pathover_dep, refine !apd_con_fn ⬝pho _ ⬝hop !apd_con_fn⁻¹, - refine ap (λx, concat2o x _) !rec_loop ⬝pho _ ⬝hop (ap011 concat2o (apd_compose1 (λa b, ap smash_pcircle_of_red_susp b) (circle_elim_constant equator_pt) loop) !apd_constant')⁻¹, - exact sorry } - - }}}, - { reflexivity } - end - - /- smash A S¹ = susp A -/ - open susp - - - definition psusp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : psusp A := - begin - induction x using smash.elim, - { induction b, exact pt, exact merid a ⬝ (merid pt)⁻¹ }, - { exact pt }, - { exact pt }, { reflexivity }, - { induction b, reflexivity, apply eq_pathover_constant_right, apply hdeg_square, - exact !elim_loop ⬝ !con.right_inv } + { apply eq_pathover, + refine ap_compose' (smash_functor' _ _) _ _ ⬝ ap02 _ !elim_gluel ⬝ !functor_gluer ⬝ph _ + ⬝hp (ap_compose' smash_flip' _ _ ⬝ ap02 _ !functor_gluel)⁻¹ᵖ, + refine _ ⬝hp (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel)⁻¹, exact hrfl }, + { apply eq_pathover, + refine ap_compose' (smash_functor' _ _) _ _ ⬝ ap02 _ !elim_gluer ⬝ !functor_gluel ⬝ph _ + ⬝hp (ap_compose' smash_flip' _ _ ⬝ ap02 _ !functor_gluer)⁻¹ᵖ, + refine _ ⬝hp (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer)⁻¹, exact hrfl }, end - definition smash_pcircle_of_psusp [unfold 2] (x : psusp A) : smash A S¹* := + definition smash_flip_smash_functor (f : A →* C) (g : B →* D) : psquare + (smash_flip A B) (smash_flip C D) (f ∧→ g) (g ∧→ f) := begin - induction x, - { exact pt }, - { exact pt }, - { exact gluel' pt a ⬝ (ap (smash.mk a) loop ⬝ gluel' a pt) }, - end - - -- the definitions below compile, but take a long time to do so and have sorry's in them - definition smash_pcircle_of_psusp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) : - smash_pcircle_of_psusp (psusp_of_smash_pcircle (smash.mk a x)) = smash.mk a x := - begin - induction x, - { exact gluel' pt a }, - { exact abstract begin apply eq_pathover, - refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _, - refine ap02 _ (elim_loop north (merid a ⬝ (merid pt)⁻¹)) ⬝ph _, - refine !ap_con ⬝ (!elim_merid ◾ (!ap_inv ⬝ !elim_merid⁻²)) ⬝ph _, - -- make everything below this a lemma defined by path induction? - exact sorry, - -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, refine !con.assoc⁻¹ ⬝ph _, - -- apply whisker_bl, apply whisker_lb, - -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, apply hrfl - -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, - -- refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb, apply hrfl - -- apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left, - -- symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv, - -- refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc, - -- refine _ ⬝ whisker_right _ !inv_con_cancel_right⁻¹, refine _ ⬝ !con.right_inv⁻¹, - -- refine !con.right_inv ◾ _, refine _ ◾ !con.right_inv, - -- refine !ap_mk_right ⬝ !con.right_inv - end end } - end - - -- definition smash_pcircle_of_psusp_of_smash_pcircle_gluer_base (b : S¹*) - -- : square (smash_pcircle_of_psusp_of_smash_pcircle_pt (Point A) b) - -- (gluer pt) - -- (ap smash_pcircle_of_psusp (ap (λ a, psusp_of_smash_pcircle a) (gluer b))) - -- (gluer b) := - -- begin - -- refine ap02 _ !elim_gluer ⬝ph _, - -- induction b, - -- { apply square_of_eq, exact whisker_right _ !con.right_inv }, - -- { apply square_pathover', exact sorry } - -- end - -exit - definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* psusp A := - begin - fapply pequiv_of_equiv, - { fapply equiv.MK, - { exact psusp_of_smash_pcircle }, - { exact smash_pcircle_of_psusp }, - { exact abstract begin intro x, induction x, - { reflexivity }, - { exact merid pt }, - { apply eq_pathover_id_right, - refine ap_compose psusp_of_smash_pcircle _ _ ⬝ph _, - refine ap02 _ !elim_merid ⬝ph _, - rewrite [↑gluel', +ap_con, +ap_inv, -ap_compose'], - refine (_ ◾ _⁻² ◾ _ ◾ (_ ◾ _⁻²)) ⬝ph _, - rotate 5, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel), - esimp, apply elim_loop, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel), - refine idp_con (merid a ⬝ (merid (Point A))⁻¹) ⬝ph _, - apply square_of_eq, refine !idp_con ⬝ _⁻¹, apply inv_con_cancel_right } end end }, - { intro x, induction x using smash.rec, - { exact smash_pcircle_of_psusp_of_smash_pcircle_pt a b }, - { exact gluel pt }, - { exact gluer pt }, - { apply eq_pathover_id_right, - refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _, - unfold [psusp_of_smash_pcircle], - refine ap02 _ !elim_gluel ⬝ph _, - esimp, apply whisker_rt, exact vrfl }, - { apply eq_pathover_id_right, - refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _, - unfold [psusp_of_smash_pcircle], - refine ap02 _ !elim_gluer ⬝ph _, - induction b, - { apply square_of_eq, exact whisker_right _ !con.right_inv }, - { exact sorry} - }}}, - { reflexivity } + apply phomotopy.mk (smash_flip_smash_functor' f g), refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, + refine !ap_ap011 ⬝ _, apply ap011_flip, end end smash diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index da2c596..6213abb 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -1,7 +1,7 @@ -- Authors: Floris van Doorn -- in collaboration with Egbert, Stefano, Robin, Ulrik - +/- the adjunction between the smash product and pointed maps -/ import .smash open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc @@ -10,8 +10,9 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w namespace smash - variables {A B C : Type*} + variables {A A' B B' C C' X X' : Type*} + /- we start by defining the unit of the adjunction -/ definition pinl [constructor] (A : Type*) {B : Type*} (b : B) : A →* A ∧ B := begin fapply pmap.mk, @@ -19,20 +20,13 @@ namespace smash { exact gluer' b pt } end - definition pinl_phomotopy {A B : Type*} {b b' : B} (p : b = b') : pinl A b ~* pinl A b' := + definition pinl_phomotopy {b b' : B} (p : b = b') : pinl A b ~* pinl A b' := begin fapply phomotopy.mk, { exact ap010 (pmap.to_fun ∘ pinl A) p }, { induction p, apply idp_con } end - definition pinr [constructor] {A : Type*} (B : Type*) (a : A) : B →* A ∧ B := - begin - fapply pmap.mk, - { intro b, exact smash.mk a b }, - { exact gluel' a pt } - end - definition smash_pmap_unit_pt [constructor] (A B : Type*) : pinl A pt ~* pconst A (A ∧ B) := begin @@ -41,6 +35,7 @@ namespace smash { rexact con.right_inv (gluel pt) ⬝ (con.right_inv (gluer pt))⁻¹ } end + /- We chose an unfortunate order of arguments, but it might be bothersome to change it-/ definition smash_pmap_unit [constructor] (A B : Type*) : B →* ppmap A (A ∧ B) := begin fapply pmap.mk, @@ -48,6 +43,7 @@ namespace smash { apply eq_of_phomotopy, exact smash_pmap_unit_pt A B } end + /- The unit is natural in the second argument -/ 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 @@ -87,7 +83,7 @@ namespace smash rexact functor_gluer'2_same (pmap_of_map id (Point A)) (pmap_of_map f pt) pt } end - definition smash_pmap_unit_natural {A B C : Type*} (f : B →* C) : + definition smash_pmap_unit_natural (f : B →* C) : smash_pmap_unit A C ∘* f ~* ppcompose_left (smash_functor (pid A) f) ∘* smash_pmap_unit A B := begin @@ -98,16 +94,16 @@ namespace smash ⬝ ap phomotopy_of_eq !respect_pt_pcompose⁻¹, esimp, refine _ ⬝ ap phomotopy_of_eq !idp_con⁻¹, refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, - refine ap (λx, _ ⬝* phomotopy_of_eq (x ⬝ _)) !pcompose_eq_of_phomotopy ⬝ _, + refine ap (λx, _ ⬝* phomotopy_of_eq (x ⬝ _)) !pcompose_left_eq_of_phomotopy ⬝ _, refine ap (λx, _ ⬝* x) (!phomotopy_of_eq_con ⬝ - ap011 phomotopy.trans !phomotopy_of_eq_of_phomotopy - !phomotopy_of_eq_of_phomotopy ⬝ !trans_refl) ⬝ _, + !phomotopy_of_eq_of_phomotopy ◾** !phomotopy_of_eq_of_phomotopy ⬝ !trans_refl) ⬝ _, refine _ ⬝ smash_pmap_unit_pt_natural (pmap_of_map f b₀) ⬝ _, { exact !trans_refl⁻¹ }, { exact !refl_trans }} end - definition smash_pmap_counit_map [unfold 3] {A B : Type*} (af : A ∧ (ppmap A B)) : B := + /- The counit -/ + definition smash_pmap_counit_map [unfold 3] (af : A ∧ (ppmap A B)) : B := begin induction af with a f a f, { exact f a }, @@ -124,8 +120,9 @@ namespace smash { reflexivity } end - definition smash_pmap_counit_natural {A B C : Type*} (g : B →* C) : - g ∘* smash_pmap_counit A B ~* smash_pmap_counit A C ∘* smash_functor (pid A) (ppcompose_left g) := + /- The counit is natural in both arguments -/ + definition smash_pmap_counit_natural (g : B →* C) : g ∘* smash_pmap_counit A B ~* + smash_pmap_counit A C ∘* smash_functor (pid A) (ppcompose_left g) := begin symmetry, fapply phomotopy.mk, @@ -147,10 +144,34 @@ namespace smash refine !idp_con ⬝ph _, apply square_of_eq, refine !idp_con ⬝ !con_inv_cancel_right⁻¹ }}, { refine !idp_con ⬝ !idp_con ⬝ _, refine _ ⬝ !ap_compose', - refine _ ⬝ !ap_prod_elim⁻¹, esimp, refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, refine !idp_con⁻¹ } end + definition smash_pmap_counit_natural_left (g : A →* A') : + smash_pmap_counit A' B ∘* g ∧→ (pid (ppmap A' B)) ~* + smash_pmap_counit A B ∘* (pid A) ∧→ (ppcompose_right g) := + begin + fapply phomotopy.mk, + { intro af, induction af with a f a f, + { reflexivity }, + { reflexivity }, + { reflexivity }, + { apply eq_pathover, apply hdeg_square, + refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ (!elim_gluel ⬝ !idp_con) ⬝ + !elim_gluel ⬝ _, + refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluel ⬝ !ap_con ⬝ + !ap_compose'⁻¹ ◾ !elim_gluel ⬝ !con_idp ⬝ _)⁻¹, + refine !to_fun_eq_of_phomotopy ⬝ _, reflexivity }, + { apply eq_pathover, apply hdeg_square, + refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝ + !ap_compose'⁻¹ ◾ !elim_gluer ⬝ _, + refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝ + !ap_compose'⁻¹ ◾ !elim_gluer ⬝ !idp_con)⁻¹ }}, + { refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _ ⬝ !ap_ap011⁻¹, esimp, + refine !to_fun_eq_of_phomotopy ⬝ _, exact !ap_constant⁻¹, } + end + + /- The unit-counit laws -/ definition smash_pmap_unit_counit (A B : Type*) : smash_pmap_counit A (A ∧ B) ∘* smash_functor (pid A) (smash_pmap_unit A B) ~* pid (A ∧ B) := begin @@ -170,12 +191,11 @@ namespace smash refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _, refine !idp_con ⬝ph _, apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ }}, - { refine _ ⬝ !ap_compose', - refine _ ⬝ !ap_prod_elim⁻¹, refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, + { refine _ ⬝ !ap_compose', refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, rexact (con.right_inv (gluer pt))⁻¹ } end - definition smash_pmap_counit_unit_pt [constructor] {A B : Type*} (f : A →* B) : + definition smash_pmap_counit_unit_pt [constructor] (f : A →* B) : smash_pmap_counit A B ∘* pinl A f ~* f := begin fconstructor, @@ -189,10 +209,9 @@ namespace smash fapply phomotopy_mk_ppmap, { intro f, exact smash_pmap_counit_unit_pt f }, { refine !trans_refl ⬝ _, - refine _ ⬝ ap (λx, phomotopy_of_eq (x ⬝ _)) !pcompose_eq_of_phomotopy⁻¹, + refine _ ⬝ ap (λx, phomotopy_of_eq (x ⬝ _)) !pcompose_left_eq_of_phomotopy⁻¹, refine _ ⬝ !phomotopy_of_eq_con⁻¹, - refine _ ⬝ ap011 phomotopy.trans !phomotopy_of_eq_of_phomotopy⁻¹ - !phomotopy_of_eq_of_phomotopy⁻¹, + refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ ◾** !phomotopy_of_eq_of_phomotopy⁻¹, refine _ ⬝ !trans_refl⁻¹, fapply phomotopy_eq, { intro a, refine !elim_gluel'⁻¹ }, @@ -204,13 +223,15 @@ namespace smash exact !idp_con }} end - definition smash_elim [constructor] {A B C : Type*} (f : A →* ppmap B C) : B ∧ A →* C := + /- The underlying (unpointed) functions of the equivalence A →* (B →* C) ≃* A ∧ B →* C) -/ + definition smash_elim [constructor] (f : A →* ppmap B C) : B ∧ A →* C := smash_pmap_counit B C ∘* smash_functor (pid B) f - definition smash_elim_inv [constructor] {A B C : Type*} (g : A ∧ B →* C) : B →* ppmap A C := + definition smash_elim_inv [constructor] (g : A ∧ B →* C) : B →* ppmap A C := ppcompose_left g ∘* smash_pmap_unit A B - definition smash_elim_left_inv {A B C : Type*} (f : A →* ppmap B C) : smash_elim_inv (smash_elim f) ~* f := + /- They are inverses, constant on the constant function and natural -/ + definition smash_elim_left_inv (f : A →* ppmap B C) : smash_elim_inv (smash_elim f) ~* f := begin refine !pwhisker_right !ppcompose_left_pcompose ⬝* _, refine !passoc ⬝* _, @@ -220,7 +241,7 @@ namespace smash apply pid_pcompose end - definition smash_elim_right_inv {A B C : Type*} (g : A ∧ B →* C) : smash_elim (smash_elim_inv g) ~* g := + definition smash_elim_right_inv (g : A ∧ B →* C) : smash_elim (smash_elim_inv g) ~* g := begin refine !pwhisker_left !smash_functor_pid_pcompose ⬝* _, refine !passoc⁻¹* ⬝* _, @@ -234,38 +255,6 @@ namespace smash smash_elim (pconst B (ppmap A C)) ~* pconst (A ∧ B) C := begin refine pwhisker_left _ (smash_functor_pconst_right (pid A)) ⬝* !pcompose_pconst - -- fconstructor, - -- { intro x, induction x with a b a b, - -- { reflexivity }, - -- { reflexivity }, - -- { reflexivity }, - -- { apply eq_pathover_constant_right, apply hdeg_square, - -- refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ !ap_con ⬝ - -- !ap_compose'⁻¹ ◾ !elim_gluel}, - -- { apply eq_pathover_constant_right, apply hdeg_square, - -- refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ !ap_con ⬝ - -- !ap_compose'⁻¹ ◾ !elim_gluer }}, - -- { reflexivity } - end - - definition pconst_pcompose_pconst (A B C : Type*) : - pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) := - idp - - definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p := - phomotopy_eq (λa, !inv_inv) - begin - induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀, esimp at *, - induction f₀, esimp, - end - - definition pconst_pcompose_phomotopy_pconst {A B C : Type*} {f : A →* B} (p : f ~* pconst A B) : - pconst_pcompose f = pwhisker_left (pconst B C) p ⬝* pcompose_pconst (pconst B C) := - begin - assert H : Π(p : pconst A B ~* f), - pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C), - { intro p, induction p using phomotopy_rec_on_idp, reflexivity }, - refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp, end definition smash_elim_inv_pconst (A B C : Type*) : @@ -274,7 +263,7 @@ namespace smash fapply phomotopy_mk_ppmap, { intro f, apply pconst_pcompose }, { esimp, refine !trans_refl ⬝ _, - refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝ + refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, apply pconst_pcompose_phomotopy_pconst } end @@ -294,18 +283,26 @@ namespace smash exact !ppcompose_left_pcompose⁻¹* end - definition smash_elim_phomotopy {A B C : Type*} {f f' : A →* ppmap B C} + definition smash_elim_natural_left (f : A →* A') (g : B →* B') + (h : B' →* ppmap A' C) : smash_elim h ∘* (f ∧→ g) ~* smash_elim (ppcompose_right f ∘* h ∘* g) := + begin + refine !smash_functor_pid_pcompose ⬝ph* _, + refine _ ⬝v* !smash_pmap_counit_natural_left, + refine smash_functor_psquare (pvrefl f) !pid_pcompose⁻¹* + end + + definition smash_elim_phomotopy {f f' : A →* ppmap B C} (p : f ~* f') : smash_elim f ~* smash_elim f' := begin apply pwhisker_left, exact smash_functor_phomotopy phomotopy.rfl p end - definition smash_elim_inv_phomotopy {A B C : Type*} {f f' : A ∧ B →* C} + definition smash_elim_inv_phomotopy {f f' : A ∧ B →* C} (p : f ~* f') : smash_elim_inv f ~* smash_elim_inv f' := pwhisker_right _ (ppcompose_left_phomotopy p) - definition smash_elim_eq_of_phomotopy {A B C : Type*} {f f' : A →* ppmap B C} + definition smash_elim_eq_of_phomotopy {f f' : A →* ppmap B C} (p : f ~* f') : ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) := begin induction p using phomotopy_rec_on_idp, @@ -316,7 +313,7 @@ namespace smash refine !pwhisker_left_refl⁻¹ end - definition smash_elim_inv_eq_of_phomotopy {A B C : Type*} {f f' : A ∧ B →* C} (p : f ~* f') : + definition smash_elim_inv_eq_of_phomotopy {f f' : A ∧ B →* C} (p : f ~* f') : ap smash_elim_inv (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_inv_phomotopy p) := begin induction p using phomotopy_rec_on_idp, @@ -327,6 +324,7 @@ namespace smash refine !pwhisker_right_refl⁻¹ end + /- The pointed maps of the equivalence A →* (B →* C) ≃* A ∧ B →* C -/ definition smash_pelim [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (B ∧ A) C := pmap.mk smash_elim (eq_of_phomotopy !smash_elim_pconst) @@ -334,7 +332,8 @@ namespace smash ppmap (B ∧ A) C →* ppmap A (ppmap B C) := pmap.mk smash_elim_inv (eq_of_phomotopy !smash_elim_inv_pconst) - theorem smash_elim_natural_pconst {A B C C' : Type*} (f : C →* C') : + /- The forward function is natural in all three arguments -/ + theorem smash_elim_natural_pconst (f : C →* C') : smash_elim_natural f (pconst A (ppmap B C)) ⬝* (smash_elim_phomotopy (pcompose_pconst (ppcompose_left f)) ⬝* smash_elim_pconst B A C') = @@ -344,31 +343,65 @@ namespace smash refine idp ◾** (!trans_assoc⁻¹ ⬝ (!pwhisker_left_trans⁻¹ ◾** idp)) ⬝ _, refine !trans_assoc⁻¹ ⬝ _, refine (!trans_assoc ⬝ (idp ◾** (!pwhisker_left_trans⁻¹ ⬝ - ap (pwhisker_left _) (smash_functor_pconst_right_pid_pcompose' (ppcompose_left f))⁻¹ ⬝ + ap (pwhisker_left _) (smash_functor_pid_pcompose_pconst' (ppcompose_left f))⁻¹ ⬝ !pwhisker_left_trans))) ◾** idp ⬝ _, refine (!trans_assoc⁻¹ ⬝ (!passoc_phomotopy_right⁻¹ʰ** ⬝h** !pwhisker_right_pwhisker_left ⬝h** !passoc_phomotopy_right) ◾** idp) ◾** idp ⬝ _, refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾**_ ⬝ !trans_assoc⁻¹ ⬝ !pwhisker_left_trans⁻¹ ◾** idp, refine !trans_assoc ⬝ !trans_assoc ⬝ (eq_symm_trans_of_trans_eq _)⁻¹, - refine !pcompose_pconst_pcompose⁻¹ ⬝ _, - refine _ ⬝ idp ◾** (!pcompose_pconst_pcompose), + refine !passoc_pconst_right ⬝ _, + refine _ ⬝ idp ◾** !passoc_pconst_right⁻¹, refine !pcompose_pconst_phomotopy⁻¹ end - definition smash_pelim_natural {A B C C' : Type*} (f : C →* C') : + definition smash_pelim_natural (f : C →* C') : ppcompose_left f ∘* smash_pelim A B C ~* smash_pelim A B C' ∘* ppcompose_left (ppcompose_left f) := begin fapply phomotopy_mk_ppmap, { exact smash_elim_natural f }, - { esimp, - refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_elim_eq_of_phomotopy ⬝ + { refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_elim_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , - refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝ + refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, exact smash_elim_natural_pconst f } end + definition smash_pelim_natural_left (C : Type*) (f : A →* A') (g : B →* B') : + psquare (smash_pelim A' B' C) (smash_pelim A B C) + (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (g ∧→ f)) := + begin + fapply phomotopy_mk_ppmap, + { intro h, apply smash_elim_natural_left }, + { esimp, + refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq + (ap02 _ (whisker_right _ !pcompose_left_eq_of_phomotopy ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ + !smash_elim_eq_of_phomotopy) ⬝ !phomotopy_of_eq_of_phomotopy) ◾** + !phomotopy_of_eq_of_phomotopy) ⬝ _, + refine _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾ idp ⬝ + !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, + refine ((idp ⬝h** ((ap (pwhisker_left _) (!trans_assoc⁻¹ ⬝ !pwhisker_left_trans⁻¹ ◾** idp) ⬝ + !pwhisker_left_trans)⁻¹ ⬝ph** (pwhisker_left_phsquare _ + (!smash_functor_phomotopy_trans_right ⬝ph** + (!smash_functor_pid_pcompose_phomotopy_right ⬝v** + !smash_functor_pid_pcompose_pconst))⁻¹ʰ** ⬝vp** !pwhisker_left_symm))) ⬝v** + (phwhisker_rt _ idp)) ⬝ _, + refine (idp ⬝h** (!passoc_phomotopy_right ⬝v** idp)) ◾** idp ⬝ _, + refine !trans_assoc ⬝ idp ◾** (!trans_assoc ⬝ !trans_assoc ⬝ idp ◾** + !passoc_pconst_right) ⬝ _, + refine idp ⬝h** (phwhisker_br _ !pwhisker_right_pwhisker_left ⬝vp** + !pcompose_pconst_phomotopy) ⬝ _, + refine (idp ⬝h** (phwhisker_br _ !passoc_phomotopy_right⁻¹ʰ** ⬝vp** + (eq_symm_trans_of_trans_eq !passoc_pconst_right)⁻¹)) ⬝ _, + refine (idp ⬝h** ((idp ◾** !pwhisker_left_trans⁻¹ ⬝ + pwhisker_left_phsquare _ !smash_psquare_lemma) ⬝v** idp ⬝hp** !trans_assoc)) ⬝ _, + refine (!passoc_phomotopy_middle ⬝v** idp ⬝v** idp) ⬝ _, + refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** !passoc_pconst_middle ⬝ _, + refine !trans_assoc⁻¹ ⬝ _ ◾** idp, + exact !pwhisker_right_trans⁻¹ } + end + + /- The equivalence (note: the forward function of smash_adjoint_pmap is smash_pelim_inv) -/ definition smash_adjoint_pmap' [constructor] (A B C : Type*) : B →* ppmap A C ≃ A ∧ B →* C := begin fapply equiv.MK, @@ -386,6 +419,7 @@ namespace smash ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) := (smash_adjoint_pmap_inv A B C)⁻¹ᵉ* + /- The naturality of the equivalence is a direct consequence of the earlier naturalities -/ definition smash_adjoint_pmap_natural_pt {A B C C' : Type*} (f : C →* C') (g : A ∧ B →* C) : ppcompose_left f ∘* smash_adjoint_pmap A B C g ~* smash_adjoint_pmap A B C' (f ∘* g) := begin @@ -412,7 +446,12 @@ namespace smash smash_adjoint_pmap A B C' ∘* ppcompose_left f := (smash_adjoint_pmap_inv_natural f)⁻¹ʰ* - /- associativity of smash -/ + definition smash_adjoint_pmap_natural_left (C : Type*) (f : A →* A') (g : B →* B') : + psquare (smash_adjoint_pmap A' B' C) (smash_adjoint_pmap A B C) + (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right f) ∘* ppcompose_right g) := + (smash_pelim_natural_left C g f)⁻¹ʰ* + + /- Corollary: associativity of smash -/ definition smash_assoc_elim_equiv (A B C X : Type*) : ppmap (A ∧ (B ∧ C)) X ≃* ppmap ((A ∧ B) ∧ C) X := @@ -426,6 +465,18 @@ namespace smash (A ∧ B) ∧ C →* X := smash_elim (ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ* (smash_elim_inv (smash_elim_inv f))) + definition smash_assoc_elim_natural (A B C : Type*) (f : X →* X') : + psquare (smash_assoc_elim_equiv A B C X) (smash_assoc_elim_equiv A B C X') + (ppcompose_left f) (ppcompose_left f) := + !smash_adjoint_pmap_natural ⬝h* + !smash_adjoint_pmap_natural ⬝h* + ppcompose_left_psquare !smash_adjoint_pmap_inv_natural ⬝h* + !smash_adjoint_pmap_inv_natural + + /- + We could prove the following two pointed homotopies by applying smash_assoc_elim_natural to g, + but we give a more explicit proof + -/ definition smash_assoc_elim_natural_pt {A B C X X' : Type*} (f : X →* X') (g : A ∧ (B ∧ C) →* X) : f ∘* smash_assoc_elim_equiv A B C X g ~* smash_assoc_elim_equiv A B C X' (f ∘* g) := begin @@ -459,7 +510,6 @@ namespace smash apply smash_elim_inv_natural end - -- TODO: maybe do it without pap / phomotopy_of_eq definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C := begin fapply pequiv.MK2, @@ -473,6 +523,30 @@ namespace smash apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_equiv } end - print axioms smash_assoc + /- the associativity of smash is natural in all arguments -/ + definition smash_assoc_elim_equiv_natural_left (X : Type*) + (f : A →* A') (g : B →* B') (h : C →* C') : + psquare (smash_assoc_elim_equiv A' B' C' X) (smash_assoc_elim_equiv A B C X) + (ppcompose_right (f ∧→ g ∧→ h)) (ppcompose_right ((f ∧→ g) ∧→ h)) := + begin + refine !smash_adjoint_pmap_natural_left ⬝h* _ ⬝h* + (!ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare !smash_pelim_natural_left) ⬝h* + !smash_pelim_natural_left, + refine !ppcompose_left_ppcompose_right⁻¹* ⬝ph* _, + refine _ ⬝hp* pwhisker_right _ (ppcompose_left_phomotopy !ppcompose_left_ppcompose_right⁻¹* ⬝* + !ppcompose_left_pcompose) ⬝* !passoc ⬝* pwhisker_left _ !ppcompose_left_ppcompose_right⁻¹* ⬝* + !passoc⁻¹*, + refine _ ⬝v* !smash_adjoint_pmap_natural_left, + refine !smash_adjoint_pmap_natural + end + + definition smash_assoc_natural (f : A →* A') (g : B →* B') (h : C →* C') : + psquare (smash_assoc A B C) (smash_assoc A' B' C') (f ∧→ (g ∧→ h)) ((f ∧→ g) ∧→ h) := + begin + refine !smash_assoc_elim_inv_natural_pt ⬝* _, + refine pap !smash_assoc_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _, + rexact phomotopy_of_eq ((smash_assoc_elim_equiv_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹ + end + end smash diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 90bb71a..a8492f8 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -5,7 +5,7 @@ Authors: Michael Shulman, Floris van Doorn -/ -import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim ..pointed_pi +import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..colim ..pointed open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group seq_colim succ_str diff --git a/homotopy/temp2.hlean b/homotopy/temp2.hlean new file mode 100644 index 0000000..5569161 --- /dev/null +++ b/homotopy/temp2.hlean @@ -0,0 +1,123 @@ + +import .smash_adjoint + +open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc + function red_susp unit smash + +variables {A A' B B' C C' D E F X X' : Type*} + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +-- definition concat2o {A B : Type} {f g h : A → B} {a₁ a₂ : A} {p₁ : f a₁ = g a₁} {p₂ : f a₂ = g a₂} +-- {q₁ : g a₁ = h a₁} {q₂ : g a₂ = h a₂} {r : a₁ = a₂} (s₁ : p₁ =[r] p₂) (s₂ : q₁ =[r] q₂) : +-- p₁ ⬝ q₁ =[r] p₂ ⬝ q₂ := +-- apo011 (λx, concat) s₁ s₂ + +-- infixl ` ◾o' `:75 := concat2o + +-- definition apd_con_fn {A B : Type} {f g h : A → B} {a₁ a₂ : A} (p : f ~ g) (q : g ~ h) (r : a₁ = a₂) +-- : apd (λa, p a ⬝ q a) r = apd p r ◾o' apd q r := +-- begin +-- induction r, reflexivity +-- end + +-- definition ap02o {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) {a₁ a₂ : A} {p₁ : g a₁ = h a₁} +-- {p₂ : g a₂ = h a₂} {q : a₁ = a₂} (r : p₁ =[q] p₂) : ap (f a₁) p₁ =[q] ap (f a₂) p₂ := +-- apo (λx, ap (f x)) r + +-- definition apo_eq_pathover {A A' B B' : Type} {a a' : A} {f g : A → B} {i : A → A'} {f' g' : A' → B'} +-- {p : a = a'} {q : f a = g a} (h : Πa, f a = g a → f' (i a) = g' (i a)) +-- {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) : +-- apo h (eq_pathover s) = eq_pathover _ := +-- sorry + +-- definition ap02o_eq_pathover {A A' B B' : Type} {a a' : A} {f g : A → B} {i : A → A'} {f' g' : A' → B'} +-- {p : a = a'} {q : f a = g a} (h : Πa, f a = g a → f' (i a) = g' (i a)) +-- {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) : +-- apo h (eq_pathover s) = eq_pathover _ := +-- sorry + +-- definition apd_ap_fn {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) (p : g ~ h) +-- {a₁ a₂ : A} (r : a₁ = a₂) : apd (λa, ap (f a) (p a)) r = ap02o f (apd p r) := +-- begin +-- induction r; reflexivity +-- end + +-- definition apd_ap_fn {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) (p : g ~ h) +-- {a₁ a₂ : A} (r : a₁ = a₂) : apd (λa, ap (f a) (p a)) r = ap02o f (apd p r) := diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 4ae0e6f..b50f404 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -53,13 +53,23 @@ section -- squares 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 = + -- should the following two equalities be cubes? + 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_compose {A B C : Type} {a a' : A} {g g' : B → C} + (p : g ~ g') (f : A → B) (q : a = a') : natural_square (λa, p (f a)) q = + ap_compose g f q ⬝ph (natural_square p (ap f q) ⬝hp (ap_compose g' f q)⁻¹) := + by induction q; reflexivity + + definition natural_square_eq2 {A B : Type} {a a' : A} {f f' : A → B} (p : f ~ f') {q q' : a = a'} + (r : q = q') : natural_square p q = ap02 f r ⬝ph (natural_square p q' ⬝hp (ap02 f' r)⁻¹) := + by induction r; reflexivity + 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 @@ -143,6 +153,21 @@ section -- cubes end + definition ap_eq_ap010 {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') (b : B) : + ap (λa, f a b) p = ap010 f p b := + by reflexivity + + definition ap011_idp {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') (b : B) : + ap011 f p idp = ap010 f p b := + by reflexivity + + definition ap011_flip {A B C : Type} (f : A → B → C) {a a' : A} {b b' : B} (p : a = a') (q : b = b') : + ap011 f p q = ap011 (λb a, f a b) q p := + by induction q; induction p; reflexivity + + theorem apd_constant' {A A' : Type} {B : A' → Type} {a₁ a₂ : A} {a' : A'} (b : B a') + (p : a₁ = a₂) : apd (λx, b) p = pathover_of_eq p idp := + by induction p; reflexivity 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') : @@ -261,13 +286,13 @@ end definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ := p - definition hhcompose (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : + 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 hvcompose (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) : + definition hvconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) : hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) := - (hhcompose p⁻¹ʰᵗʸ q⁻¹ʰᵗʸ)⁻¹ʰᵗʸ + (hhconcat p⁻¹ʰᵗʸ q⁻¹ʰᵗʸ)⁻¹ʰᵗʸ definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ := @@ -277,8 +302,8 @@ end hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ := (hhinverse p⁻¹ʰᵗʸ)⁻¹ʰᵗʸ - infix ` ⬝htyh `:73 := hhcompose - infix ` ⬝htyv `:73 := hvcompose + infix ` ⬝htyh `:73 := hhconcat + infix ` ⬝htyv `:73 := hvconcat postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse @@ -291,11 +316,19 @@ end induction p using homotopy.rec_on, induction q, exact H end - --eq2 + --eq2 (duplicate of ap_compose_ap02_constant) 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 + definition ap_constant_compose {A B C : Type} {a a' : A} (c : C) (f : A → B) (p : a = a') : + square (ap_constant p c) (ap_constant (ap f p) c) (ap_compose (λx, c) f p) idp := + by induction p; exact ids + + definition ap02_constant {A B : Type} {a a' : A} (b : B) {p p' : a = a'} + (q : p = p') : square (ap_constant p b) (ap_constant p' b) (ap02 (λx, b) q) idp := + by induction q; exact vrfl + end eq open eq namespace wedge @@ -313,540 +346,6 @@ namespace pi 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' := - pwhisker_right f q ⬝* pwhisker_left g' p - - infixr ` ◾*' `:80 := pcompose2' - - definition phomotopy_of_homotopy {X Y : Type*} {f g : X →* Y} (h : f ~ g) [is_set Y] : f ~* g := - begin - fapply phomotopy.mk, - { exact h }, - { apply is_set.elim } - end - - definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B} - {f : A → b₀ = b₁} {f' : A → b₁ = b₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂} - (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') : - ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') = - whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') := - begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end - - definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B} - {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂} - (r₀ : f a = q₀) (r₁ : f' a = q₁) : - ap1_gen_con_left idp r₀ r₀ r₁ r₁ = - !con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ := - begin induction r₀, induction r₁, reflexivity end - - -- /- the pointed type of (unpointed) dependent maps -/ - -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* := - -- pointed.mk' (Πa, P a) - - -- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) := - -- pequiv_of_equiv eq_equiv_homotopy rfl - - -- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a) - -- : pupi P ≃* pupi Q := - -- pequiv_of_equiv (pi_equiv_pi_right g) - -- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) 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₄₄ : 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 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 phcompose (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 pvcompose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : - psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) := - (phcompose p⁻¹* q⁻¹*)⁻¹* - - 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⁻¹*)⁻¹* - - infix ` ⬝h* `:73 := phcompose - infix ` ⬝v* `:73 := pvcompose - postfix `⁻¹ʰ*`:(max+1) := phinverse - postfix `⁻¹ᵛ*`:(max+1) := pvinverse - - 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 phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : - phomotopy_of_eq (eq_of_phomotopy p) = p := - to_right_inv (pmap_eq_equiv f g) p - - definition ap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : - ap (λf : A →* B, f a) (eq_of_phomotopy p) = p a := - ap010 to_homotopy (phomotopy_of_eq_of_phomotopy p) a - - definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B} - {Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p := - phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p) - - definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B} - {Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p := - begin - induction p using phomotopy_rec_on_eq, - induction q, exact H - end - - definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B} - {Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : - phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p := - begin - unfold phomotopy_rec_on_eq, - refine ap (λp, p ▸ _) !adj ⬝ _, - refine !tr_compose⁻¹ ⬝ _, - apply apdt - end - - definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B) - {Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) : - phomotopy_rec_on_idp phomotopy.rfl H = H := - !phomotopy_rec_on_eq_phomotopy_of_eq - - definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) : - (h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k), - whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h := - calc - h = k ≃ phomotopy.sigma_char _ _ h = phomotopy.sigma_char _ _ k - : eq_equiv_fn_eq (phomotopy.sigma_char f g) h k - ... ≃ Σ(p : to_homotopy h = to_homotopy k), - pathover (λp, p pt ⬝ respect_pt g = respect_pt f) (to_homotopy_pt h) p (to_homotopy_pt k) - : sigma_eq_equiv _ _ - ... ≃ Σ(p : to_homotopy h = to_homotopy k), - to_homotopy_pt h = ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k - : sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (to_homotopy_pt h) (to_homotopy_pt k)) - ... ≃ Σ(p : to_homotopy h = to_homotopy k), - ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k = to_homotopy_pt h - : 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⁻¹)) - ... ≃ Σ(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 - - definition phomotopy_eq {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) - (q : whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h) : h = k := - to_inv (phomotopy_eq_equiv h k) ⟨p, q⟩ - - definition phomotopy_eq' {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) - (q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k := - phomotopy_eq p (eq_of_square q)⁻¹ - - definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) : - eq_of_phomotopy (phomotopy.refl f) = idpath f := - begin - apply to_inv_eq_of_eq, reflexivity - end - - definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p := - begin - induction A with A a₀, induction B with B b₀, - induction f with f f₀, induction g with g g₀, induction p with p p₀, - esimp at *, induction g₀, induction p₀, - reflexivity - end - - definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p := - begin - induction p using phomotopy_rec_on_idp, - induction A with A a₀, induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, - reflexivity - end - - definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h) - (r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) := - begin - induction r using phomotopy_rec_on_idp, - induction q using phomotopy_rec_on_idp, - induction p using phomotopy_rec_on_idp, - induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, - reflexivity - end - - definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f := - begin - induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, - reflexivity - end - - definition trans_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl := - begin - induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm - end - - definition symm_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl := - begin - induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm - end - - definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h} - (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' := - ap011 phomotopy.trans r s - - infixl ` ◾** `:80 := pointed.trans2 - - definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h} - (s : q = q') : p ⬝* q = p ⬝* q' := - idp ◾** s - - definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h) - (r : p = p') : p ⬝* q = p' ⬝* q := - r ◾** idp - - definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) : - pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, - induction f with f f₀, induction g with g g₀, - esimp at *, induction g₀, induction f₀, reflexivity - end - - definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) : - pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, - induction f with f f₀, induction g with g g₀, - esimp at *, induction g₀, induction f₀, reflexivity - end - - definition pwhisker_left_trans {A B C : Type*} (g : B →* C) {f₁ f₂ f₃ : A →* B} - (p : f₁ ~* f₂) (q : f₂ ~* f₃) : - pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q := - begin - induction p using phomotopy_rec_on_idp, - induction q using phomotopy_rec_on_idp, - refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹, - refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹ - end - - definition pwhisker_right_trans {A B C : Type*} (f : A →* B) {g₁ g₂ g₃ : B →* C} - (p : g₁ ~* g₂) (q : g₂ ~* g₃) : - pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q := - begin - induction p using phomotopy_rec_on_idp, - induction q using phomotopy_rec_on_idp, - refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹, - refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹ - end - - definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r := - idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_symm p ◾** idp ⬝ !refl_trans - - definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r := - !refl_trans⁻¹ ⬝ !symm_trans⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s - - definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r := - s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** symm_trans q ⬝ !trans_refl - - definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* := - !trans_refl⁻¹ ⬝ idp ◾** !trans_symm⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp - - section phsquare - /- - Squares of pointed homotopies - -/ - - variables {A B : Type*} {f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B} - {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀} - {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂} - {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂} - {p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄} - {p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄} - - definition phsquare [reducible] (p₁₀ : f₀₀ ~* f₂₀) (p₁₂ : f₀₂ ~* f₂₂) - (p₀₁ : f₀₀ ~* f₀₂) (p₂₁ : f₂₀ ~* f₂₂) : Type := - p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ - - definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p - definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p - - definition phhcompose (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) : - phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ := - !trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc - - definition phvcompose (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₁₂ p₁₄ p₀₃ p₂₃) : - phsquare p₁₀ p₁₄ (p₀₁ ⬝* p₀₃) (p₂₁ ⬝* p₂₃) := - (phhcompose p⁻¹ q⁻¹)⁻¹ - - /- - The names are very baroque. The following stands for - "pointed homotopy path-horizontal composition" (i.e. composition on the left with a path) - The names are obtained by using the ones for squares, and putting "ph" in front of it. - In practice, use the notation ⬝ph** defined below, which might be easier to remember - -/ - definition phphcompose {p₀₁'} (p : p₀₁' = p₀₁) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : - phsquare p₁₀ p₁₂ p₀₁' p₂₁ := - by induction p; exact q - - definition phhpcompose {p₂₁'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₂₁ = p₂₁') : - phsquare p₁₀ p₁₂ p₀₁ p₂₁' := - by induction p; exact q - - definition phpvcompose {p₁₀'} (p : p₁₀' = p₁₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : - phsquare p₁₀' p₁₂ p₀₁ p₂₁ := - by induction p; exact q - - definition phvpcompose {p₁₂'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₁₂ = p₁₂') : - phsquare p₁₀ p₁₂' p₀₁ p₂₁ := - by induction p; exact q - - definition phhinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₀⁻¹* p₁₂⁻¹* p₂₁ p₀₁ := - begin - refine (eq_symm_trans_of_trans_eq _)⁻¹, - refine !trans_assoc⁻¹ ⬝ _, - refine (eq_trans_symm_of_trans_eq _)⁻¹, - exact (eq_of_phsquare p)⁻¹ - end - - definition phvinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₂ p₁₀ p₀₁⁻¹* p₂₁⁻¹* := - (phhinverse p⁻¹)⁻¹ - - infix ` ⬝h** `:71 := phhcompose - infix ` ⬝v** `:72 := phvcompose - infix ` ⬝ph** `:73 := phphcompose - infix ` ⬝hp** `:73 := phhpcompose - infix ` ⬝pv** `:73 := phpvcompose - infix ` ⬝vp** `:73 := phvpcompose - postfix `⁻¹ʰ**`:(max+1) := phhinverse - postfix `⁻¹ᵛ**`:(max+1) := phvinverse - - definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B} - (p : f ~* f') : phsquare (passoc h g f) (passoc h g f') - (pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) := - begin - induction p using phomotopy_rec_on_idp, - refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝ - !pwhisker_left_refl⁻¹ ◾** idp, - exact !trans_refl ⬝ !refl_trans⁻¹ - end - - definition pwhisker_right_pwhisker_left {A B C : Type*} {g g' : B →* C} {f f' : A →* B} - (p : g ~* g') (q : f ~* f') : - phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) := - begin - induction p using phomotopy_rec_on_idp, - induction q using phomotopy_rec_on_idp, - exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ - !pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹ - end - - end phsquare - - definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) : - phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q := - begin induction q, induction p, exact !trans_refl⁻¹ end - - definition pcompose_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B} (H : f ~* f') : - ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) := - begin - induction H using phomotopy_rec_on_idp, - refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, - exact !pwhisker_left_refl⁻¹ - end - - definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B) - : respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g := - idp - - definition phomotopy_mk_ppmap [constructor] {A B C : Type*} {f g : A →* ppmap B C} (p : Πa, f a ~* g a) - (q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f)) - : f ~* g := - begin - apply phomotopy.mk (λa, eq_of_phomotopy (p a)), - apply eq_of_fn_eq_fn (pmap_eq_equiv _ _), esimp [pmap_eq_equiv], - refine !phomotopy_of_eq_con ⬝ _, - refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q, - end - - definition pcompose_pconst_pcompose {A B C D : Type*} (h : C →* D) (g : B →* C) : - pcompose_pconst (h ∘* g) = - passoc h g (pconst A B) ⬝* (pwhisker_left h (pcompose_pconst g) ⬝* pcompose_pconst h) := - begin - fapply phomotopy_eq, - { intro a, exact !idp_con⁻¹ }, - { induction h with h h₀, induction g with g g₀, induction D with D d₀, induction C with C c₀, - esimp at *, induction g₀, induction h₀, reflexivity } - end - - definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) : - @ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g := - begin - fapply phomotopy_mk_ppmap, - { exact passoc h g }, - { esimp, - refine idp ◾** (!phomotopy_of_eq_con ⬝ ap011 phomotopy.trans - (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) - !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, - exact (pcompose_pconst_pcompose h g)⁻¹ } - end - - definition pcompose_pconst_phomotopy {A B C : Type*} {f f' : B →* C} (p : f ~* f') : - pwhisker_right (pconst A B) p ⬝* pcompose_pconst f' = pcompose_pconst f := - begin - fapply phomotopy_eq, - { intro a, exact to_homotopy_pt p }, - { induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀, - esimp at *, induction f₀, reflexivity } - end - - definition ppcompose_left_pconst [constructor] (A B C : Type*) : - @ppcompose_left A _ _ (pconst B C) ~* pconst (ppmap A B) (ppmap A C) := - begin - fapply phomotopy_mk_ppmap, - { exact pconst_pcompose }, - { refine idp ◾** !phomotopy_of_eq_idp ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ } - end - - definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') : - @ppcompose_left A _ _ g ~* ppcompose_left g' := - begin - induction p using phomotopy_rec_on_idp, - reflexivity - end - /- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it - -/ - -- fapply phomotopy_mk_ppmap, - -- { intro f, exact pwhisker_right f p }, - -- { refine ap (λx, _ ⬝* x) !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, - -- exact pcompose_pconst_phomotopy p } - - definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) : - ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) := - !phomotopy_rec_on_idp_refl - - -- definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) := - -- begin - -- refine eq_equiv_fn_eq_of_equiv (@pmap.sigma_char X Y) f g ⬝e _, - -- refine !sigma_eq_equiv ⬝e _, - -- refine _ ⬝e (phomotopy.sigma_char f g)⁻¹ᵉ, - -- fapply sigma_equiv_sigma, - -- { esimp, apply eq_equiv_homotopy }, - -- { induction g with g gp, induction Y with Y y0, esimp, intro p, induction p, esimp at *, - -- refine !pathover_idp ⬝e _, refine _ ⬝e !eq_equiv_eq_symm, - -- apply equiv_eq_closed_right, exact !idp_con⁻¹ } - -- end - - definition pmap_eq_idp {X Y : Type*} (f : X →* Y) : - pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f := - ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f - - definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := - begin - fapply pequiv_of_equiv, - { fapply equiv.MK: esimp, - { intro f, fapply pmap_eq, - { intro x, exact f x }, - { exact (respect_pt f)⁻¹ }}, - { intro p, fapply pmap.mk, - { intro x, exact ap010 pmap.to_fun p x }, - { note z := apd respect_pt p, - note z2 := square_of_pathover z, - refine eq_of_hdeg_square z2 ⬝ !ap_constant }}, - { intro p, exact sorry }, - { intro p, exact sorry }}, - { apply pmap_eq_idp} - end - -end pointed open pointed - namespace trunc -- TODO: redefine loopn_ptrunc_pequiv @@ -964,6 +463,17 @@ namespace sigma end sigma open sigma +namespace pointed + + definition phomotopy_of_homotopy {X Y : Type*} {f g : X →* Y} (h : f ~ g) [is_set Y] : f ~* g := + begin + fapply phomotopy.mk, + { exact h }, + { apply is_set.elim } + end + +end pointed open pointed + namespace group open is_trunc @@ -1137,6 +647,15 @@ namespace circle exact to_right_inv !eq_pathover_equiv_square q end + definition circle_elim_constant [unfold 5] {A : Type} {a : A} {p : a = a} (r : p = idp) (x : S¹) : + circle.elim a p x = a := + begin + induction x, + { reflexivity }, + { apply eq_pathover_constant_right, apply hdeg_square, exact !elim_loop ⬝ r } + end + + end circle diff --git a/pointed.hlean b/pointed.hlean new file mode 100644 index 0000000..784bf17 --- /dev/null +++ b/pointed.hlean @@ -0,0 +1,828 @@ +/- equalities between pointed homotopies -/ + +-- Author: Floris van Doorn + +--import .pointed_pi + +import .move_to_lib + +open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra group sigma + +namespace pointed + + 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 + + definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B} + {f : A → b₀ = b₁} {f' : A → b₁ = b₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂} + (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') : + ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') = + whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') := + begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end + + definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B} + {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂} + (r₀ : f a = q₀) (r₁ : f' a = q₁) : + ap1_gen_con_left idp r₀ r₀ r₁ r₁ = + !con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ := + begin induction r₀, induction r₁, reflexivity end + + -- /- the pointed type of (unpointed) dependent maps -/ + -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* := + -- pointed.mk' (Πa, P a) + + -- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) := + -- pequiv_of_equiv eq_equiv_homotopy rfl + + -- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a) + -- : pupi P ≃* pupi Q := + -- pequiv_of_equiv (pi_equiv_pi_right g) + -- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) 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₂₄ 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 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 phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : + phomotopy_of_eq (eq_of_phomotopy p) = p := + to_right_inv (pmap_eq_equiv f g) p + + definition ap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : + ap (λf : A →* B, f a) (eq_of_phomotopy p) = p a := + ap010 to_homotopy (phomotopy_of_eq_of_phomotopy p) a + + definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B} + {Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p := + phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p) + + definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B} + {Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p := + begin + induction p using phomotopy_rec_on_eq, + induction q, exact H + end + + definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B} + {Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : + phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p := + begin + unfold phomotopy_rec_on_eq, + refine ap (λp, p ▸ _) !adj ⬝ _, + refine !tr_compose⁻¹ ⬝ _, + apply apdt + end + + definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B) + {Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) : + phomotopy_rec_on_idp phomotopy.rfl H = H := + !phomotopy_rec_on_eq_phomotopy_of_eq + + definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) : + (h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k), + whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h := + calc + h = k ≃ phomotopy.sigma_char _ _ h = phomotopy.sigma_char _ _ k + : eq_equiv_fn_eq (phomotopy.sigma_char f g) h k + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + pathover (λp, p pt ⬝ respect_pt g = respect_pt f) (to_homotopy_pt h) p (to_homotopy_pt k) + : sigma_eq_equiv _ _ + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + to_homotopy_pt h = ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k + : sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (to_homotopy_pt h) (to_homotopy_pt k)) + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k = to_homotopy_pt h + : 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⁻¹)) + ... ≃ Σ(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 + + definition phomotopy_eq {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) + (q : whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h) : h = k := + to_inv (phomotopy_eq_equiv h k) ⟨p, q⟩ + + definition phomotopy_eq' {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) + (q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k := + phomotopy_eq p (eq_of_square q)⁻¹ + + definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) : + eq_of_phomotopy (phomotopy.refl f) = idpath f := + begin + apply to_inv_eq_of_eq, reflexivity + end + + definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p := + begin + induction A with A a₀, induction B with B b₀, + induction f with f f₀, induction g with g g₀, induction p with p p₀, + esimp at *, induction g₀, induction p₀, + reflexivity + end + + definition eq_of_phomotopy_trans {X Y : Type*} {f g h : X →* Y} (p : f ~* g) (q : g ~* h) : + eq_of_phomotopy (p ⬝* q) = eq_of_phomotopy p ⬝ eq_of_phomotopy q := + begin + induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp, + exact ap eq_of_phomotopy !trans_refl ⬝ whisker_left _ !eq_of_phomotopy_refl⁻¹ + end + + definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p := + begin + induction p using phomotopy_rec_on_idp, + induction A with A a₀, induction B with B b₀, + induction f with f f₀, esimp at *, induction f₀, + reflexivity + end + + definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h) + (r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) := + begin + induction r using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + induction p using phomotopy_rec_on_idp, + induction B with B b₀, + induction f with f f₀, esimp at *, induction f₀, + reflexivity + end + + definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f := + begin + induction B with B b₀, + induction f with f f₀, esimp at *, induction f₀, + reflexivity + end + + definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p := + phomotopy_eq (λa, !inv_inv) + begin + induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀, + esimp at *, induction f₀, reflexivity + end + + definition trans_right_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl := + begin + induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm + end + + definition trans_left_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl := + begin + induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm + end + + definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h} + (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' := + ap011 phomotopy.trans r s + + definition pcompose3 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} + {p p' : g ~* g'} {q q' : f ~* f'} (r : p = p') (s : q = q') : p ◾* q = p' ◾* q' := + ap011 pcompose2 r s + + definition symm2 {A B : Type*} {f g : A →* B} {p p' : f ~* g} (r : p = p') : p⁻¹* = p'⁻¹* := + ap phomotopy.symm r + + infixl ` ◾** `:80 := pointed.trans2 + infixl ` ◽* `:81 := pointed.pcompose3 + postfix `⁻²**`:(max+1) := pointed.symm2 + + definition trans_symm {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g ~* h) : + (p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* := + begin + induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp, + exact !trans_refl⁻²** ⬝ !trans_refl⁻¹ ⬝ idp ◾** !refl_symm⁻¹ + end + + definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h} + (s : q = q') : p ⬝* q = p ⬝* q' := + idp ◾** s + + definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h) + (r : p = p') : p ⬝* q = p' ⬝* q := + r ◾** idp + + definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) : + pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, + induction f with f f₀, induction g with g g₀, + esimp at *, induction g₀, induction f₀, reflexivity + end + + definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) : + pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, + induction f with f f₀, induction g with g g₀, + esimp at *, induction g₀, induction f₀, reflexivity + end + + definition pcompose2_refl {A B C : Type*} (g : B →* C) (f : A →* B) : + phomotopy.refl g ◾* phomotopy.refl f = phomotopy.rfl := + !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ !refl_trans + + definition pcompose2_refl_left {A B C : Type*} (g : B →* C) {f f' : A →* B} (p : f ~* f') : + phomotopy.rfl ◾* p = pwhisker_left g p := + !pwhisker_right_refl ◾** idp ⬝ !refl_trans + + definition pcompose2_refl_right {A B C : Type*} {g g' : B →* C} (f : A →* B) (p : g ~* g') : + p ◾* phomotopy.rfl = pwhisker_right f p := + idp ◾** !pwhisker_left_refl ⬝ !trans_refl + + definition pwhisker_left_trans {A B C : Type*} (g : B →* C) {f₁ f₂ f₃ : A →* B} + (p : f₁ ~* f₂) (q : f₂ ~* f₃) : + pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹, + refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹ + end + + definition pwhisker_right_trans {A B C : Type*} (f : A →* B) {g₁ g₂ g₃ : B →* C} + (p : g₁ ~* g₂) (q : g₂ ~* g₃) : + pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹, + refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹ + end + + definition pwhisker_left_symm {A B C : Type*} (g : B →* C) {f₁ f₂ : A →* B} (p : f₁ ~* f₂) : + pwhisker_left g p⁻¹* = (pwhisker_left g p)⁻¹* := + begin + induction p using phomotopy_rec_on_idp, + refine _ ⬝ ap phomotopy.symm !pwhisker_left_refl⁻¹, + refine ap (pwhisker_left g) !refl_symm ⬝ !pwhisker_left_refl ⬝ !refl_symm⁻¹ + end + + definition pwhisker_right_symm {A B C : Type*} (f : A →* B) {g₁ g₂ : B →* C} (p : g₁ ~* g₂) : + pwhisker_right f p⁻¹* = (pwhisker_right f p)⁻¹* := + begin + induction p using phomotopy_rec_on_idp, + refine _ ⬝ ap phomotopy.symm !pwhisker_right_refl⁻¹, + refine ap (pwhisker_right f) !refl_symm ⬝ !pwhisker_right_refl ⬝ !refl_symm⁻¹ + end + + definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r := + idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_right_inv p ◾** idp ⬝ !refl_trans + + definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r := + !refl_trans⁻¹ ⬝ !trans_left_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s + + definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r := + s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_left_inv q ⬝ !trans_refl + + definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* := + !trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp + + section phsquare + /- + Squares of pointed homotopies + -/ + + variables {A B C : Type*} {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B} + {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀} + {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂} + {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂} + {p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄} + {p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄} + + definition phsquare [reducible] (p₁₀ : f₀₀ ~* f₂₀) (p₁₂ : f₀₂ ~* f₂₂) + (p₀₁ : f₀₀ ~* f₀₂) (p₂₁ : f₂₀ ~* f₂₂) : Type := + p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ + + definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p + definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p + + definition phhconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) : + phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ := + !trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc + + definition phvconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₁₂ p₁₄ p₀₃ p₂₃) : + phsquare p₁₀ p₁₄ (p₀₁ ⬝* p₀₃) (p₂₁ ⬝* p₂₃) := + (phhconcat p⁻¹ q⁻¹)⁻¹ + + definition phhdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare phomotopy.rfl phomotopy.rfl p₁ p₂ := + !refl_trans ⬝ q⁻¹ ⬝ !trans_refl⁻¹ + definition phvdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare p₁ p₂ phomotopy.rfl phomotopy.rfl := + !trans_refl ⬝ q ⬝ !refl_trans⁻¹ + + variables (p₀₁ p₁₀) + definition phhrefl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhdeg_square idp + definition phvrefl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvdeg_square idp + variables {p₀₁ p₁₀} + definition phhrfl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhrefl p₀₁ + definition phvrfl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvrefl p₁₀ + + /- + The names are very baroque. The following stands for + "pointed homotopy path-horizontal composition" (i.e. composition on the left with a path) + The names are obtained by using the ones for squares, and putting "ph" in front of it. + In practice, use the notation ⬝ph** defined below, which might be easier to remember + -/ + definition phphconcat {p₀₁'} (p : p₀₁' = p₀₁) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare p₁₀ p₁₂ p₀₁' p₂₁ := + by induction p; exact q + + definition phhpconcat {p₂₁'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₂₁ = p₂₁') : + phsquare p₁₀ p₁₂ p₀₁ p₂₁' := + by induction p; exact q + + definition phpvconcat {p₁₀'} (p : p₁₀' = p₁₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare p₁₀' p₁₂ p₀₁ p₂₁ := + by induction p; exact q + + definition phvpconcat {p₁₂'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₁₂ = p₁₂') : + phsquare p₁₀ p₁₂' p₀₁ p₂₁ := + by induction p; exact q + + definition phhinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₀⁻¹* p₁₂⁻¹* p₂₁ p₀₁ := + begin + refine (eq_symm_trans_of_trans_eq _)⁻¹, + refine !trans_assoc⁻¹ ⬝ _, + refine (eq_trans_symm_of_trans_eq _)⁻¹, + exact (eq_of_phsquare p)⁻¹ + end + + definition phvinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₂ p₁₀ p₀₁⁻¹* p₂₁⁻¹* := + (phhinverse p⁻¹)⁻¹ + + infix ` ⬝h** `:78 := phhconcat + infix ` ⬝v** `:78 := phvconcat + infixr ` ⬝ph** `:77 := phphconcat + infixl ` ⬝hp** `:77 := phhpconcat + infixr ` ⬝pv** `:77 := phpvconcat + infixl ` ⬝vp** `:77 := phvpconcat + postfix `⁻¹ʰ**`:(max+1) := phhinverse + postfix `⁻¹ᵛ**`:(max+1) := phvinverse + + definition phwhisker_rt (p : f ~* f₂₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare (p₁₀ ⬝* p⁻¹*) p₁₂ p₀₁ (p ⬝* p₂₁) := + !trans_assoc ⬝ idp ◾** (!trans_assoc⁻¹ ⬝ !trans_left_inv ◾** idp ⬝ !refl_trans) ⬝ q + + definition phwhisker_br (p : f₂₂ ~* f) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare p₁₀ (p₁₂ ⬝* p) p₀₁ (p₂₁ ⬝* p) := + !trans_assoc⁻¹ ⬝ q ◾** idp ⬝ !trans_assoc + + definition phmove_top_of_left' {p₀₁ : f ~* f₀₂} (p : f₀₀ ~* f) + (q : phsquare p₁₀ p₁₂ (p ⬝* p₀₁) p₂₁) : phsquare (p⁻¹* ⬝* p₁₀) p₁₂ p₀₁ p₂₁ := + !trans_assoc ⬝ (eq_symm_trans_of_trans_eq (q ⬝ !trans_assoc)⁻¹)⁻¹ + + definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B} + (p : f ~* f') : phsquare (passoc h g f) (passoc h g f') + (pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) := + begin + induction p using phomotopy_rec_on_idp, + refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝ + !pwhisker_left_refl⁻¹ ◾** idp, + exact !trans_refl ⬝ !refl_trans⁻¹ + end + + theorem passoc_phomotopy_middle {A B C D : Type*} (h : C →* D) {g g' : B →* C} (f : A →* B) + (p : g ~* g') : phsquare (passoc h g f) (passoc h g' f) + (pwhisker_right f (pwhisker_left h p)) (pwhisker_left h (pwhisker_right f p)) := + begin + induction p using phomotopy_rec_on_idp, + rewrite [pwhisker_right_refl, pwhisker_left_refl], + rewrite [pwhisker_right_refl, pwhisker_left_refl], + exact phvrfl + end + + definition pwhisker_right_pwhisker_left {A B C : Type*} {g g' : B →* C} {f f' : A →* B} + (p : g ~* g') (q : f ~* f') : + phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ + !pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹ + end + + definition pwhisker_left_phsquare (f : B →* C) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare (pwhisker_left f p₁₀) (pwhisker_left f p₁₂) + (pwhisker_left f p₀₁) (pwhisker_left f p₂₁) := + !pwhisker_left_trans⁻¹ ⬝ ap (pwhisker_left f) p ⬝ !pwhisker_left_trans + + definition pwhisker_right_phsquare (f : C →* A) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare (pwhisker_right f p₁₀) (pwhisker_right f p₁₂) + (pwhisker_right f p₀₁) (pwhisker_right f p₂₁) := + !pwhisker_right_trans⁻¹ ⬝ ap (pwhisker_right f) p ⬝ !pwhisker_right_trans + + end phsquare + + definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) : + phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q := + begin induction q, induction p, exact !trans_refl⁻¹ end + + definition pcompose_left_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B} + (H : f ~* f') : ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) := + begin + induction H using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, + exact !pwhisker_left_refl⁻¹ + end + + definition pcompose_right_eq_of_phomotopy {A B C : Type*} {g g' : B →* C} (f : A →* B) + (H : g ~* g') : ap (λg, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_right f H) := + begin + induction H using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, + exact !pwhisker_right_refl⁻¹ + end + + definition to_fun_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : + ap010 pmap.to_fun (eq_of_phomotopy p) a = p a := + begin + induction p using phomotopy_rec_on_idp, + exact ap (λx, ap010 pmap.to_fun x a) !eq_of_phomotopy_refl + end + + definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B) + : respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g := + idp + + definition phomotopy_mk_ppmap [constructor] {A B C : Type*} {f g : A →* ppmap B C} (p : Πa, f a ~* g a) + (q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f)) + : f ~* g := + begin + apply phomotopy.mk (λa, eq_of_phomotopy (p a)), + apply eq_of_fn_eq_fn (pmap_eq_equiv _ _), esimp [pmap_eq_equiv], + refine !phomotopy_of_eq_con ⬝ _, + refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q, + end + + definition pconst_pcompose_pconst (A B C : Type*) : + pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) := + idp + + definition pconst_pcompose_phomotopy_pconst {A B C : Type*} {f : A →* B} (p : f ~* pconst A B) : + pconst_pcompose f = pwhisker_left (pconst B C) p ⬝* pcompose_pconst (pconst B C) := + begin + assert H : Π(p : pconst A B ~* f), + pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C), + { intro p, induction p using phomotopy_rec_on_idp, reflexivity }, + refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp, + end + + definition passoc_pconst_right {A B C D : Type*} (h : C →* D) (g : B →* C) : + passoc h g (pconst A B) ⬝* (pwhisker_left h (pcompose_pconst g) ⬝* pcompose_pconst h) = + pcompose_pconst (h ∘* g) := + begin + fapply phomotopy_eq, + { intro a, exact !idp_con }, + { induction h with h h₀, induction g with g g₀, induction D with D d₀, induction C with C c₀, + esimp at *, induction g₀, induction h₀, reflexivity } + end + + definition passoc_pconst_middle {A A' B B' : Type*} (g : B →* B') (f : A' →* A) : + passoc g (pconst A B) f ⬝* (pwhisker_left g (pconst_pcompose f) ⬝* pcompose_pconst g) = + pwhisker_right f (pcompose_pconst g) ⬝* pconst_pcompose f := + begin + fapply phomotopy_eq, + { intro a, esimp, exact !idp_con ⬝ !idp_con }, + { induction g with g g₀, induction f with f f₀, induction B' with D d₀, induction A with C c₀, + esimp at *, induction g₀, induction f₀, reflexivity } + end + + definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) : + @ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g := + begin + fapply phomotopy_mk_ppmap, + { exact passoc h g }, + { esimp, + refine idp ◾** (!phomotopy_of_eq_con ⬝ + (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, + exact passoc_pconst_right h g } + end + + definition ppcompose_left_ppcompose_right {A A' B B' : Type*} (g : B →* B') (f : A' →* A) : + psquare (ppcompose_left g) (ppcompose_left g) (ppcompose_right f) (ppcompose_right f) := + begin + fapply phomotopy_mk_ppmap, + { intro h, exact passoc g h f }, + { refine idp ◾** (!phomotopy_of_eq_con ⬝ + (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝ + (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** + !phomotopy_of_eq_of_phomotopy)⁻¹, + apply passoc_pconst_middle } + end + + definition pcompose_pconst_phomotopy {A B C : Type*} {f f' : B →* C} (p : f ~* f') : + pwhisker_right (pconst A B) p ⬝* pcompose_pconst f' = pcompose_pconst f := + begin + fapply phomotopy_eq, + { intro a, exact to_homotopy_pt p }, + { induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀, + esimp at *, induction f₀, reflexivity } + end + + definition pid_pconst (A B : Type*) : pcompose_pconst (pid B) = pid_pcompose (pconst A B) := + by reflexivity + + definition pid_pconst_pcompose {A B C : Type*} (f : A →* B) : + phsquare (pid_pcompose (pconst B C ∘* f)) + (pcompose_pconst (pid C)) + (pwhisker_left (pid C) (pconst_pcompose f)) + (pconst_pcompose f) := + begin + fapply phomotopy_eq, + { reflexivity }, + { induction f with f f₀, induction B with B b₀, esimp at *, induction f₀, reflexivity } + end + + definition ppcompose_left_pconst [constructor] (A B C : Type*) : + @ppcompose_left A _ _ (pconst B C) ~* pconst (ppmap A B) (ppmap A C) := + begin + fapply phomotopy_mk_ppmap, + { exact pconst_pcompose }, + { refine idp ◾** !phomotopy_of_eq_idp ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ } + end + + definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') : + @ppcompose_left A _ _ g ~* ppcompose_left g' := + begin + induction p using phomotopy_rec_on_idp, + reflexivity + end + + section psquare + + variables {A 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 ppcompose_left_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (@ppcompose_left A _ _ f₁₀) (ppcompose_left f₁₂) + (ppcompose_left f₀₁) (ppcompose_left f₂₁) := + !ppcompose_left_pcompose⁻¹* ⬝* ppcompose_left_phomotopy p ⬝* !ppcompose_left_pcompose + + definition trans_phomotopy_hconcat {f₀₁' f₀₁''} + (q₂ : f₀₁'' ~* f₀₁') (q₁ : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + (q₂ ⬝* q₁) ⬝ph* p = q₂ ⬝ph* q₁ ⬝ph* p := + idp ◾** (ap (pwhisker_left f₁₂) !trans_symm ⬝ !pwhisker_left_trans) ⬝ !trans_assoc⁻¹ + + definition symm_phomotopy_hconcat {f₀₁'} (q : f₀₁ ~* f₀₁') + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : q⁻¹* ⬝ph* p = p ⬝* pwhisker_left f₁₂ q := + idp ◾** ap (pwhisker_left f₁₂) !symm_symm + + definition refl_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝ph* p = p := + idp ◾** (ap (pwhisker_left _) !refl_symm ⬝ !pwhisker_left_refl) ⬝ !trans_refl + + local attribute phomotopy.rfl [reducible] + theorem pwhisker_left_phomotopy_hconcat {f₀₁'} (r : f₀₁' ~* f₀₁) + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : + pwhisker_left f₀₃ r ⬝ph* (p ⬝v* q) = (r ⬝ph* p) ⬝v* q := + by induction r using phomotopy_rec_on_idp; rewrite [pwhisker_left_refl, +refl_phomotopy_hconcat] + + theorem pvcompose_pwhisker_left {f₀₁'} (r : f₀₁ ~* f₀₁') + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : + (p ⬝v* q) ⬝* (pwhisker_left f₁₄ (pwhisker_left f₀₃ r)) = (p ⬝* pwhisker_left f₁₂ r) ⬝v* q := + by induction r using phomotopy_rec_on_idp; rewrite [+pwhisker_left_refl, + trans_refl] + + definition phconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₃₀ f₃₂ f₂₁ f₄₁} + (r : p = p') (s : q = q') : p ⬝h* q = p' ⬝h* q' := + ap011 phconcat r s + + definition pvconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₁₂ f₁₄ f₀₃ f₂₃} + (r : p = p') (s : q = q') : p ⬝v* q = p' ⬝v* q' := + ap011 pvconcat r s + + definition phinverse2 {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} + (r : p = p') : p⁻¹ʰ* = p'⁻¹ʰ* := + ap phinverse r + + definition pvinverse2 {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} + (r : p = p') : p⁻¹ᵛ* = p'⁻¹ᵛ* := + ap pvinverse r + + definition phomotopy_hconcat2 {q q' : f₀₁' ~* f₀₁} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} + (r : q = q') (s : p = p') : q ⬝ph* p = q' ⬝ph* p' := + ap011 phomotopy_hconcat r s + + definition hconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₂₁' ~* f₂₁} + (r : p = p') (s : q = q') : p ⬝hp* q = p' ⬝hp* q' := + ap011 hconcat_phomotopy r s + + definition phomotopy_vconcat2 {q q' : f₁₀' ~* f₁₀} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} + (r : q = q') (s : p = p') : q ⬝pv* p = q' ⬝pv* p' := + ap011 phomotopy_vconcat r s + + definition vconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₁₂' ~* f₁₂} + (r : p = p') (s : q = q') : p ⬝vp* q = p' ⬝vp* q' := + ap011 vconcat_phomotopy r s + + -- for consistency, should there be a second star here? + infix ` ◾h* `:79 := phconcat2 + infix ` ◾v* `:79 := pvconcat2 + infixl ` ◾hp* `:79 := hconcat_phomotopy2 + infixr ` ◾ph* `:79 := phomotopy_hconcat2 + infixl ` ◾vp* `:79 := vconcat_phomotopy2 + infixr ` ◾pv* `:79 := phomotopy_vconcat2 + postfix `⁻²ʰ*`:(max+1) := phinverse2 + postfix `⁻²ᵛ*`:(max+1) := pvinverse2 + + end psquare + + /- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it + -/ + -- fapply phomotopy_mk_ppmap, + -- { intro f, exact pwhisker_right f p }, + -- { refine ap (λx, _ ⬝* x) !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, + -- exact pcompose_pconst_phomotopy p } + + definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) : + ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) := + !phomotopy_rec_on_idp_refl + + -- definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) := + -- begin + -- refine eq_equiv_fn_eq_of_equiv (@pmap.sigma_char X Y) f g ⬝e _, + -- refine !sigma_eq_equiv ⬝e _, + -- refine _ ⬝e (phomotopy.sigma_char f g)⁻¹ᵉ, + -- fapply sigma_equiv_sigma, + -- { esimp, apply eq_equiv_homotopy }, + -- { induction g with g gp, induction Y with Y y0, esimp, intro p, induction p, esimp at *, + -- refine !pathover_idp ⬝e _, refine _ ⬝e !eq_equiv_eq_symm, + -- apply equiv_eq_closed_right, exact !idp_con⁻¹ } + -- end + + definition pmap_eq_idp {X Y : Type*} (f : X →* Y) : + pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f := + ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f + + definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := + begin + fapply pequiv_of_equiv, + { fapply equiv.MK: esimp, + { intro f, fapply pmap_eq, + { intro x, exact f x }, + { exact (respect_pt f)⁻¹ }}, + { intro p, fapply pmap.mk, + { intro x, exact ap010 pmap.to_fun p x }, + { note z := apd respect_pt p, + note z2 := square_of_pathover z, + refine eq_of_hdeg_square z2 ⬝ !ap_constant }}, + { intro p, exact sorry }, + { intro p, exact sorry }}, + { apply pmap_eq_idp} + end + + /- + Do we want to use a structure of homotopies between pointed homotopies? Or are equalities fine? + If we set up things more generally, we could define this as + "pointed homotopies between the dependent pointed maps p and q" + -/ + structure phomotopy2 {A B : Type*} {f g : A →* B} (p q : f ~* g) : Type := + (homotopy_eq : p ~ q) + (homotopy_pt_eq : whisker_right (respect_pt g) (homotopy_eq pt) ⬝ to_homotopy_pt q = to_homotopy_pt p) + + /- this sets it up more generally, for illustrative purposes -/ + structure ppi' (A : Type*) (P : A → Type) (p : P pt) := + (to_fun : Π a : A, P a) + (resp_pt : to_fun (Point A) = p) + attribute ppi'.to_fun [coercion] + definition ppi_homotopy' {A : Type*} {P : A → Type} {x : P pt} (f g : ppi' A P x) : Type := + ppi' A (λa, f a = g a) (ppi'.resp_pt f ⬝ (ppi'.resp_pt g)⁻¹) + definition ppi_homotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x} (p q : ppi_homotopy' f g) : Type := + ppi_homotopy' p q + + infix ` ~*2 `:50 := phomotopy2 + + variables {A B : Type*} {f g : A →* B} (p q : f ~* g) + + -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q := + -- sorry + +end pointed diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 6441d21..6dfe10b 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -12,7 +12,7 @@ open eq pointed equiv sigma The goal of this file is to give the truncation level of the type of pointed maps, giving the connectivity of the domain and the truncation level of the codomain. - This is is_trunc_pmap at the end. + This is is_trunc_pmap_of_is_conn at the end. First we define the type of dependent pointed maps as a tool, because these appear in the more general @@ -164,7 +164,7 @@ section { exact pt } } end - definition is_trunc_pmap (k : ℕ₋₂) (B : (n.+1+2+k)-Type*) + definition is_trunc_pmap_of_is_conn (k : ℕ₋₂) (B : (n.+1+2+k)-Type*) : is_trunc k.+1 (A →* B) := @is_trunc_equiv_closed _ _ k.+1 (ppi_equiv_pmap A B) (is_trunc_ppi A n k (λ a, B))