From da033c0f4c66e0ea0ba965dff14b977fdeb7c003 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 20 Sep 2018 02:08:45 +0200 Subject: [PATCH] work on dependent smash and cup product on EM-spaces also many small fixes --- algebra/arrow_group.hlean | 37 +- archive/smash_assoc.hlean | 2 +- homotopy/EM.hlean | 16 +- homotopy/EMRing.hlean | 20 +- homotopy/degree.hlean | 7 +- homotopy/dsmash.hlean | 1737 +++++++++++++++++++++++++++ homotopy/smash.hlean | 4 +- homotopy/spherical_fibrations.hlean | 2 +- move_to_lib.hlean | 2 +- pointed_binary.hlean | 94 ++ pointed_pi.hlean | 2 +- spectrum/basic.hlean | 12 +- univalent_subcategory.hlean | 4 +- 13 files changed, 1905 insertions(+), 34 deletions(-) create mode 100644 homotopy/dsmash.hlean diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index 77c1dc4..ac16067 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -9,7 +9,7 @@ which are used in the definition of cohomology. -/ import algebra.group_theory ..pointed ..pointed_pi eq2 -open pi pointed algebra group eq equiv is_trunc trunc susp +open pi pointed algebra group eq equiv is_trunc trunc susp nat function namespace group /- Group of dependent functions into a loop space -/ @@ -39,13 +39,15 @@ namespace group { exact !con_left_inv_idp }}, end - definition inf_group_ppi [constructor] {A : Type*} (B : A → Type*) : - inf_group (Π*a, Ω (B a)) := + definition inf_group_ppi [constructor] {A : Type*} (B : A → Type*) : inf_group (Π*a, Ω (B a)) := @inf_group_of_inf_pgroup _ (inf_pgroup_pppi B) definition gppi_loop [constructor] {A : Type*} (B : A → Type*) : InfGroup := InfGroup.mk (Π*a, Ω (B a)) (inf_group_ppi B) + definition gppi_loopn [constructor] (n : ℕ) [H : is_succ n] {A : Type*} (B : A → Type*) : InfGroup := + InfGroup.mk (Π*a, Ω[n] (B a)) (by induction H with n; exact inf_group_ppi (Ω[n] ∘ B)) + definition Group_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : Group := gtrunc (gppi_loop B) @@ -98,9 +100,7 @@ namespace group clear f g, esimp at *, exact ppi_mul_loop.lemma2 (f' pt) (g' pt) f_pt g_pt end - variable (k) - - definition gloop_ppi_isomorphism : + definition gloop_ppi_isomorphism_gen (k : ppi B x₀) : Ωg (pointed.Mk k) ≃∞g gppi_loop (λ a, pointed.Mk (ppi.to_fun k a)) := begin apply inf_isomorphism_of_equiv (ppi_loop_equiv k), @@ -109,13 +109,24 @@ namespace group exact ppi_mul_loop (phomotopy_of_eq f) (phomotopy_of_eq g) end - definition trunc_ppi_loop_isomorphism_lemma : - gtrunc (gloop (pointed.Mk k)) ≃g gtrunc (gppi_loop (λa, pointed.Mk (k a))) := - gtrunc_isomorphism_gtrunc (gloop_ppi_isomorphism k) + definition gloop_ppi_isomorphism (B : A → Type*) : Ωg (Π*a, B a) ≃∞g gppi_loop B := + proof gloop_ppi_isomorphism_gen (ppi_const B) qed - definition trunc_ppi_loop_isomorphism {A : Type*} (B : A → Type*) : + definition gloopn_ppi_isomorphism (n : ℕ) [H : is_succ n] (B : A → Type*) : + Ωg[n] (Π*a, B a) ≃∞g gppi_loopn n B := + begin + induction H with n, induction n with n IH, + { exact gloop_ppi_isomorphism B }, + { exact Ωg≃ (pequiv_of_inf_isomorphism IH) ⬝∞g gloop_ppi_isomorphism (Ω[succ n] ∘ B) } + end + + definition trunc_ppi_loop_isomorphism_gen (k : ppi B x₀) : + gtrunc (gloop (pointed.Mk k)) ≃g gtrunc (gppi_loop (λa, pointed.Mk (k a))) := + gtrunc_isomorphism_gtrunc (gloop_ppi_isomorphism_gen k) + + definition trunc_ppi_loop_isomorphism (B : A → Type*) : gtrunc (gloop (Π*(a : A), B a)) ≃g gtrunc (gppi_loop B) := - proof trunc_ppi_loop_isomorphism_lemma (ppi_const B) qed + proof trunc_ppi_loop_isomorphism_gen (ppi_const B) qed /- We first define the group structure on A →* Ω B (except for truncatedness). @@ -169,10 +180,10 @@ namespace group loop_susp_intro (pmap_mul f g) ~* pmap_mul (loop_susp_intro f) (loop_susp_intro g) := pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose - definition InfGroup_pmap [reducible] [constructor] (A B : Type*) : InfGroup := + definition gpmap_loop [reducible] [constructor] (A B : Type*) : InfGroup := InfGroup.mk (A →* Ω B) !inf_group_ppi - definition InfGroup_pmap' [reducible] [constructor] (A : Type*) {B C : Type*} (e : Ω C ≃* B) : + definition gpmap_loop' [reducible] [constructor] (A : Type*) {B C : Type*} (e : Ω C ≃* B) : InfGroup := InfGroup.mk (A →* B) (@inf_group_of_inf_pgroup _ (inf_pgroup_pequiv_closed (ppmap_pequiv_ppmap_right e) diff --git a/archive/smash_assoc.hlean b/archive/smash_assoc.hlean index 1741bf9..c056ca6 100644 --- a/archive/smash_assoc.hlean +++ b/archive/smash_assoc.hlean @@ -1,7 +1,7 @@ -- Authors: Floris van Doorn -- In collaboration with Stefano, Robin -import ..homotopy.smash +import ..homotopy.smash 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 sigma diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 5df2456..ba94e0c 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -346,7 +346,13 @@ namespace EM /- properties about EM -/ definition gEM (G : AbGroup) (n : ℕ) : InfGroup := - InfGroup.mk (EM G n) (inf_group_equiv_closed (loop_EM G n) _) + InfGroup_equiv_closed (Ωg (EMadd1 G n)) (loop_EM G n) + + definition gloop_EM1 [constructor] (G : Group) : Ωg (EM1 G) ≃∞g InfGroup_of_Group G := + inf_isomorphism_of_equiv (EM.base_eq_base_equiv G) groupoid_quotient.encode_con + + definition gEM0_isomorphism (G : AbGroup) : gEM G 0 ≃∞g InfGroup_of_Group G := + !InfGroup_equiv_closed_isomorphism⁻¹ᵍ⁸ ⬝∞g gloop_EM1 G definition gEM_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : gEM G n →∞g gEM H n := inf_homomorphism.mk (EM_functor φ n) sorry @@ -359,6 +365,14 @@ namespace EM { have is_trunc (n.+1) X, from H, exact EMadd1_pmap n e } end + definition EM_homomorphism_gloop [unfold 8] {G : AbGroup} (X : Type*) (n : ℕ) + (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc n X] : gEM G n →∞g Ωg X := + Ωg→ (EMadd1_pmap n e) ∘∞g !InfGroup_equiv_closed_isomorphism⁻¹ᵍ⁸ + + -- definition EM_homomorphism [unfold 8] {G : AbGroup} {X : Type*} (Y : Type*) (e : Ω Y ≃* X) (n : ℕ) + -- (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc n X] : gEM G n →∞g X := + -- _ + -- definition gEM_gfunctor {G H : AbGroup} (n : ℕ) : (G →gg H) →∞g (gEM G n →∞g gEM H n) := -- inf_homomorphism.mk (EM_functor _ n) sorry diff --git a/homotopy/EMRing.hlean b/homotopy/EMRing.hlean index c2c4ec8..a69ea67 100644 --- a/homotopy/EMRing.hlean +++ b/homotopy/EMRing.hlean @@ -38,7 +38,7 @@ begin -- EM0EMadd1product φ m end -definition EMproduct {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : +definition EMproduct1 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : EM A n →* EM B m →** EM C (m + n) := begin cases n with n, @@ -51,17 +51,29 @@ begin { exact ppcompose_left (ptransport (EMadd1 C) !succ_add⁻¹) ∘* EMadd1product φ n m }} end -definition EMproduct' {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : +definition EMproduct2 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : EM A n →* EM B m →** EM C (m + n) := begin - assert H1 : is_trunc n (InfGroup_pmap' (EM B m) (loop_EM C (m + n))), + assert H1 : is_trunc n (gpmap_loop' (EM B m) (loop_EM C (m + n))), { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM }, - apply EM_pmap (InfGroup_pmap' (EM B m) (loop_EM C (m + n))) n, + apply EM_pmap (gpmap_loop' (EM B m) (loop_EM C (m + n))) n, exact sorry -- exact _ /- (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* -/ ∘∞g _ /-ppcompose_left !loopn_EMadd1_add⁻¹ᵉ*-/ ∘∞g -- _ ∘∞g inf_homomorphism_of_homomorphism φ end +definition EMproduct3' {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : + gEM A n →∞g gpmap_loop' (EM B m) (loop_EM C (m + n)) := +begin + assert H1 : is_trunc n (gpmap_loop' (EM B m) (loop_EM C (m + n))), + { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM }, +-- refine EM_homomorphism _ _ _, +-- --(gmap_loop' (EM B m) (loop_EM C (m + n))) n, +-- exact _ /- (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* -/ ∘∞g _ /-ppcompose_left !loopn_EMadd1_add⁻¹ᵉ*-/ ∘∞g +-- _ ∘∞g inf_homomorphism_of_homomorphism φ + exact sorry +end + end EM diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 5883237..a49c7cf 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -1,6 +1,6 @@ import homotopy.sphere2 ..move_to_lib -open fin eq equiv group algebra sphere.ops pointed nat int trunc is_equiv function circle +open fin eq equiv group algebra sphere.ops pointed trunc is_equiv function circle int nat protected definition nat.eq_one_of_mul_eq_one {n : ℕ} (m : ℕ) (q : n * m = 1) : n = 1 := begin @@ -83,7 +83,8 @@ namespace sphere -- (pair 1 2)) -- (tr surf)) - definition πnSn_surf (n : ℕ) : πnSn (n+1) (tr surf) = 1 :> ℤ := + attribute gloopn [reducible] + definition πnSn_surf (n : ℕ) : πnSn (n+1) (tr (@surf (n+1))) = 1 := begin cases n with n IH, { refine ap (πnSn _ ∘ tr) surf_eq_loop ⬝ _, apply transport_code_loop }, @@ -91,7 +92,7 @@ namespace sphere end definition deg {n : ℕ} [H : is_succ n] (f : S n →* S n) : ℤ := - by induction H with n; exact πnSn (n+1) (π→g[n+1] f (tr surf)) + by induction H with n; exact πnSn (n+1) (π→g[n+1] f (tr (@surf (n+1)))) definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S n)) = (1 : ℤ) := by induction H with n; diff --git a/homotopy/dsmash.hlean b/homotopy/dsmash.hlean new file mode 100644 index 0000000..7913519 --- /dev/null +++ b/homotopy/dsmash.hlean @@ -0,0 +1,1737 @@ +-- Authors: Floris van Doorn + +/- + +The "dependent" smash product. + +Given A : Type* and B : A → Type* it is the cofiber of +A ∨ B pt → Σ(a : A), B a +However, we define it (equivalently) as the pushout of 2 ← A + B pt → Σ(a : A), B a. +-/ + +import .smash_adjoint ..pointed_binary + +open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber sigma.ops wedge sigma function prod.ops + +namespace dsmash + + variables {A : Type*} {B : A → Type*} + + definition sigma_of_sum [unfold 3] (u : A + B pt) : Σa, B a := + by induction u with a b; exact ⟨a, pt⟩; exact ⟨pt, b⟩ + + definition dsmash' (B : A → Type*) : Type := pushout.pushout (@sigma_of_sum A B) (@smash.bool_of_sum A (B pt)) + protected definition mk' (a : A) (b : B a) : dsmash' B := pushout.inl ⟨a, b⟩ + + definition dsmash [constructor] (B : A → Type*) : Type* := + pointed.MK (dsmash' B) (dsmash.mk' pt pt) + + notation `⋀` := dsmash + + protected definition mk (a : A) (b : B a) : ⋀ B := pushout.inl ⟨a, b⟩ + definition auxl : ⋀ B := pushout.inr ff + definition auxr : ⋀ B := pushout.inr tt + definition gluel (a : A) : dsmash.mk a pt = auxl :> ⋀ B := pushout.glue (sum.inl a) + definition gluer (b : B pt) : dsmash.mk pt b = auxr :> ⋀ B := pushout.glue (sum.inr b) + + definition gluel' (a a' : A) : dsmash.mk a pt = dsmash.mk a' pt :> ⋀ B := + gluel a ⬝ (gluel a')⁻¹ + definition gluer' (b b' : B pt) : dsmash.mk pt b = dsmash.mk pt b' :> ⋀ B := + gluer b ⬝ (gluer b')⁻¹ + definition glue (a : A) (b : B pt) : dsmash.mk a pt = dsmash.mk pt b :> ⋀ B := + gluel' a pt ⬝ gluer' pt b + + definition glue_pt_left (b : B pt) : glue (Point A) b = gluer' pt b := + whisker_right _ !con.right_inv ⬝ !idp_con + + definition glue_pt_right (a : A) : glue a (Point (B a)) = gluel' a pt := + proof whisker_left _ !con.right_inv qed + + definition ap_mk_left {a a' : A} (p : a = a') : ap (λa, dsmash.mk a (Point (B a))) p = gluel' a a' := + !ap_is_constant + + definition ap_mk_right {b b' : B pt} (p : b = b') : ap (dsmash.mk (Point A)) p = gluer' b b' := + !ap_is_constant + + protected definition rec {P : ⋀ B → Type} (Pmk : Πa b, P (dsmash.mk a b)) + (Pl : P auxl) (Pr : P auxr) (Pgl : Πa, Pmk a pt =[gluel a] Pl) + (Pgr : Πb, Pmk pt b =[gluer b] Pr) (x : dsmash' B) : P x := + begin + induction x with x b u, + { induction x with a b, exact Pmk a b }, + { induction b, exact Pl, exact Pr }, + { induction u, + { apply Pgl }, + { apply Pgr }} + end + + theorem rec_gluel {P : ⋀ B → Type} {Pmk : Πa b, P (dsmash.mk a b)} + {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) + (Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) : + apd (dsmash.rec Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a := + !pushout.rec_glue + + theorem rec_gluer {P : ⋀ B → Type} {Pmk : Πa b, P (dsmash.mk a b)} + {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) + (Pgr : Πb, Pmk pt b =[gluer b] Pr) (b : B pt) : + apd (dsmash.rec Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b := + !pushout.rec_glue + + theorem rec_glue {P : ⋀ B → Type} {Pmk : Πa b, P (dsmash.mk a b)} + {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) + (Pgr : Π(b : B pt), Pmk pt b =[gluer b] Pr) (a : A) (b : B pt) : + apd (dsmash.rec Pmk Pl Pr Pgl Pgr) (dsmash.glue a b) = + (Pgl a ⬝o (Pgl pt)⁻¹ᵒ) ⬝o (Pgr pt ⬝o (Pgr b)⁻¹ᵒ) := + by rewrite [↑glue, ↑gluel', ↑gluer', +apd_con, +apd_inv, +rec_gluel, +rec_gluer] + + protected definition elim {P : Type} (Pmk : Πa b, P) (Pl Pr : P) + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B pt, Pmk pt b = Pr) (x : dsmash' B) : P := + dsmash.rec Pmk Pl Pr (λa, pathover_of_eq _ (Pgl a)) (λb, pathover_of_eq _ (Pgr b)) x + + -- an elim where you are forced to make (Pgl pt) and (Pgl pt) to be reflexivity + protected definition elim' [reducible] {P : Type} (Pmk : Πa b, P) + (Pgl : Πa : A, Pmk a pt = Pmk pt pt) (Pgr : Πb : B pt, Pmk pt b = Pmk pt pt) + (ql : Pgl pt = idp) (qr : Pgr pt = idp) (x : dsmash' B) : P := + dsmash.elim Pmk (Pmk pt pt) (Pmk pt pt) Pgl Pgr x + + theorem elim_gluel {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B pt, Pmk pt b = Pr) (a : A) : + ap (dsmash.elim Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a := + begin + apply inj_inv !(pathover_constant (@gluel A B a)), + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑dsmash.elim,rec_gluel], + end + + theorem elim_gluer {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B pt, Pmk pt b = Pr) (b : B pt) : + ap (dsmash.elim Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b := + begin + apply inj_inv !(pathover_constant (@gluer A B b)), + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑dsmash.elim,rec_gluer], + end + + theorem elim_glue {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B pt, Pmk pt b = Pr) (a : A) (b : B pt) : + ap (dsmash.elim Pmk Pl Pr Pgl Pgr) (glue a b) = (Pgl a ⬝ (Pgl pt)⁻¹) ⬝ (Pgr pt ⬝ (Pgr b)⁻¹) := + by rewrite [↑glue, ↑gluel', ↑gluer', +ap_con, +ap_inv, +elim_gluel, +elim_gluer] + +end dsmash +open dsmash +attribute dsmash.mk dsmash.mk' dsmash.auxl dsmash.auxr [constructor] +attribute dsmash.elim' dsmash.rec dsmash.elim [unfold 9] [recursor 9] + +namespace dsmash + + variables {A A' C : Type*} {B : A → Type*} {D : C → Type*} {a a' : A} {b : B a} {b' : B a'} + + definition mk_eq_mk (p : a = a') (q : b =[p] b') : dsmash.mk a b = dsmash.mk a' b' := + ap pushout.inl (dpair_eq_dpair p q) + + definition gluer2 (b : B a) (p : a = pt) : dsmash.mk a b = auxr := + mk_eq_mk p !pathover_tr ⬝ gluer _ + + definition elim_gluel' {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B pt, Pmk pt b = Pr) (a a' : A) : + ap (dsmash.elim Pmk Pl Pr Pgl Pgr) (gluel' a a') = Pgl a ⬝ (Pgl a')⁻¹ := + !ap_con ⬝ whisker_left _ !ap_inv ⬝ !elim_gluel ◾ !elim_gluel⁻² + + definition elim_gluer' {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B pt, Pmk pt b = Pr) (b b' : B pt) : + ap (dsmash.elim Pmk Pl Pr Pgl Pgr) (gluer' b b') = Pgr b ⬝ (Pgr b')⁻¹ := + !ap_con ⬝ whisker_left _ !ap_inv ⬝ !elim_gluer ◾ !elim_gluer⁻² + + definition elim_gluel'_same {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B pt, Pmk pt b = Pr) (a : A) : + elim_gluel' Pgl Pgr a a = + ap02 (dsmash.elim Pmk Pl Pr Pgl Pgr) (con.right_inv (gluel a)) ⬝ (con.right_inv (Pgl 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 + + definition elim_gluer'_same {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B pt, Pmk pt b = Pr) (b : B pt) : + elim_gluer' Pgl Pgr b b = + ap02 (dsmash.elim Pmk Pl Pr Pgl Pgr) (con.right_inv (gluer b)) ⬝ (con.right_inv (Pgr 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 elim'_gluel'_pt {P : Type} {Pmk : Πa b, P} + (Pgl : Πa : A, Pmk a pt = Pmk pt pt) (Pgr : Πb : B pt, Pmk pt b = Pmk pt pt) + (a : A) (ql : Pgl pt = idp) (qr : Pgr pt = idp) : + ap (dsmash.elim' Pmk Pgl Pgr ql qr) (gluel' a pt) = Pgl a := + !elim_gluel' ⬝ whisker_left _ ql⁻² + + definition elim'_gluer'_pt {P : Type} {Pmk : Πa b, P} + (Pgl : Πa : A, Pmk a pt = Pmk pt pt) (Pgr : Πb : B pt, Pmk pt b = Pmk pt pt) + (b : B pt) (ql : Pgl pt = idp) (qr : Pgr pt = idp) : + ap (dsmash.elim' Pmk Pgl Pgr ql qr) (gluer' b pt) = Pgr b := + !elim_gluer' ⬝ whisker_left _ qr⁻² + + protected definition rec_eq {C : Type} {f g : ⋀ B → C} + (Pmk : Πa b, f (dsmash.mk a b) = g (dsmash.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 : dsmash' 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 {C : Type} {f g : ⋀ B → C} + {Pmk : Πa b, f (dsmash.mk a b) = g (dsmash.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 (dsmash.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 {C : Type} {f g : ⋀ B → C} + {Pmk : Πa b, f (dsmash.mk a b) = g (dsmash.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 pt) : + natural_square (dsmash.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 dependent smash product -/ + definition dsmash_functor' [unfold 7] (f : A →* C) (g : Πa, B a →* D (f a)) : ⋀ B → ⋀ D := + begin + intro x, induction x, + { exact dsmash.mk (f a) (g a b) }, + { exact auxl }, + { exact auxr }, + { exact ap (dsmash.mk (f a)) (respect_pt (g a)) ⬝ gluel (f a) }, + { exact gluer2 (g pt b) (respect_pt f) } + end + + definition dsmash_functor [constructor] (f : A →* C) (g : Πa, B a →* D (f a)) : ⋀ B →* ⋀ D := + begin + fapply pmap.mk, + { exact dsmash_functor' f g }, + { exact mk_eq_mk (respect_pt f) (respect_pt (g pt) ⬝po apd (λa, Point (D a)) (respect_pt f)) }, + end + + infixr ` ⋀→ `:65 := dsmash_functor + + definition pmap_of_map' [constructor] (A : Type*) {B : Type} (f : A → B) : + A →* pointed.MK B (f pt) := + pmap.mk f idp + + definition functor_gluel (f : A →* C) (g : Πa, B a →* D (f a)) (a : A) : + ap (f ⋀→ g) (gluel a) = ap (dsmash.mk (f a)) (respect_pt (g a)) ⬝ gluel (f a) := + !elim_gluel + + definition functor_gluer (f : A →* C) (g : Πa, B a →* D (f a)) (b : B pt) : + ap (f ⋀→ g) (gluer b) = gluer2 (g pt b) (respect_pt f) := + !elim_gluer + + -- definition functor_gluel2 {C : Type} {D : C → Type} (f : A → C) (g : Πa, B a → D (f a)) (a : A) : + -- ap (@dsmash_functor A (pointed.MK C (f pt)) B (λc, pointed.MK (D c) _) (pmap_of_map' A f) (λa, pmap_of_map' (B a) (g 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 : Πa, B a →* D (f a)) (a a' : A) : + -- ap (f ⋀→ g) (gluel' a a') = ap (dsmash.mk (f a)) (respect_pt g) ⬝ + -- gluel' (f a) (f a') ⬝ (ap (dsmash.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 : Πa, B a →* D (f a)) (b b' : B) : + -- ap (f ⋀→ g) (gluer' b b') = ap (λc, dsmash.mk c (g b)) (respect_pt f) ⬝ + -- gluer' (g b) (g b') ⬝ (ap (λc, dsmash.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 : Πa, B a →* D (f a)) (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 g 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 dsmash_functor_pid [constructor] (B : A → Type*) : + pid A ⋀→ (λa, pid (B a)) ~* pid (⋀ 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 dependent smash product respects pointed homotopies, and some computation rules for this pointed homotopy -/ + definition dsmash_functor_phomotopy {f f' : A →* C} {g : Πa, B a →* D (f a)} {g' : Πa, B a →* D (f' a)} + (h₁ : f ~* f') (h₂ : Πa, ptransport D (h₁ a) ∘* g a ~* g' a) : f ⋀→ g ~* f' ⋀→ g' := + begin + induction h₁ using phomotopy_rec_idp, + --induction h₂ using phomotopy_rec_idp, + exact sorry --reflexivity + end + + infixr ` ⋀~ `:78 := dsmash_functor_phomotopy + + /- a more explicit proof, if we ever need it -/ + -- definition dsmash_functor_homotopy [unfold 11] {f f' : A →* C} {g g' : Πa, B a →* D (f a)} + -- (h₁ : f ~* f') (h₂ : g ~* g') : f ⋀→ g ~ f' ⋀→ g' := + -- begin + -- intro x, induction x with a b a b, + -- { exact ap011 dsmash.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 dsmash.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 dsmash.mk (h₂ b) (to_homotopy_pt h₁) }, + -- end + + -- definition dsmash_functor_phomotopy [constructor] {f f' : A →* C} {g g' : Πa, B a →* D (f a)} + -- (h₁ : f ~* f') (h₂ : g ~* g') : f ⋀→ g ~* f' ⋀→ g' := + -- begin + -- apply phomotopy.mk (dsmash_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 dsmash_functor_phomotopy_refl (f : A →* C) (g : Πa, B a →* D (f a)) : + -- dsmash_functor_phomotopy (phomotopy.refl f) (phomotopy.refl g) = phomotopy.rfl := + -- !phomotopy_rec_idp_refl ⬝ !phomotopy_rec_idp_refl + + -- definition dsmash_functor_phomotopy_symm {f₁ f₂ : A →* C} {g₁ g₂ : Πa, B a →* D (f a)} + -- (h : f₁ ~* f₂) (k : g₁ ~* g₂) : + -- dsmash_functor_phomotopy h⁻¹* k⁻¹* = (dsmash_functor_phomotopy h k)⁻¹* := + -- begin + -- induction h using phomotopy_rec_idp, induction k using phomotopy_rec_idp, + -- exact ap011 dsmash_functor_phomotopy !refl_symm !refl_symm ⬝ !dsmash_functor_phomotopy_refl ⬝ + -- !refl_symm⁻¹ ⬝ !dsmash_functor_phomotopy_refl⁻¹⁻²** + -- end + + -- definition dsmash_functor_phomotopy_trans {f₁ f₂ f₃ : A →* C} {g₁ g₂ g₃ : Πa, B a →* D (f a)} + -- (h₁ : f₁ ~* f₂) (h₂ : f₂ ~* f₃) (k₁ : g₁ ~* g₂) (k₂ : g₂ ~* g₃) : + -- dsmash_functor_phomotopy (h₁ ⬝* h₂) (k₁ ⬝* k₂) = + -- dsmash_functor_phomotopy h₁ k₁ ⬝* dsmash_functor_phomotopy h₂ k₂ := + -- begin + -- induction h₁ using phomotopy_rec_idp, induction h₂ using phomotopy_rec_idp, + -- induction k₁ using phomotopy_rec_idp, induction k₂ using phomotopy_rec_idp, + -- refine ap011 dsmash_functor_phomotopy !trans_refl !trans_refl ⬝ !trans_refl⁻¹ ⬝ idp ◾** _, + -- exact !dsmash_functor_phomotopy_refl⁻¹ + -- end + + -- definition dsmash_functor_phomotopy_trans_right {f₁ f₂ : A →* C} {g₁ g₂ g₃ : Πa, B a →* D (f a)} + -- (h₁ : f₁ ~* f₂) (k₁ : g₁ ~* g₂) (k₂ : g₂ ~* g₃) : + -- dsmash_functor_phomotopy h₁ (k₁ ⬝* k₂) = + -- dsmash_functor_phomotopy h₁ k₁ ⬝* dsmash_functor_phomotopy phomotopy.rfl k₂ := + -- begin + -- refine ap (λx, dsmash_functor_phomotopy x _) !trans_refl⁻¹ ⬝ !dsmash_functor_phomotopy_trans, + -- end + + -- definition dsmash_functor_phomotopy_phsquare {f₁ f₂ f₃ f₄ : A →* C} {g₁ g₂ g₃ g₄ : Πa, B a →* D (f a)} + -- {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 (dsmash_functor_phomotopy h₁ k₁) + -- (dsmash_functor_phomotopy h₂ k₂) + -- (dsmash_functor_phomotopy h₃ k₃) + -- (dsmash_functor_phomotopy h₄ k₄) := + -- !dsmash_functor_phomotopy_trans⁻¹ ⬝ ap011 dsmash_functor_phomotopy p q ⬝ + -- !dsmash_functor_phomotopy_trans + + -- definition dsmash_functor_eq_of_phomotopy (f : A →* C) {g g' : Πa, B a →* D (f a)} + -- (p : g ~* g') : ap (dsmash_functor f) (eq_of_phomotopy p) = + -- eq_of_phomotopy (dsmash_functor_phomotopy phomotopy.rfl p) := + -- begin + -- induction p using phomotopy_rec_idp, + -- refine ap02 _ !eq_of_phomotopy_refl ⬝ _, + -- refine !eq_of_phomotopy_refl⁻¹ ⬝ _, + -- apply ap eq_of_phomotopy, + -- exact !dsmash_functor_phomotopy_refl⁻¹ + -- end + + -- definition dsmash_functor_eq_of_phomotopy_left (g : Πa, B a →* D (f a)) {f f' : A →* C} + -- (p : f ~* f') : ap (λf, dsmash_functor f g) (eq_of_phomotopy p) = + -- eq_of_phomotopy (dsmash_functor_phomotopy p phomotopy.rfl) := + -- begin + -- induction p using phomotopy_rec_idp, + -- refine ap02 _ !eq_of_phomotopy_refl ⬝ _, + -- refine !eq_of_phomotopy_refl⁻¹ ⬝ _, + -- apply ap eq_of_phomotopy, + -- exact !dsmash_functor_phomotopy_refl⁻¹ + -- end + + /- the functorial action preserves compositions, the interchange law -/ + -- definition dsmash_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 dsmash_functor_pcompose (f' : C →* E) (f : A →* C) (g' : D →* F) (g : Πa, B a →* D (f a)) : + -- (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 dsmash_functor_pcompose_homotopy f' f g' g }, + -- { reflexivity } + -- end + + -- definition dsmash_functor_split (f : A →* C) (g : Πa, B a →* D (f a)) : + -- f ⋀→ g ~* f ⋀→ pid D ∘* pid A ⋀→ g := + -- dsmash_functor_phomotopy !pcompose_pid⁻¹* !pid_pcompose⁻¹* ⬝* !dsmash_functor_pcompose + + -- definition dsmash_functor_split_rev (f : A →* C) (g : Πa, B a →* D (f a)) : + -- f ⋀→ g ~* pid C ⋀→ g ∘* f ⋀→ pid B := + -- dsmash_functor_phomotopy !pid_pcompose⁻¹* !pcompose_pid⁻¹* ⬝* !dsmash_functor_pcompose + + /- An alternative proof which doesn't start by applying inductions, so which is more explicit -/ + -- definition dsmash_functor_pcompose_homotopy [unfold 11] (f' : C →* E) (f : A →* C) (g' : D →* F) + -- (g : Πa, B a →* D (f a)) : (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 dsmash_functor_pcompose [constructor] (f' : C →* E) (f : A →* C) (g' : D →* F) (g : Πa, B a →* D (f a)) : + -- (f' ∘* f) ⋀→ (g' ∘* g) ~* f' ⋀→ g' ∘* f ⋀→ g := + -- begin + -- fapply phomotopy.mk, + -- { exact dsmash_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 dsmash_functor_pid_pcompose [constructor] (A : Type*) (g' : C →* D) (g : B →* C) + -- : pid A ⋀→ (g' ∘* g) ~* pid A ⋀→ g' ∘* pid A ⋀→ g := + -- dsmash_functor_phomotopy !pid_pcompose⁻¹* phomotopy.rfl ⬝* !dsmash_functor_pcompose + + -- definition dsmash_functor_pcompose_pid [constructor] (B : Type*) (f' : C →* D) (f : A →* C) + -- : (f' ∘* f) ⋀→ pid B ~* f' ⋀→ (pid B) ∘* f ⋀→ (pid B) := + -- dsmash_functor_phomotopy phomotopy.rfl !pid_pcompose⁻¹* ⬝* !dsmash_functor_pcompose + + /- composing commutes with applying homotopies -/ + -- definition dsmash_functor_pcompose_phomotopy {f₂ f₂' : C →* E} {f f' : A →* C} {g₂ g₂' : D →* F} + -- {g g' : Πa, B a →* D (f a)} (h₂ : f₂ ~* f₂') (h₁ : f ~* f') (k₂ : g₂ ~* g₂') (k₁ : g ~* g') : + -- phsquare (dsmash_functor_pcompose f₂ f g₂ g) + -- (dsmash_functor_pcompose f₂' f' g₂' g') + -- (dsmash_functor_phomotopy (h₂ ◾* h₁) (k₂ ◾* k₁)) + -- (dsmash_functor_phomotopy h₂ k₂ ◾* dsmash_functor_phomotopy h₁ k₁) := + -- begin + -- induction h₁ using phomotopy_rec_idp, induction h₂ using phomotopy_rec_idp, + -- induction k₁ using phomotopy_rec_idp, induction k₂ using phomotopy_rec_idp, + -- refine (ap011 dsmash_functor_phomotopy !pcompose2_refl !pcompose2_refl ⬝ + -- !dsmash_functor_phomotopy_refl) ⬝ph** phvrfl ⬝hp** + -- (ap011 pcompose2 !dsmash_functor_phomotopy_refl !dsmash_functor_phomotopy_refl ⬝ + -- !pcompose2_refl)⁻¹, + -- end + + -- definition dsmash_functor_pid_pcompose_phomotopy_right (g₂ : D →* E) {g g' : Πa, B a →* D (f a)} + -- (k : g ~* g') : + -- phsquare (dsmash_functor_pid_pcompose A g₂ g) + -- (dsmash_functor_pid_pcompose A g₂ g') + -- (dsmash_functor_phomotopy phomotopy.rfl (pwhisker_left g₂ k)) + -- (pwhisker_left (pid A ⋀→ g₂) (dsmash_functor_phomotopy phomotopy.rfl k)) := + -- begin + -- refine dsmash_functor_phomotopy_phsquare _ _ ⬝h** !dsmash_functor_pcompose_phomotopy ⬝hp** + -- ((ap (pwhisker_right _) !dsmash_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 dsmash to squares of pointed maps -/ + -- definition dsmash_functor_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare g₁₀ g₁₂ g₀₁ g₂₁) : + -- psquare (f₁₀ ⋀→ g₁₀) (f₁₂ ⋀→ g₁₂) (f₀₁ ⋀→ g₀₁) (f₂₁ ⋀→ g₂₁) := + -- !dsmash_functor_pcompose⁻¹* ⬝* dsmash_functor_phomotopy p q ⬝* !dsmash_functor_pcompose + end + + /- f ∧ g is a pointed equivalence if f and g are -/ + definition dsmash_functor_using_pushout [unfold 7] (f : A →* C) (g : Πa, B a →* D (f a)) : + ⋀ B → ⋀ D := + begin + refine pushout.functor (f +→ (transport D (respect_pt f) ∘ g pt)) (sigma_functor f g) id _ _, + { intro v, induction v with a b, + exact ap (dpair _) (respect_pt (g a)), + exact sigma_eq (respect_pt f) !pathover_tr }, + { intro v, induction v with a b: reflexivity } + end + + definition dsmash_functor_homotopy_pushout_functor (f : A →* C) (g : Πa, B a →* D (f a)) : + f ⋀→ g ~ dsmash_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, apply ap_compose }, + { apply eq_pathover, refine !elim_gluer ⬝ph _ ⬝hp !pushout.elim_glue⁻¹, + apply hdeg_square, reflexivity } + end + + definition dsmash_pequiv [constructor] (f : A ≃* C) (g : Πa, B a ≃* D (f a)) : ⋀ B ≃* ⋀ D := + begin + fapply pequiv_of_pmap (f ⋀→ g), + refine homotopy_closed _ (dsmash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ _, + apply pushout.is_equiv_functor, + { apply is_equiv_sum_functor, apply is_equiv_compose, apply pequiv.to_is_equiv, + exact to_is_equiv (equiv_ap _ _) }, + apply is_equiv_sigma_functor, intro a, apply pequiv.to_is_equiv + end + + infixr ` ⋀≃ `:80 := dsmash_pequiv + + definition dsmash_pequiv_left [constructor] (B : C → Type*) (f : A ≃* C) : + ⋀ (B ∘ f) ≃* ⋀ B := + f ⋀≃ λa, pequiv.rfl + + definition dsmash_pequiv_right [constructor] {D : A → Type*} (g : Πa, B a ≃* D a) : ⋀ B ≃* ⋀ D := + pequiv.rfl ⋀≃ g + + /- f ∧ g is constant if f is constant -/ + -- definition dsmash_functor_pconst_left_homotopy [unfold 6] {B' : Type} (f : B → B') (x : ⋀ B) : + -- (pconst A C ⋀→ pmap_of_map f pt) x = pt := + -- begin + -- induction x with a b a b, + -- { exact gluer' (f b) pt }, + -- { exact (gluel pt)⁻¹ }, + -- { exact (gluer pt)⁻¹ᵖ }, + -- { apply eq_pathover, note x := functor_gluel2 (λx : A, Point A') f a, + -- refine x ⬝ph _, refine _ ⬝hp !ap_constant⁻¹, apply square_of_eq, + -- rexact con.right_inv (gluer (f pt)) ⬝ (con.right_inv (gluel pt))⁻¹ }, + -- { apply eq_pathover, note x := functor_gluer2 (λx : A, Point A') f b, + -- refine x ⬝ph _, refine _ ⬝hp !ap_constant⁻¹, apply square_of_eq, reflexivity } + -- end + + -- definition dsmash_functor_pconst_left (f : B →* B') : pconst A A' ⋀→ f ~* pconst (⋀ B) (A' ∧ B') := + -- begin + -- induction B' with B', induction f with f f₀, esimp at *, induction f₀, + -- fapply phomotopy.mk, + -- { exact dsmash_functor_pconst_left_homotopy f }, + -- { rexact con.right_inv (gluer (f pt)) } + -- end + + -- definition dsmash_functor_pconst_left_phomotopy {f f' : B →* B'} (p : f ~* f') : + -- phomotopy.refl (pconst A A') ⋀~ p ⬝* dsmash_functor_pconst_left f' = dsmash_functor_pconst_left f := + -- begin + -- induction p using phomotopy_rec_idp, + -- exact !dsmash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans + -- end + + -- /- This makes dsmash_functor into a pointed map (B →* B') →* (⋀ B →* ⋀ B') -/ + + -- definition dsmash_functor_left [constructor] (A A' B : Type*) : + -- ppmap A A' →* ppmap (⋀ B) (A' ∧ B) := + -- pmap.mk (λf, f ⋀→ pid B) (eq_of_phomotopy (dsmash_functor_pconst_left (pid B))) + + /- We want to show that dsmash_functor_left is natural in A, B and C. + + For this we need two coherence rules. Given the function h := (f' ∘ f) ⋀→ (g' ∘ g) and suppose + that either f' or f 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 f 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 {B C : Type} {g : B → C} {fa₁ fa₂ b₀ : B} + -- {pa₁ : fa₁ = b₀} {pa₂ : fa₂ = b₀} {qa₁ : g (fa₁) = g b₀} {qa₂ : g (fa₂) = g b₀} + -- (ra₁ : ap g (pa₁) = qa₁) (ra₂ : ap g (pa₂) = qa₂) : + -- cube (hrfl ⬝hp (ra₁)⁻¹) hrfl + -- (my_squarel (qa₁) (qa₂)) (aps g (my_squarel (pa₁) (pa₂))) + -- (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (ra₁) ◾ (ra₂)⁻²)⁻¹) + -- (hrfl ⬝hp (ra₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) := + -- begin + -- induction ra₂, induction ra₁, induction pa₂, induction pa₁, 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 dsmash_functor_pcompose_pconst2_homotopy {A A' A'' B B' B'' : Type} + -- (a₀ : A) (b₀ : B) (a₀' : A') (f' : A' → A'') (g' : B' → B'') (g : B → B') + -- (x : pointed.MK A a₀ ∧ pointed.MK B b₀) : + -- square (dsmash_functor_pcompose_homotopy f' (λ a, a₀') g' g x) + -- idp + -- (dsmash_functor_pconst_left_homotopy (λ a, g' (g a)) x) + -- (ap (dsmash_functor' (pmap.mk f' (refl (f' a₀'))) (pmap.mk g' (refl (g' (g b₀))))) + -- (dsmash_functor_pconst_left_homotopy g x)) := + -- begin + -- induction x with a b a b, + -- { refine _ ⬝hp (functor_gluer'2 f' g' (g b) (g b₀))⁻¹, 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_fillerr 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_fillerl end end } + -- end + + -- definition dsmash_functor_pcompose_pconst2 (f' : A' →* A'') (g' : B' →* B'') (g : B →* B') : + -- phsquare (dsmash_functor_pcompose f' (pconst A A') g' g) + -- (dsmash_functor_pconst_left (g' ∘* g)) + -- (dsmash_functor_phomotopy (pcompose_pconst f') phomotopy.rfl) + -- (pwhisker_left (f' ⋀→ g') (dsmash_functor_pconst_left g) ⬝* + -- pcompose_pconst (f' ⋀→ g')) := + -- begin + -- induction A with A a₀, induction B with B b₀, + -- induction A' with A' a₀', induction B' with B' b₀', + -- induction A'' with A'' a₀'', induction B'' with B'' b₀'', + -- induction f' with f' f'₀, induction g' with g' g₀', induction g with g g₀, + -- esimp at *, induction f'₀, induction g₀', induction g₀, + -- refine !dsmash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, + -- fapply phomotopy_eq, + -- { intro x, refine eq_of_square _ ⬝ !con_idp, + -- exact dsmash_functor_pcompose_pconst2_homotopy a₀ b₀ a₀' f' g' 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, + -- refine whisker_right _ _ ⬝ _, rotate 1, rexact functor_gluer'2_same f' g' (g b₀), + -- refine !inv_con_cancel_right ⬝ _, + -- refine !whisker_left_idp⁻¹ ⬝ _, + -- refine !con_idp ⬝ _, + -- apply whisker_left, + -- apply ap (whisker_left idp), + -- exact (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹ } + -- end + + -- /- a version where the left maps are identities -/ + -- definition dsmash_functor_pcompose_pconst2_pid (f' : A' →* A'') : + -- phsquare (dsmash_functor_pcompose_pid B f' (pconst A A')) + -- (dsmash_functor_pconst_left (pid B)) + -- (pcompose_pconst f' ⋀~ phomotopy.rfl) + -- (pwhisker_left (f' ⋀→ pid B) (dsmash_functor_pconst_left (pid B)) ⬝* + -- pcompose_pconst (f' ⋀→ pid B)) := + -- (!dsmash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** + -- dsmash_functor_pcompose_pconst2 f' (pid B) (pid B) + + -- /- a small rewrite of the previous -/ + -- -- definition dsmash_functor_pcompose_pid_pconst' (f' : A' →* A'') : + -- -- pwhisker_left (f' ⋀→ pid B) (dsmash_functor_pconst_left (pid B)) ⬝* + -- -- pcompose_pconst (f' ⋀→ pid B) = + -- -- (dsmash_functor_pcompose_pid B f' (pconst A A'))⁻¹* ⬝* + -- -- (pcompose_pconst f' ⋀~ phomotopy.rfl ⬝* + -- -- dsmash_functor_pconst_left (pid B)) := + -- -- begin + -- -- apply eq_symm_trans_of_trans_eq, + -- -- exact dsmash_functor_pcompose_pid_pconst f' + -- -- end + + -- /- if f' is constant -/ + -- definition dsmash_functor_pcompose_pconst1_homotopy [unfold 13] {A A' A'' B B' B'' : Type} + -- (a₀ : A) (b₀ : B) (a₀'' : A'') (f : A → A') (g' : B' → B'') (g : B → B') + -- (x : pointed.MK A a₀ ∧ pointed.MK B b₀) : + -- square (dsmash_functor_pcompose_homotopy (λa', a₀'') f g' g x) + -- idp + -- (dsmash_functor_pconst_left_homotopy (λ a, g' (g a)) x) + -- (dsmash_functor_pconst_left_homotopy g' + -- ((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 (dsmash_functor_pconst_left_homotopy g') _ _)⁻¹ᵖ, + -- 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 (dsmash_functor_pconst_left_homotopy g') _ _)⁻¹ᵖ, + -- 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 dsmash_functor_pcompose_pconst1 (f : A →* A') (g' : B' →* B'') (g : B →* B') : + -- phsquare (dsmash_functor_pcompose (pconst A' A'') f g' g) + -- (dsmash_functor_pconst_left (g' ∘* g)) + -- (pconst_pcompose f ⋀~ phomotopy.rfl) + -- (pwhisker_right (f ⋀→ g) (dsmash_functor_pconst_left g') ⬝* + -- pconst_pcompose (f ⋀→ g)) := + -- begin + -- induction A with A a₀, induction B with B b₀, + -- induction A' with A' a₀', induction B' with B' b₀', + -- induction A'' with A'' a₀'', induction B'' with B'' b₀'', + -- induction f with f f₀, induction g' with g' g₀', induction g with g g₀, + -- esimp at *, induction f₀, induction g₀', induction g₀, + -- refine !dsmash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, + -- fapply phomotopy_eq, + -- { intro x, refine eq_of_square (dsmash_functor_pcompose_pconst1_homotopy a₀ b₀ a₀'' f g' 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 (gluer (g' (g b₀))) } + -- end + + -- /- a version where the left maps are identities -/ + -- definition dsmash_functor_pcompose_pconst1_pid (f : A →* A') : + -- phsquare (dsmash_functor_pcompose_pid B (pconst A' A'') f) + -- (dsmash_functor_pconst_left (pid B)) + -- (pconst_pcompose f ⋀~ phomotopy.rfl) + -- (pwhisker_right (f ⋀→ pid B) (dsmash_functor_pconst_left (pid B)) ⬝* + -- pconst_pcompose (f ⋀→ pid B)) := + -- (!dsmash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** + -- dsmash_functor_pcompose_pconst1 f (pid B) (pid B) + + -- /- Using these lemmas we show that dsmash_functor_left is natural in all arguments -/ + + -- definition dsmash_functor_left_natural_left (B C : Type*) (f : A' →* A) : + -- psquare (dsmash_functor_left A B C) (dsmash_functor_left A' B C) + -- (ppcompose_right f) (ppcompose_right (f ⋀→ pid C)) := + -- begin + -- refine _⁻¹*, + -- fapply phomotopy_mk_ppmap, + -- { intro g, exact dsmash_functor_pcompose_pid C g f }, + -- { refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ + -- !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , + -- refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !dsmash_functor_eq_of_phomotopy_left ⬝ + -- !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + -- apply dsmash_functor_pcompose_pconst1_pid } + -- end + + -- definition dsmash_functor_left_natural_middle (A C : Type*) (f : B →* B') : + -- psquare (dsmash_functor_left A B C) (dsmash_functor_left A B' C) + -- (ppcompose_left f) (ppcompose_left (f ⋀→ pid C)) := + -- begin + -- refine _⁻¹*, + -- fapply phomotopy_mk_ppmap, + -- { exact dsmash_functor_pcompose_pid C 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) ⬝ _ , + -- refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !dsmash_functor_eq_of_phomotopy_left ⬝ + -- !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + -- apply dsmash_functor_pcompose_pconst2_pid } + -- end + + -- definition dsmash_functor_left_natural_right (A B : Type*) (f : C →* C') : + -- psquare (dsmash_functor_left A B C) (ppcompose_right (pid A ⋀→ f)) + -- (dsmash_functor_left A B C') (ppcompose_left (pid B ⋀→ f)) := + -- begin + -- refine _⁻¹*, + -- fapply phomotopy_mk_ppmap, + -- { intro g, exact dsmash_functor_psquare proof phomotopy.rfl qed proof phomotopy.rfl qed }, + -- { 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) ⬝ _ , + -- refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ + -- !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + -- apply eq_of_phsquare, + -- refine (phmove_bot_of_left _ !dsmash_functor_pcompose_pconst1⁻¹ʰ**) ⬝h** + -- (!dsmash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !dsmash_functor_pcompose_pconst2 ⬝vp** _, + -- refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl, + -- refine idp ◾** !refl_trans ⬝ !trans_left_inv } + -- end + + -- definition dsmash_functor_left_natural_middle_phomotopy (A C : Type*) {f f' : B →* B'} + -- (p : f ~* f') : dsmash_functor_left_natural_middle A C f = + -- ppcompose_left_phomotopy p ⬝ph* dsmash_functor_left_natural_middle A C f' ⬝hp* + -- ppcompose_left_phomotopy (p ⋀~ phomotopy.rfl) := + -- begin + -- induction p using phomotopy_rec_idp, + -- symmetry, + -- refine !ppcompose_left_phomotopy_refl ◾ph* idp ◾hp* + -- (ap ppcompose_left_phomotopy !dsmash_functor_phomotopy_refl ⬝ + -- !ppcompose_left_phomotopy_refl) ⬝ _, + -- exact !rfl_phomotopy_hconcat ⬝ !hconcat_phomotopy_rfl + -- end + + -- /- the following is not really used, but a symmetric version of the natural equivalence + -- dsmash_functor_left -/ + -- /- f ∧ g is constant if g is constant -/ + -- definition dsmash_functor_pconst_right_homotopy [unfold 6] {C : Type} (f : A → C) (x : ⋀ 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 dsmash_functor_pconst_right (f : A →* C) : + -- f ⋀→ (pconst B D) ~* pconst (⋀ B) (⋀ D) := + -- begin + -- induction C with C, induction f with f f₀, esimp at *, induction f₀, + -- fapply phomotopy.mk, + -- { exact dsmash_functor_pconst_right_homotopy f }, + -- { rexact con.right_inv (gluel (f pt)) } + -- end + + -- definition dsmash_functor_pconst_right_phomotopy {f f' : A →* C} (p : f ~* f') : + -- dsmash_functor_phomotopy p (phomotopy.refl (pconst B D)) ⬝* dsmash_functor_pconst_right f' = + -- dsmash_functor_pconst_right f := + -- begin + -- induction p using phomotopy_rec_idp, + -- exact !dsmash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans + -- end + + -- /- This makes dsmash_functor into a pointed map (B →* B') →* (⋀ B →* ⋀ B') -/ + + -- definition dsmash_functor_right [constructor] (B : A → Type*) (C : Type*) : + -- ppmap B C →* ppmap (⋀ B) (A ∧ C) := + -- pmap.mk (dsmash_functor (pid A)) (eq_of_phomotopy (dsmash_functor_pconst_right (pid A))) + + -- /- We want to show that dsmash_functor_right is natural in A, B and C. + + -- For this we need two coherence rules. 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 -/ + + -- definition dsmash_functor_pcompose_pconst4_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 (dsmash_functor_pcompose_homotopy f' f g (λ a, d₀) x) + -- idp + -- (dsmash_functor_pconst_right_homotopy (λ a, f' (f a)) x) + -- (ap (dsmash_functor' (pmap.mk f' (refl (f' (f a₀)))) (pmap.mk g (refl (g d₀)))) + -- (dsmash_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 dsmash_functor_pcompose_pconst4 (f' : C →* E) (f : A →* C) (g : D →* F) : + -- phsquare (dsmash_functor_pcompose f' f g (pconst B D)) + -- (dsmash_functor_pconst_right (f' ∘* f)) + -- (dsmash_functor_phomotopy phomotopy.rfl (pcompose_pconst g)) + -- (pwhisker_left (f' ⋀→ g) (dsmash_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 !dsmash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, + -- fapply phomotopy_eq, + -- { intro x, refine eq_of_square _ ⬝ !con_idp, + -- exact dsmash_functor_pcompose_pconst4_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, + -- refine whisker_right _ _ ⬝ _, rotate 1, rexact functor_gluel'2_same f' g (f a₀), + -- refine !inv_con_cancel_right ⬝ _, + -- refine !whisker_left_idp⁻¹ ⬝ _, + -- refine !con_idp ⬝ _, + -- apply whisker_left, + -- apply ap (whisker_left idp), + -- exact (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹ } + -- end + + -- /- a version where the left maps are identities -/ + -- definition dsmash_functor_pcompose_pconst4_pid (g : D →* F) : + -- phsquare (dsmash_functor_pid_pcompose A g (pconst B D)) + -- (dsmash_functor_pconst_right (pid A)) + -- (dsmash_functor_phomotopy phomotopy.rfl (pcompose_pconst g)) + -- (pwhisker_left (pid A ⋀→ g) (dsmash_functor_pconst_right (pid A)) ⬝* + -- pcompose_pconst (pid A ⋀→ g)) := + -- (!dsmash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** + -- dsmash_functor_pcompose_pconst4 (pid A) (pid A) g + + -- /- a small rewrite of the previous -/ + -- -- definition dsmash_functor_pid_pcompose_pconst' (g : D →* F) : + -- -- pwhisker_left (pid A ⋀→ g) (dsmash_functor_pconst_right (pid A)) ⬝* + -- -- pcompose_pconst (pid A ⋀→ g) = + -- -- (dsmash_functor_pid_pcompose A g (pconst B D))⁻¹* ⬝* + -- -- (dsmash_functor_phomotopy phomotopy.rfl (pcompose_pconst g) ⬝* + -- -- dsmash_functor_pconst_right (pid A)) := + -- -- begin + -- -- apply eq_symm_trans_of_trans_eq, + -- -- exact dsmash_functor_pid_pcompose_pconst g + -- -- end + + -- /- if g' is constant -/ + -- definition dsmash_functor_pcompose_pconst3_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 (dsmash_functor_pcompose_homotopy f' f (λ a, x₀) g x) + -- idp + -- (dsmash_functor_pconst_right_homotopy (λ a, f' (f a)) x) + -- (dsmash_functor_pconst_right_homotopy f' + -- (dsmash_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 (dsmash_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 (dsmash_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 dsmash_functor_pcompose_pconst3 (f' : C →* E) (f : A →* C) (g : Πa, B a →* D (f a)) : + -- phsquare (dsmash_functor_pcompose f' f (pconst D F) g) + -- (dsmash_functor_pconst_right (f' ∘* f)) + -- (dsmash_functor_phomotopy phomotopy.rfl (pconst_pcompose g)) + -- (pwhisker_right (f ⋀→ g) (dsmash_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 !dsmash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, + -- fapply phomotopy_eq, + -- { intro x, refine eq_of_square (dsmash_functor_pcompose_pconst3_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 version where the left maps are identities -/ + -- definition dsmash_functor_pcompose_pconst3_pid (g : Πa, B a →* D (f a)) : + -- phsquare (dsmash_functor_pid_pcompose A (pconst D F) g) + -- (dsmash_functor_pconst_right (pid A)) + -- (dsmash_functor_phomotopy phomotopy.rfl (pconst_pcompose g)) + -- (pwhisker_right (pid A ⋀→ g) (dsmash_functor_pconst_right (pid A)) ⬝* + -- pconst_pcompose (pid A ⋀→ g)) := + -- (!dsmash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** + -- dsmash_functor_pcompose_pconst3 (pid A) (pid A) g + + -- /- Using these lemmas we show that dsmash_functor_right is natural in all arguments -/ + -- definition dsmash_functor_right_natural_right (A B : Type*) (f : C →* C') : + -- psquare (dsmash_functor_right A B C) (dsmash_functor_right A B C') + -- (ppcompose_left f) (ppcompose_left (pid A ⋀→ f)) := + -- begin + -- refine _⁻¹*, + -- fapply phomotopy_mk_ppmap, + -- { exact dsmash_functor_pid_pcompose A 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) ⬝ _ , + -- refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !dsmash_functor_eq_of_phomotopy ⬝ + -- !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + -- apply dsmash_functor_pcompose_pconst4_pid } + -- end + + -- definition dsmash_functor_right_natural_middle (A C : Type*) (f : B' →* B) : + -- psquare (dsmash_functor_right A B C) (dsmash_functor_right A B' C) + -- (ppcompose_right f) (ppcompose_right (pid A ⋀→ f)) := + -- begin + -- refine _⁻¹*, + -- fapply phomotopy_mk_ppmap, + -- { intro g, exact dsmash_functor_pid_pcompose A g f }, + -- { refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ + -- !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , + -- refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !dsmash_functor_eq_of_phomotopy ⬝ + -- !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + -- apply dsmash_functor_pcompose_pconst3_pid } + -- end + + -- definition dsmash_functor_right_natural_left (B C : Type*) (f : A →* A') : + -- psquare (dsmash_functor_right A B C) (ppcompose_right (f ⋀→ (pid B))) + -- (dsmash_functor_right A' B C) (ppcompose_left (f ⋀→ (pid C))) := + -- begin + -- refine _⁻¹*, + -- fapply phomotopy_mk_ppmap, + -- { intro g, exact dsmash_functor_psquare proof phomotopy.rfl qed proof phomotopy.rfl qed }, + -- { 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) ⬝ _ , + -- refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ + -- !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + -- apply eq_of_phsquare, + -- refine (phmove_bot_of_left _ !dsmash_functor_pcompose_pconst3⁻¹ʰ**) ⬝h** + -- (!dsmash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !dsmash_functor_pcompose_pconst4 ⬝vp** _, + -- refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl, + -- refine idp ◾** !refl_trans ⬝ !trans_left_inv } + -- end + + -- /- ⋀ B ≃* pcofiber (pprod_of_wedge A B) -/ + + -- variables (A B) + -- open pushout + + -- definition dsmash_equiv_cofiber : ⋀ B ≃ cofiber (@prod_of_wedge A B) := + -- begin + -- unfold [dsmash, cofiber, dsmash'], symmetry, + -- fapply pushout_vcompose_equiv wedge_of_sum, + -- { symmetry, refine equiv_unit_of_is_contr _ _, apply is_contr_pushout_wedge_of_sum }, + -- { intro x, reflexivity }, + -- { apply prod_of_wedge_of_sum } + -- end + + -- definition dsmash_punit_pequiv [constructor] : dsmash A punit ≃* punit := + -- begin + -- apply pequiv_punit_of_is_contr, + -- apply is_contr.mk (dsmash.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_wedge [constructor] : wedge A B →* A ×* B := + -- begin + -- fconstructor, + -- { exact prod_of_wedge }, + -- { reflexivity } + -- end + + -- definition dsmash_pequiv_pcofiber [constructor] : ⋀ B ≃* pcofiber (pprod_of_wedge A B) := + -- begin + -- apply pequiv_of_equiv (dsmash_equiv_cofiber A B), + -- exact cofiber.glue pt + -- end + + -- variables {A B} + + -- /- commutativity -/ + + -- definition dsmash_flip' [unfold 3] (x : ⋀ B) : dsmash B A := + -- begin + -- induction x, + -- { exact dsmash.mk b a }, + -- { exact auxr }, + -- { exact auxl }, + -- { exact gluer a }, + -- { exact gluel b } + -- end + + -- definition dsmash_flip_dsmash_flip' [unfold 3] (x : ⋀ B) : dsmash_flip' (dsmash_flip' x) = x := + -- begin + -- induction x, + -- { reflexivity }, + -- { reflexivity }, + -- { reflexivity }, + -- { apply eq_pathover_id_right, + -- refine ap_compose dsmash_flip' _ _ ⬝ ap02 _ !elim_gluel ⬝ !elim_gluer ⬝ph _, + -- apply hrfl }, + -- { apply eq_pathover_id_right, + -- refine ap_compose dsmash_flip' _ _ ⬝ ap02 _ !elim_gluer ⬝ !elim_gluel ⬝ph _, + -- apply hrfl } + -- end + + -- variables (A B) + + -- definition dsmash_flip [constructor] : ⋀ B →* dsmash B A := + -- pmap.mk dsmash_flip' idp + + -- definition dsmash_flip_dsmash_flip [constructor] : + -- dsmash_flip B A ∘* dsmash_flip A B ~* pid (⋀ B) := + -- phomotopy.mk dsmash_flip_dsmash_flip' idp + + -- definition dsmash_comm [constructor] : ⋀ B ≃* dsmash B A := + -- begin + -- apply pequiv.MK, do 2 apply dsmash_flip_dsmash_flip + -- end + + -- variables {A B} + -- definition dsmash_flip_dsmash_functor' [unfold 7] (f : A →* C) (g : Πa, B a →* D (f a)) : hsquare + -- dsmash_flip' dsmash_flip' (dsmash_functor' f g) (dsmash_functor' g f) := + -- begin + -- intro x, induction x, + -- { reflexivity }, + -- { reflexivity }, + -- { reflexivity }, + -- { apply eq_pathover, + -- refine ap_compose (dsmash_functor' _ _) _ _ ⬝ ap02 _ !elim_gluel ⬝ !functor_gluer ⬝ph _ + -- ⬝hp (ap_compose dsmash_flip' _ _ ⬝ ap02 _ !functor_gluel)⁻¹ᵖ, + -- refine _ ⬝hp (!ap_con ⬝ !ap_compose' ◾ !elim_gluel)⁻¹, exact hrfl }, + -- { apply eq_pathover, + -- refine ap_compose (dsmash_functor' _ _) _ _ ⬝ ap02 _ !elim_gluer ⬝ !functor_gluel ⬝ph _ + -- ⬝hp (ap_compose dsmash_flip' _ _ ⬝ ap02 _ !functor_gluer)⁻¹ᵖ, + -- refine _ ⬝hp (!ap_con ⬝ !ap_compose' ◾ !elim_gluer)⁻¹, exact hrfl }, + -- end + + -- definition dsmash_flip_dsmash_functor (f : A →* C) (g : Πa, B a →* D (f a)) : + -- psquare (dsmash_flip A B) (dsmash_flip C D) (f ⋀→ g) (g ⋀→ f) := + -- begin + -- apply phomotopy.mk (dsmash_flip_dsmash_functor' f g), refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, + -- refine !ap_ap011 ⬝ _, apply ap011_flip, + -- end + + definition pinr [constructor] (B : A → Type*) (a : A) : B a →* ⋀ B := + begin + fapply pmap.mk, + { intro b, exact dsmash.mk a b }, + { exact gluel' a pt } + end + + definition pinl [constructor] (b : Πa, B a) : A →* ⋀ B := + begin + fapply pmap.mk, + { intro a, exact dsmash.mk a (b a) }, + { exact gluer' (b pt) pt } + end + + -- definition pinr_phomotopy {a a' : A} (p : a = a') : pinr B a ~* pinr B a' := + -- begin + -- fapply phomotopy.mk, + -- { exact ap010 (pmap.to_fun ∘ pinr B) p }, + -- { induction p, apply idp_con } + -- end + + definition dsmash_pmap_unit_pt [constructor] (B : A → Type*) : pinr B pt ~* pconst (B pt) (⋀ B) := + begin + fapply phomotopy.mk, + { intro b, exact gluer' b pt }, + { rexact con.right_inv (gluer pt) ⬝ (con.right_inv (gluel pt))⁻¹ } + end + + definition dsmash_pmap_unit [constructor] (B : A → Type*) : Π*(a : A), B a →** ⋀ B := + begin + fapply ppi.mk, + { exact pinr B }, + { apply eq_of_phomotopy, exact dsmash_pmap_unit_pt B } + end + + /- The unit is natural in the first argument -/ + definition dsmash_functor_pid_pinr' [constructor] (B : A' → Type*) (f : A →* A') (a : A) : + pinr B (f a) ~* (f ⋀→ λa, !pid) ∘* pinr (B ∘ f) a := + begin + fapply phomotopy.mk, + { intro b, reflexivity }, + { refine !idp_con ⬝ _, + induction A' with A' a₀', induction f with f f₀, esimp at *, + induction f₀, exact sorry } + end + + -- definition dsmash_pmap_unit_pt_natural [constructor] (B : A → Type*) (f : A →* A') : + -- dsmash_functor_pid_pinr' B f pt ⬝* + -- pwhisker_left (f ⋀→ λa, !pid) (dsmash_pmap_unit_pt A B) ⬝* + -- pcompose_pconst (f ⋀→ λa, !pid) = + -- _ /-pinr_phomotopy (respect_pt f)-/ ⬝* dsmash_pmap_unit_pt A' B := + -- begin + -- induction f with f f₀, induction A' with A' a₀', esimp at *, + -- induction f₀, refine _ ⬝ !refl_trans⁻¹, + -- refine !trans_refl ⬝ _, + -- fapply phomotopy_eq', + -- { intro b, refine !idp_con ⬝ _, + -- rexact functor_gluer'2 f (pid B) b pt }, + -- { refine whisker_right_idp _ ⬝ph _, + -- refine ap (λx, _ ⬝ x) _ ⬝ph _, + -- rotate 1, rexact (functor_gluer'2_same f (pid B) pt), + -- refine whisker_right _ !idp_con ⬝pv _, + -- refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, + -- refine whisker_left _ !to_homotopy_pt_mk ⬝pv _, + -- refine !con.assoc⁻¹ ⬝ whisker_right _ _ ⬝pv _, + -- rotate 1, esimp, apply whisker_left_idp_con, + -- refine !con.assoc ⬝pv _, apply whisker_tl, + -- refine whisker_right _ !idp_con ⬝pv _, + -- refine whisker_right _ !whisker_right_idp ⬝pv _, + -- refine whisker_right _ (!idp_con ⬝ !ap02_con) ⬝ !con.assoc ⬝pv _, + -- apply whisker_tl, + -- apply vdeg_square, + -- refine whisker_right _ !ap_inv ⬝ _, apply inv_con_eq_of_eq_con, + -- rexact functor_gluel'2_same (pmap_of_map f pt) (pmap_of_map id (Point B)) pt } + -- end + + -- definition dsmash_pmap_unit_natural (B : A' → Type*) (f : A →* A') : + -- psquare (dsmash_pmap_unit (B ∘ f)) (dsmash_pmap_unit B) f _ := --(ppcompose_left (f ⋀→ pid B)) + -- begin + -- apply ptranspose, + -- induction A with A a₀, induction B with B b₀, induction A' with A' a₀', + -- induction f with f f₀, esimp at *, induction f₀, fapply phomotopy_mk_ppmap, + -- { intro a, exact dsmash_functor_pid_pinr' _ (pmap_of_map f a₀) a }, + -- { refine ap (λx, _ ⬝* phomotopy_of_eq x) !respect_pt_pcompose ⬝ _ + -- ⬝ 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_left_eq_of_phomotopy ⬝ _, + -- refine ap (λx, _ ⬝* x) (!phomotopy_of_eq_con ⬝ + -- !phomotopy_of_eq_of_phomotopy ◾** !phomotopy_of_eq_of_phomotopy ⬝ !trans_refl) ⬝ _, + -- refine _ ⬝ dsmash_pmap_unit_pt_natural _ (pmap_of_map f a₀) ⬝ _, + -- { exact !trans_refl⁻¹ }, + -- { exact !refl_trans }} + -- end + + + /- The unit is also dinatural in the first argument, but that's easier to prove after the adjunction. + We don't need it for the adjunction -/ + + /- The unit-counit laws -/ + -- definition dsmash_pmap_unit_counit (B : A → Type*) : + -- dsmash_pmap_counit B (⋀ B) ∘* dsmash_pmap_unit A B ⋀→ pid B ~* pid (⋀ B) := + -- begin + -- fapply phomotopy.mk, + -- { intro x, + -- induction x with a b a b, + -- { reflexivity }, + -- { exact gluel pt }, + -- { exact gluer pt }, + -- { apply eq_pathover_id_right, + -- refine ap_compose dsmash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ph _, + -- refine !ap_con ⬝ !ap_compose' ◾ !elim_gluel ⬝ph _, + -- refine !idp_con ⬝ph _, + -- apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ }, + -- { apply eq_pathover_id_right, + -- refine ap_compose dsmash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ph _, + -- refine !ap_con ⬝ !ap_compose' ◾ !elim_gluer ⬝ph _, + -- refine !ap_eq_of_phomotopy ⬝ph _, + -- apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ }}, + -- { refine _ ⬝ !ap_compose, refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, + -- rexact (con.right_inv (gluel pt))⁻¹ } + -- end + + -- definition dsmash_pmap_counit_unit_pt [constructor] (f : A →* B) : + -- dsmash_pmap_counit A B ∘* pinr A f ~* f := + -- begin + -- fapply phomotopy.mk, + -- { intro a, reflexivity }, + -- { refine !idp_con ⬝ !elim_gluel'⁻¹ } + -- end + + -- definition dsmash_pmap_counit_unit (B : A → Type*) : + -- ppcompose_left (dsmash_pmap_counit A B) ∘* dsmash_pmap_unit (ppmap A B) A ~* pid (ppmap A B) := + -- begin + -- fapply phomotopy_mk_ppmap, + -- { intro f, exact dsmash_pmap_counit_unit_pt f }, + -- { refine !trans_refl ⬝ _, + -- refine _ ⬝ ap (λx, phomotopy_of_eq (x ⬝ _)) !pcompose_left_eq_of_phomotopy⁻¹, + -- refine _ ⬝ !phomotopy_of_eq_con⁻¹, + -- refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ ◾** !phomotopy_of_eq_of_phomotopy⁻¹, + -- refine _ ⬝ !trans_refl⁻¹, + -- fapply phomotopy_eq, + -- { intro a, esimp, refine !elim_gluer'⁻¹ }, + -- { esimp, refine whisker_right _ !whisker_right_idp ⬝ _ ⬝ !idp_con⁻¹, + -- refine whisker_right _ !elim_gluer'_same⁻² ⬝ _ ⬝ !elim_gluel'_same⁻¹⁻², + -- apply inv_con_eq_of_eq_con, refine !idp_con ⬝ _, esimp, + -- refine _ ⬝ !ap02_con ⬝ whisker_left _ !ap_inv, + -- refine !whisker_right_idp ⬝ _, + -- exact !idp_con }} + -- end + + /- The underlying (unpointed) functions of the equivalence A →* (B →* C) ≃* ⋀ B →* C) -/ + -- definition dsmash_elim [constructor] (f : Π*(a : A), ppmap (B a) C) : ⋀ B →* C := + -- smash.smash_pmap_counit _ C ∘* _ /-f ⋀→ pid B_-/ + + -- definition dsmash_elim_inv [constructor] (g : ⋀ B →* C) : A →* ppmap B C := + -- ppcompose_left g ∘* dsmash_pmap_unit A B + + -- /- They are inverses, constant on the constant function and natural -/ + -- definition dsmash_elim_left_inv (f : A →* ppmap B C) : dsmash_elim_inv (dsmash_elim f) ~* f := + -- begin + -- refine !pwhisker_right !ppcompose_left_pcompose ⬝* _, + -- refine !passoc ⬝* _, + -- refine !pwhisker_left !dsmash_pmap_unit_natural ⬝* _, + -- refine !passoc⁻¹* ⬝* _, + -- refine !pwhisker_right !dsmash_pmap_counit_unit ⬝* _, + -- apply pid_pcompose + -- end + + -- definition dsmash_elim_right_inv (g : ⋀ B →* C) : dsmash_elim (dsmash_elim_inv g) ~* g := + -- begin + -- refine !pwhisker_left !dsmash_functor_pcompose_pid ⬝* _, + -- refine !passoc⁻¹* ⬝* _, + -- refine !pwhisker_right !dsmash_pmap_counit_natural_right⁻¹* ⬝* _, + -- refine !passoc ⬝* _, + -- refine !pwhisker_left !dsmash_pmap_unit_counit ⬝* _, + -- apply pcompose_pid + -- end + + -- definition dsmash_elim_pconst (B : A → Type*) (C : Type*) : + -- dsmash_elim (pconst A (ppmap B C)) ~* pconst (⋀ B) C := + -- begin + -- refine pwhisker_left _ (dsmash_functor_pconst_left (pid B)) ⬝* !pcompose_pconst + -- end + + -- definition dsmash_elim_inv_pconst (B : A → Type*) (C : Type*) : + -- dsmash_elim_inv (pconst (⋀ B) C) ~* pconst A (ppmap B C) := + -- begin + -- fapply phomotopy_mk_ppmap, + -- { intro f, apply pconst_pcompose }, + -- { esimp, refine !trans_refl ⬝ _, + -- 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 + + -- definition dsmash_elim_natural_right (f : C →* C') (g : A →* ppmap B C) : + -- f ∘* dsmash_elim g ~* dsmash_elim (ppcompose_left f ∘* g) := + -- begin + -- refine _ ⬝* pwhisker_left _ !dsmash_functor_pcompose_pid⁻¹*, + -- refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc, + -- apply dsmash_pmap_counit_natural_right + -- end + + -- definition dsmash_elim_inv_natural_right {A B C C' : Type*} (f : C →* C') + -- (g : ⋀ B →* C) : ppcompose_left f ∘* dsmash_elim_inv g ~* dsmash_elim_inv (f ∘* g) := + -- begin + -- refine !passoc⁻¹* ⬝* pwhisker_right _ _, + -- exact !ppcompose_left_pcompose⁻¹* + -- end + + -- definition dsmash_elim_natural_left (f : A →* A') (g : B →* B') (h : A' →* ppmap B' C) : + -- dsmash_elim h ∘* (f ⋀→ g) ~* dsmash_elim (ppcompose_right g ∘* h ∘* f) := + -- begin + -- refine !dsmash_functor_pcompose_pid ⬝ph* _, + -- refine _ ⬝v* !dsmash_pmap_counit_natural_left, + -- refine dsmash_functor_psquare !pid_pcompose⁻¹* (phrefl g) + -- end + + -- definition dsmash_elim_phomotopy {f f' : A →* ppmap B C} (p : f ~* f') : + -- dsmash_elim f ~* dsmash_elim f' := + -- begin + -- apply pwhisker_left, + -- exact dsmash_functor_phomotopy p phomotopy.rfl + -- end + + -- definition dsmash_elim_inv_phomotopy {f f' : ⋀ B →* C} (p : f ~* f') : + -- dsmash_elim_inv f ~* dsmash_elim_inv f' := + -- pwhisker_right _ (ppcompose_left_phomotopy p) + + -- definition dsmash_elim_eq_of_phomotopy {f f' : A →* ppmap B C} (p : f ~* f') : + -- ap dsmash_elim (eq_of_phomotopy p) = eq_of_phomotopy (dsmash_elim_phomotopy p) := + -- begin + -- induction p using phomotopy_rec_idp, + -- refine ap02 _ !eq_of_phomotopy_refl ⬝ _, + -- refine !eq_of_phomotopy_refl⁻¹ ⬝ _, + -- apply ap eq_of_phomotopy, + -- refine _ ⬝ ap (pwhisker_left _) !dsmash_functor_phomotopy_refl⁻¹, + -- refine !pwhisker_left_refl⁻¹ + -- end + + -- definition dsmash_elim_inv_eq_of_phomotopy {f f' : ⋀ B →* C} (p : f ~* f') : + -- ap dsmash_elim_inv (eq_of_phomotopy p) = eq_of_phomotopy (dsmash_elim_inv_phomotopy p) := + -- begin + -- induction p using phomotopy_rec_idp, + -- refine ap02 _ !eq_of_phomotopy_refl ⬝ _, + -- refine !eq_of_phomotopy_refl⁻¹ ⬝ _, + -- apply ap eq_of_phomotopy, + -- refine _ ⬝ ap (pwhisker_right _) !ppcompose_left_phomotopy_refl⁻¹, + -- refine !pwhisker_right_refl⁻¹ + -- end + + /- The pointed maps of the equivalence A →* (B →* C) ≃* ⋀ B →* C -/ +-- definition dsmash_pelim : (Π*(a : A), ppmap (B a) C) →* ppmap (⋀ B) C := +-- ppcompose_left (smash.smash_pmap_counit (B pt) C) ∘* sorry +-- -- ppcompose_left (smash_pmap_counit B C) ∘* dsmash_functor_left A (ppmap B C) B + +-- open smash +-- definition smash_pelim_inv (B : A → Type*) (C : Type*) : +-- ppmap (A ∧ B) C →* ppmap A (ppmap B C) := +-- ppcompose_right (smash_pmap_unit A B) ∘* pppcompose B (A ∧ B) C + +-- -- definition smash_pelim_inv : ppmap (⋀ B) C →* Π*a, ppmap (B a) C := +-- -- _ ∘* pppcompose _ (⋀ B) C --ppcompose_right (smash_pmap_unit A B) ∘* pppcompose B (A ∧ B) C + +-- /- The forward function is natural in all three arguments -/ +-- definition dsmash_pelim_natural_left (B C : Type*) (f : A' →* A) : +-- psquare (dsmash_pelim A B C) (dsmash_pelim A' B C) +-- (ppcompose_right f) (ppcompose_right (f ⋀→ pid B)) := +-- dsmash_functor_left_natural_left (ppmap B C) B f ⬝h* !ppcompose_left_ppcompose_right + +-- definition dsmash_pelim_natural_middle (A C : Type*) (f : B' →* B) : +-- psquare (dsmash_pelim A B C) (dsmash_pelim A B' C) +-- (ppcompose_left (ppcompose_right f)) (ppcompose_right (pid A ⋀→ f)) := +-- pwhisker_tl _ !ppcompose_left_ppcompose_right ⬝* +-- (!dsmash_functor_left_natural_right⁻¹* ⬝pv* +-- dsmash_functor_left_natural_middle _ _ (ppcompose_right f) ⬝h* +-- ppcompose_left_psquare !dsmash_pmap_counit_natural_left) + +-- definition dsmash_pelim_natural_right (B : A → Type*) (f : C →* C') : +-- psquare (dsmash_pelim A B C) (dsmash_pelim A B C') +-- (ppcompose_left (ppcompose_left f)) (ppcompose_left f) := +-- dsmash_functor_left_natural_middle _ _ (ppcompose_left f) ⬝h* +-- ppcompose_left_psquare (dsmash_pmap_counit_natural_right _ f) + +-- definition dsmash_pelim_natural_lm (C : Type*) (f : A' →* A) (g : B' →* B) : +-- psquare (dsmash_pelim A B C) (dsmash_pelim A' B' C) +-- (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (f ⋀→ g)) := +-- dsmash_pelim_natural_left B C f ⬝v* dsmash_pelim_natural_middle A' C g ⬝hp* +-- ppcompose_right_phomotopy (dsmash_functor_split f g) ⬝* !ppcompose_right_pcompose + +-- definition dsmash_pelim_pid (B C : Type*) : +-- dsmash_pelim (ppmap B C) B C !pid ~* dsmash_pmap_counit B C := +-- pwhisker_left _ !dsmash_functor_pid ⬝* !pcompose_pid + +-- definition dsmash_pelim_inv_pid (B : A → Type*) : +-- dsmash_pelim_inv A B (⋀ B) !pid ~* dsmash_pmap_unit A B := +-- pwhisker_right _ !ppcompose_left_pid ⬝* !pid_pcompose + +-- /- The equivalence (note: the forward function of dsmash_adjoint_pmap is dsmash_pelim_inv) -/ +-- definition is_equiv_dsmash_elim [constructor] (B : A → Type*) (C : Type*) : is_equiv (@dsmash_elim A B C) := +-- begin +-- fapply adjointify, +-- { exact dsmash_elim_inv }, +-- { intro g, apply eq_of_phomotopy, exact dsmash_elim_right_inv g }, +-- { intro f, apply eq_of_phomotopy, exact dsmash_elim_left_inv f } +-- end + +-- definition dsmash_adjoint_pmap_inv [constructor] (B : A → Type*) (C : Type*) : +-- ppmap A (ppmap B C) ≃* ppmap (⋀ B) C := +-- pequiv_of_pmap (dsmash_pelim A B C) (is_equiv_dsmash_elim A B C) + + definition dsmash_pelim_fn_fn [constructor] (f : ⋀ B →* C) (a : A) : B a →* C := + pmap.mk (λb, f (dsmash.mk a b)) (ap f (gluel' a pt) ⬝ respect_pt f) + + definition dsmash_pelim_fn [constructor] (f : ⋀ B →* C) : dbpmap B (λa, C) := + begin + fapply dbpmap.mk (dsmash_pelim_fn_fn f), + { intro b, exact ap f (gluer' b pt) ⬝ respect_pt f }, + { apply whisker_right, apply ap02, exact !con.right_inv ⬝ !con.right_inv⁻¹ } + end + + definition dsmash_pelim_pmap [constructor] (B : A → Type*) (C : Type*) : + ppmap (⋀ B) C →* dbppmap B (λa, C) := + begin + apply pmap.mk dsmash_pelim_fn, + fapply dbpmap_eq, + { intro a, exact phomotopy.mk homotopy.rfl !ap_constant⁻¹ }, + { intro b, exact !ap_constant ⬝pv ids }, + { esimp, esimp [whisker_right], exact sorry } + end + + definition dsmash_pelim_pequiv [constructor] (B : A → Type*) (C : Type*) : + ppmap (⋀ B) C ≃* dbppmap B (λa, C) := + sorry + +set_option pp.binder_types true +open is_trunc + + /- we could also use pushout_arrow_equiv -/ + definition dsmash_arrow_equiv [constructor] (B : A → Type*) (C : Type) : + (⋀ B → C) ≃ Σ(f : Πa, B a → C) (c₁ : C) (c₀ : C), (Πa, f a pt = c₀) × (Πb, f pt b = c₁) := + begin + fapply equiv.MK, + { intro f, exact ⟨λa b, f (dsmash.mk a b), f auxr, f auxl, (λa, ap f (gluel a), λb, ap f (gluer b))⟩ }, + { intro x, exact dsmash.elim x.1 x.2.2.1 x.2.1 x.2.2.2.1 x.2.2.2.2 }, + { intro x, induction x with f x, induction x with c₁ x, induction x with c₀ x, induction x with p₁ p₂, + apply ap (dpair _), apply ap (dpair _), apply ap (dpair _), esimp, + exact pair_eq (eq_of_homotopy (elim_gluel _ _)) (eq_of_homotopy (elim_gluer _ _)) }, + { intro f, apply eq_of_homotopy, intro x, induction x, reflexivity, reflexivity, reflexivity, + apply eq_pathover, apply hdeg_square, apply elim_gluel, + apply eq_pathover, apply hdeg_square, apply elim_gluer } + end + + definition dsmash_arrow_equiv_inv_pt [constructor] + (x : Σ(f : Πa, B a → C) (c₁ : C) (c₀ : C), (Πa, f a pt = c₀) × (Πb, f pt b = c₁)) : + to_inv (dsmash_arrow_equiv B C) x pt = x.1 pt pt := + by reflexivity + + open pi + + definition dsmash_pelim_equiv (B : A → Type*) (C : Type*) : + ppmap (⋀ B) C ≃ dbppmap B (λa, C) := + begin + refine !pmap.sigma_char ⬝e _, + refine sigma_equiv_sigma_left !dsmash_arrow_equiv ⬝e _, + refine sigma_equiv_sigma_right (λx, equiv_eq_closed_left _ (dsmash_arrow_equiv_inv_pt x)) ⬝e _, + refine !sigma_assoc_equiv ⬝e _, + refine sigma_equiv_sigma_right (λf, !sigma_assoc_equiv ⬝e + sigma_equiv_sigma_right (λc₁, !sigma_assoc_equiv ⬝e + sigma_equiv_sigma_right (λc₂, sigma_equiv_sigma_left !sigma.equiv_prod⁻¹ᵉ ⬝e + !sigma_assoc_equiv) ⬝e + sigma_assoc_equiv_left _ (sigma_homotopy_constant_equiv pt (λa, f a pt))⁻¹ᵉ ⬝e + sigma_equiv_sigma_right (λh₁, !sigma_comm_equiv) ⬝e !sigma_comm_equiv) ⬝e + sigma_assoc_equiv_left _ (sigma_homotopy_constant_equiv pt (f pt))⁻¹ᵉ ⬝e + sigma_equiv_sigma_right (λh₂, + sigma_equiv_sigma_right (λr₂, + sigma_equiv_sigma_right (λh₁, !comm_equiv_nondep) ⬝e !sigma_comm_equiv) ⬝e + !sigma_comm_equiv) ⬝e + !sigma_comm_equiv ⬝e + sigma_equiv_sigma_right (λr, + sigma_equiv_sigma_left (pi_equiv_pi_right (λb, equiv_eq_closed_right _ r)) ⬝e + sigma_equiv_sigma_right (λh₂, + sigma_equiv_sigma !eq_equiv_con_inv_eq_idp⁻¹ᵉ (λr₂, + sigma_equiv_sigma_left (pi_equiv_pi_right (λa, equiv_eq_closed_right _ r)) ⬝e + sigma_equiv_sigma_right (λh₁, !eq_equiv_con_inv_eq_idp⁻¹ᵉ)) ⬝e + !sigma_comm_equiv ⬝e + sigma_equiv_sigma_right (λh₁, !comm_equiv_nondep)) ⬝e + !sigma_comm_equiv) ⬝e + !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λh₁, + !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λh₂, + !sigma_sigma_eq_right))) ⬝e _, + refine !sigma_assoc_equiv' ⬝e _, + refine sigma_equiv_sigma_left (@sigma_pi_equiv_pi_sigma _ _ (λa f, f pt = pt) ⬝e + pi_equiv_pi_right (λa, !pmap.sigma_char⁻¹ᵉ)) ⬝e _, + exact !dbpmap.sigma_char⁻¹ᵉ + end + + definition dsmash_pelim_equiv' (B : A → Type*) (C : Type*) : + ppmap (⋀ B) C ≃ Π*a, B a →** C := + dsmash_pelim_equiv B C ⬝e (ppi_equiv_dbpmap B (λa, C))⁻¹ᵉ +exit + definition dsmash_arrow_equiv2 [constructor] (B : A → Type*) (C : Type) : + (⋀ B → C) ≃ Σ(f : Πa, B a → C) (c₀ : C) (p : Πa, f a pt = c₀) (q : Πb, f pt b = c₀), p pt = q pt := + begin + fapply equiv.MK, + { intro f, exact ⟨λa b, f (dsmash.mk a b), f auxr, f auxl, (λa, ap f (gluel a), λb, ap f (gluer b))⟩ }, + { intro x, exact dsmash.elim x.1 x.2.2.1 x.2.1 x.2.2.2.1 x.2.2.2.2 }, + { intro x, induction x with f x, induction x with c₁ x, induction x with c₀ x, induction x with p₁ p₂, + apply ap (dpair _), apply ap (dpair _), apply ap (dpair _), esimp, + exact pair_eq (eq_of_homotopy (elim_gluel _ _)) (eq_of_homotopy (elim_gluer _ _)) }, + { intro f, apply eq_of_homotopy, intro x, induction x, reflexivity, reflexivity, reflexivity, + apply eq_pathover, apply hdeg_square, apply elim_gluel, + apply eq_pathover, apply hdeg_square, apply elim_gluer } + end + + definition dsmash_arrow_equiv2_inv_pt [constructor] + (x : Σ(f : Πa, B a → C) (c₁ : C) (c₀ : C), (Πa, f a pt = c₀) × (Πb, f pt b = c₁)) : + to_inv (dsmash_arrow_equiv B C) x pt = x.1 pt pt := + by reflexivity + + open pi + + definition dsmash_pmap_equiv2 (B : A → Type*) (C : Type*) : + (⋀ B →* C) ≃ dbppmap B (λa, C) := + begin + refine !pmap.sigma_char ⬝e _, + refine sigma_equiv_sigma_left !dsmash_arrow_equiv ⬝e _, + refine sigma_equiv_sigma_right (λx, equiv_eq_closed_left _ (dsmash_arrow_equiv_inv_pt x)) ⬝e _, + refine !sigma_assoc_equiv ⬝e _, + refine sigma_equiv_sigma_right (λf, !sigma_assoc_equiv ⬝e + sigma_equiv_sigma_right (λc₁, !sigma_assoc_equiv ⬝e + sigma_equiv_sigma_right (λc₂, sigma_equiv_sigma_left !sigma.equiv_prod⁻¹ᵉ ⬝e + !sigma_assoc_equiv) ⬝e + sigma_assoc_equiv_left _ (sigma_homotopy_constant_equiv pt (λa, f a pt))⁻¹ᵉ ⬝e + sigma_equiv_sigma_right (λh₁, !sigma_comm_equiv) ⬝e !sigma_comm_equiv) ⬝e + sigma_assoc_equiv_left _ (sigma_homotopy_constant_equiv pt (f pt))⁻¹ᵉ ⬝e + sigma_equiv_sigma_right (λh₂, + sigma_equiv_sigma_right (λr₂, + sigma_equiv_sigma_right (λh₁, !comm_equiv_nondep) ⬝e !sigma_comm_equiv) ⬝e + !sigma_comm_equiv) ⬝e + !sigma_comm_equiv ⬝e + sigma_equiv_sigma_right (λr, + sigma_equiv_sigma_left (pi_equiv_pi_right (λb, equiv_eq_closed_right _ r)) ⬝e + sigma_equiv_sigma_right (λh₂, + sigma_equiv_sigma !eq_equiv_con_inv_eq_idp⁻¹ᵉ (λr₂, + sigma_equiv_sigma_left (pi_equiv_pi_right (λa, equiv_eq_closed_right _ r)) ⬝e + sigma_equiv_sigma_right (λh₁, !eq_equiv_con_inv_eq_idp⁻¹ᵉ)) ⬝e + !sigma_comm_equiv ⬝e + sigma_equiv_sigma_right (λh₁, !comm_equiv_nondep)) ⬝e + !sigma_comm_equiv) ⬝e + !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λh₁, + !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λh₂, + !sigma_sigma_eq_right))) ⬝e _, + refine !sigma_assoc_equiv' ⬝e _, + refine sigma_equiv_sigma_left (@sigma_pi_equiv_pi_sigma _ _ (λa f, f pt = pt) ⬝e + pi_equiv_pi_right (λa, !pmap.sigma_char⁻¹ᵉ)) ⬝e _, + exact !dbpmap.sigma_char⁻¹ᵉ + end + +end dsmash diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 578eefa..9ce3b5f 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -1,9 +1,9 @@ -- Authors: Floris van Doorn -import homotopy.smash types.pointed2 .pushout homotopy.red_susp ..pointed +import homotopy.smash types.pointed2 .pushout ..pointed open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc - function red_susp unit + function unit /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash) -/ diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean index 8bbb8f0..82b6380 100644 --- a/homotopy/spherical_fibrations.hlean +++ b/homotopy/spherical_fibrations.hlean @@ -20,7 +20,7 @@ namespace spherical_fibrations definition G_char (n : ℕ) [is_succ n] : G n ≃ (S (pred n) ≃ S (pred n)) := calc G n ≃ Σ(p : pType.carrier (S (pred n)) = pType.carrier (S (pred n))), _ : sigma_eq_equiv - ... ≃ (pType.carrier (S (pred n)) = pType.carrier (S (pred n))) : sigma_equiv_of_is_contr_right + ... ≃ (pType.carrier (S (pred n)) = pType.carrier (S (pred n))) : sigma_equiv_of_is_contr_right _ _ ... ≃ (S (pred n) ≃ S (pred n)) : eq_equiv_equiv definition mirror (n : ℕ) [is_succ n] : S (pred n) → G n := diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 949f87c..63e94e6 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -125,7 +125,7 @@ namespace sigma definition sigma_equiv_of_is_embedding_left_contr [constructor] {X Y : Type} {P : Y → Type} (f : X → Y) (Hf : is_embedding f) (HP : Πx, is_contr (P (f x))) (H : Πy, P y → fiber f y) : (Σy, P y) ≃ X := - sigma_equiv_of_is_embedding_left f Hf _ H ⬝e !sigma_equiv_of_is_contr_right + sigma_equiv_of_is_embedding_left f Hf _ H ⬝e sigma_equiv_of_is_contr_right _ _ end sigma open sigma diff --git a/pointed_binary.hlean b/pointed_binary.hlean index 4a3b699..d3c8a60 100644 --- a/pointed_binary.hlean +++ b/pointed_binary.hlean @@ -10,6 +10,7 @@ open eq pointed equiv sigma is_equiv trunc option pi function fiber sigma.ops namespace pointed +section bpmap /- binary pointed maps -/ structure bpmap (A B C : Type*) : Type := (f : A → B →* C) @@ -159,6 +160,99 @@ begin { exact sorry }}, { exact sorry } end +end bpmap +/- fiberwise pointed maps -/ +structure dbpmap {A : Type*} (B C : A → Type*) : Type := + (f : Πa, B a →* C a) + (q : Πb, f pt b = pt) + (r : q pt = respect_pt (f pt)) + +attribute [coercion] dbpmap.f +variables {A A' : Type*} {B C : A → Type*} {B' C' : A' → Type*} {f f' : dbpmap B C} +definition respect_ptd1 [unfold 4] (f : dbpmap B C) (b : B pt) : f pt b = pt := +dbpmap.q f b + +definition respect_ptd2 [unfold 4] (f : dbpmap B C) (a : A) : f a pt = pt := +respect_pt (f a) + +definition respect_dptpt [unfold 4] (f : dbpmap B C) : respect_ptd1 f pt = respect_ptd2 f pt := +dbpmap.r f + +definition dbpconst [constructor] (B C : A → Type*) : dbpmap B C := +dbpmap.mk (λa, pconst (B a) (C a)) (λb, idp) idp + +definition dbppmap [constructor] (B C : A → Type*) : Type* := +pointed.MK (dbpmap B C) (dbpconst B C) + +definition ppi_of_dbpmap [constructor] (f : dbppmap B C) : Π*a, B a →** C a := +begin + fapply ppi.mk, + { intro a, exact pmap.mk (f a) (respect_ptd2 f a) }, + { exact eq_of_phomotopy (phomotopy.mk (respect_ptd1 f) (respect_dptpt f)) } +end + +definition dbpmap_of_ppi [constructor] (f : Π*a, B a →** C a) : dbppmap B C := +begin + apply dbpmap.mk (λa, f a) (ap010 pmap.to_fun (respect_pt f)), + exact respect_pt (phomotopy_of_eq (respect_pt f)) +end + +protected definition dbpmap.sigma_char [constructor] (B C : A → Type*) : + dbpmap B C ≃ Σ(f : Πa, B a →* C a) (q : Πb, f pt b = pt), q pt = respect_pt (f pt) := +begin + fapply equiv.MK, + { intro f, exact ⟨f, respect_ptd1 f, respect_dptpt f⟩ }, + { intro fqr, exact dbpmap.mk fqr.1 fqr.2.1 fqr.2.2 }, + { intro fqr, induction fqr with f qr, induction qr with q r, reflexivity }, + { intro f, induction f, reflexivity } +end + +definition dbpmap_eq_equiv [constructor] (f f' : dbpmap B C): + f = f' ≃ Σ(h : Πa, f a ~* f' a) (q : Πb, square (respect_ptd1 f b) (respect_ptd1 f' b) (h pt b) idp), cube (vdeg_square (respect_dptpt f)) (vdeg_square (respect_dptpt f')) + vrfl ids + (q pt) (to_homotopy_pt_square (h pt)) := +begin + refine eq_equiv_fn_eq (dbpmap.sigma_char B C) f f' ⬝e _, + refine !sigma_eq_equiv ⬝e _, esimp, + refine sigma_equiv_sigma (!eq_equiv_homotopy ⬝e pi_equiv_pi_right (λa, !pmap_eq_equiv)) _, + intro h, exact sorry +end + +definition dbpmap_eq [constructor] (h : Πa, f a ~* f' a) + (q : Πb, square (respect_ptd1 f b) (respect_ptd1 f' b) (h pt b) idp) + (r : cube (vdeg_square (respect_dptpt f)) (vdeg_square (respect_dptpt f')) + vrfl ids + (q pt) (to_homotopy_pt_square (h pt))) : f = f' := +(dbpmap_eq_equiv f f')⁻¹ᵉ ⟨h, q, r⟩ + +definition ppi_equiv_dbpmap [constructor] (B C : A → Type*) : (Π*a, B a →** C a) ≃ dbpmap B C := +begin + refine !ppi.sigma_char ⬝e _ ⬝e !dbpmap.sigma_char⁻¹ᵉ, + refine sigma_equiv_sigma_right (λf, pmap_eq_equiv (f pt) !pconst) ⬝e _, + refine sigma_equiv_sigma_right (λf, !phomotopy.sigma_char) +end + +definition ppi_equiv_dbpmap' [constructor] (B C : A → Type*) : (Π*a, B a →** C a) ≃ dbpmap B C := +begin + refine equiv_change_fun (ppi_equiv_dbpmap B C) _, + exact dbpmap_of_ppi, intro f, reflexivity +end + +definition pppi_pequiv_dbppmap [constructor] (B C : A → Type*) : + (Π*a, B a →** C a) ≃* dbppmap B C := +pequiv_of_equiv (ppi_equiv_dbpmap' B C) idp + +definition dbpmap_functor [constructor] (f : A' →* A) (g : Πa, B' a →* B (f a)) (h : Πa, C (f a) →* C' a) + (k : dbpmap B C) : dbpmap B' C' := +begin + fapply dbpmap.mk (λa', h a' ∘* k (f a') ∘* g a'), + { intro b', refine ap (h pt) _ ⬝ respect_pt (h pt), + exact sorry }, --ap010 (λa b, k a b) (respect_pt f) (g pt b') ⬝ respect_ptd1 k (g pt b') }, + { exact sorry }, + -- apply whisker_right, apply ap02 h, esimp, + -- induction A with A a₀, induction B with B b₀, induction f with f f₀, induction g with g g₀, + -- esimp at *, induction f₀, induction g₀, esimp, apply whisker_left, exact respect_dptpt k }, +end end pointed diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 9f64d9a..cb3524e 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -699,7 +699,7 @@ namespace pointed definition psigma_gen_assoc [constructor] {A : Type*} {B : A → Type} (C : Πa, B a → Type) (b₀ : B pt) (c₀ : C pt b₀) : psigma_gen (λa, Σb, C a b) ⟨b₀, c₀⟩ ≃* @psigma_gen (psigma_gen B b₀) (λv, C v.1 v.2) c₀ := - pequiv_of_equiv !sigma_assoc_equiv idp + pequiv_of_equiv !sigma_assoc_equiv' idp definition psigma_gen_swap [constructor] {A : Type*} {B B' : A → Type} (C : Π⦃a⦄, B a → B' a → Type) (b₀ : B pt) (b₀' : B' pt) (c₀ : C b₀ b₀') : diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean index 0eb075f..ad3a31b 100644 --- a/spectrum/basic.hlean +++ b/spectrum/basic.hlean @@ -562,7 +562,7 @@ namespace spectrum definition shomotopy_group_isomorphism_of_pequiv (n : ℤ) {E F : spectrum} (f : Πn, E n ≃* F n) : πₛ[n] E ≃g πₛ[n] F := - proof homotopy_group_isomorphism_of_pequiv 1 (f (2 - n)) qed + by rexact homotopy_group_isomorphism_of_pequiv 1 (f (2 - n)) definition shomotopy_group_isomorphism_of_pequiv_nat (n : ℕ) {E F : spectrum} (f : Πn, E n ≃* F n) : πₛ[n] E ≃g πₛ[n] F := @@ -699,8 +699,8 @@ namespace spectrum definition shomotopy_groups_fun : Π(v : +3ℤ), shomotopy_groups (S v) →g shomotopy_groups v | (n, fin.mk 0 H) := proof πₛ→[n] f qed | (n, fin.mk 1 H) := proof πₛ→[n] (spoint f) qed - | (n, fin.mk 2 H) := proof homomorphism_LES_of_homotopy_groups_fun (f (2 - n)) (nat.succ nat.zero, 2) ∘g - πg_glue Y n ∘g (by reflexivity) qed + | (n, fin.mk 2 H) := by rexact homomorphism_LES_of_homotopy_groups_fun (f (2 - n)) (nat.succ nat.zero, 2) ∘g + πg_glue Y n | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end --(homomorphism_LES_of_homotopy_groups_fun (f (2 - n)) (1, 2) ∘g πg_glue Y n) @@ -724,13 +724,15 @@ namespace spectrum /- homotopy group of a prespectrum -/ + local attribute [reducible] agtrunc aghomotopy_group ghomotopy_group gtrunc definition pshomotopy_group_hom (n : ℤ) (E : prespectrum) (k : ℕ) : πag[k + 2] (E (-n + 2 + k)) →g πag[k + 3] (E (-n + 2 + (k + 1))) := begin + change πg[k + 2] (E (-n + 2 + k)) →g πg[k + 3] (E (-n + 2 + (k + 1))), refine _ ∘g π→g[k+2] (glue E _), refine (ghomotopy_group_succ_in (k+1) _)⁻¹ᵍ ∘g _, - refine homotopy_group_isomorphism_of_pequiv (k+1) - (loop_pequiv_loop (pequiv_of_eq (ap E (add.assoc (-n + 2) k 1)))) + refine homotopy_group_isomorphism_of_pequiv (k+1) _, + exact (loop_pequiv_loop (pequiv_of_eq (ap E (add.assoc (-n + 2) k 1)))) end definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup := diff --git a/univalent_subcategory.hlean b/univalent_subcategory.hlean index 5012425..e3425ca 100644 --- a/univalent_subcategory.hlean +++ b/univalent_subcategory.hlean @@ -166,7 +166,7 @@ repeat (fconstructor; assumption), assumption, intro b, open sigma.ops definition sigma_prod_equiv_sigma_sigma {A} {B C : A→Type} : (Σa, B a × C a) ≃ Σ p : (Σa, B a), C p.1 := -sigma_equiv_sigma_right (λa, !sigma.equiv_prod⁻¹ᵉ) ⬝e !sigma_assoc_equiv +sigma_equiv_sigma_right (λa, !sigma.equiv_prod⁻¹ᵉ) ⬝e !sigma_assoc_equiv' definition ab_group_equiv_group_comm (A : Type) : ab_group A ≃ Σ (g : group A), ∀ a b : A, a * b = b * a := begin @@ -232,7 +232,7 @@ end ((sigma_char2 G).2 =[p] (sigma_char2 H).2) ≃ (is_mul_hom (equiv_of_eq (proof p qed : Group.carrier G = Group.carrier H))) := begin - refine !sigma_pathover_equiv_of_is_prop ⬝e _, + refine sigma_pathover_equiv_of_is_prop _ _ _ _ _ ⬝e _, induction G with G g, induction H with H h, esimp [sigma_char2] at p, esimp [sigma_functor] at p, esimp [Group_sigma] at *,