more on pushouts, interaction with sums, and induction principle for certain cofibers

latter part ported from Agda

homotopy/pushout.hlean

@@ -6,6 +6,11 @@ open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool
 
 namespace pushout
 
+  /-
+    WIP: proving that satisfying the universal property of the pushout is equivalent to
+    being equivalent to the pushout
+  -/
+
   universe variables u₁ u₂ u₃ u₄
   variables {A : Type.{u₁}} {B : Type.{u₂}} {C : Type.{u₃}} {D D' : Type.{u₄}}
             {f : A → B} {g : A → C} {h : B → D} {k : C → D} (p : h ∘ f ~ k ∘ g)
@@ -125,6 +130,8 @@ namespace pushout
 --       }
 --   end
 
+  /- composing pushouts -/
+
   definition pushout_vcompose_to [unfold 8] {A B C D : Type} {f : A → B} {g : A → C} {h : B → D}
     (x : pushout h (@inl _ _ _ f g)) : pushout (h ∘ f) g :=
   begin
@@ -207,25 +214,6 @@ namespace pushout
       ... ≃ pushout hg f : by exact pushout_vcompose_equiv _ (e ⬝e pushout.symm f g) p q
       ... ≃ pushout f hg : pushout.symm
 
-  -- is the following even true?
-  -- definition pushout_vcancel_right [constructor] {A B C D E : Type} {f : A → B} {g : A → C}
-  --   (h : B → D) (k : B → E) (e : pushout h k ≃ pushout (h ∘ f) g)
-  --   (p : e ∘ inl ~ inl) : E ≃ pushout f g :=
-  -- begin
-  --   fapply equiv.MK,
-  --   { intro x, note aux := refl (e (inr x)), revert aux,
-  --     refine pushout.rec (λy (p : e (inr x) = inl y), _) _ _ (e (inr x)),
-  --       intro d q, note r := eq_of_fn_eq_fn e (q ⬝ (p d)⁻¹), exact sorry,
-  --       intro c q, exact inr c,
-  --       intro a, exact sorry },
-  --   { intro x, induction x with b c a,
-  --     { exact k b },
-  --     { },
-  --     { }},
-  --   { },
-  --   { }
-  -- end
-
   definition pushout_of_equiv_left_to [unfold 6] {A B C : Type} {f : A ≃ B} {g : A → C}
     (x : pushout f g) : C :=
   begin
@@ -257,46 +245,50 @@ namespace pushout
     pushout f g ≃ pushout g f : pushout.symm f g
             ... ≃ B           : pushout_of_equiv_left g f
 
+  /- pushout where one map is constant is a cofiber -/
+
   definition pushout_const_equiv_to [unfold 6] {A B C : Type} {f : A → B} {c₀ : C}
-    (x : pushout f (const A c₀)) : pushout (sum_functor f (const unit c₀)) (const _ ⋆) :=
+    (x : pushout (const A c₀) f) : cofiber (sum_functor f (const unit c₀)) :=
   begin
-    induction x with b c a,
+    induction x with c b a,
-    { exact inl (sum.inl b) },
+    { exact inr (sum.inr c) },
-    { exact inl (sum.inr c) },
+    { exact inr (sum.inl b) },
-    { exact glue (sum.inl a) ⬝ (glue (sum.inr ⋆))⁻¹ }
+    { exact (glue (sum.inr ⋆))⁻¹ ⬝ glue (sum.inl a) }
   end
 
   definition pushout_const_equiv_from [unfold 6] {A B C : Type} {f : A → B} {c₀ : C}
-    (x : pushout (sum_functor f (const unit c₀)) (const _ ⋆)) : pushout f (const A c₀) :=
+    (x : cofiber (sum_functor f (const unit c₀))) : pushout (const A c₀) f :=
   begin
-    induction x with v u v,
+    induction x with v v,
-    { induction v with b c, exact inl b, exact inr c },
+    { exact inl c₀ },
-    { exact inr c₀ },
+    { induction v with b c, exact inr b, exact inl c },
     { induction v with a u, exact glue a, reflexivity }
   end
 
   definition pushout_const_equiv [constructor] {A B C : Type} (f : A → B) (c₀ : C) :
-    pushout f (const A c₀) ≃ pushout (sum_functor f (const unit c₀)) (const _ ⋆) :=
+    pushout (const A c₀) f ≃ cofiber (sum_functor f (const unit c₀)) :=
   begin
     fapply equiv.MK,
     { exact pushout_const_equiv_to },
     { exact pushout_const_equiv_from },
-    { intro x, induction x with v u v,
+    { intro x, induction x with v v,
+      { exact (glue (sum.inr ⋆))⁻¹ },
       { induction v with b c, reflexivity, reflexivity },
-      { induction u, exact glue (sum.inr ⋆) },
       { apply eq_pathover_id_right,
         refine ap_compose pushout_const_equiv_to _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
         induction v with a u,
-        { refine !elim_glue ⬝ph _, apply whisker_bl, exact hrfl},
+        { refine !elim_glue ⬝ph _, esimp, apply whisker_tl, exact hrfl },
-        { induction u, exact square_of_eq idp }}},
+        { induction u, exact square_of_eq !con.left_inv }}},
-    { intro x, induction x with b c a,
+    { intro x, induction x with c b a,
       { reflexivity },
       { reflexivity },
       { apply eq_pathover_id_right, apply hdeg_square,
         refine ap_compose pushout_const_equiv_from _ _ ⬝ ap02 _ !elim_glue ⬝ _,
-        exact !ap_con ⬝ !elim_glue ◾ (!ap_inv ⬝ !elim_glue⁻²) }}
+        refine !ap_con ⬝ (!ap_inv ⬝ !elim_glue⁻²) ◾ !elim_glue ⬝ !idp_con }}
   end
 
+  /- wedge is the cofiber of the map 2 -> A + B -/
+
   -- move to sum
   definition sum_of_bool [unfold 3] (A B : Type*) (b : bool) : A + B :=
   by induction b; exact sum.inl pt; exact sum.inr pt
@@ -306,18 +298,22 @@ namespace pushout
 
   -- move to wedge
   definition wedge_equiv_pushout_sum [constructor] (A B : Type*) :
-    wedge A B ≃ pushout (sum_of_bool A B) (const bool ⋆) :=
+    wedge A B ≃ cofiber (sum_of_bool A B) :=
   begin
+    refine !pushout.symm ⬝e _,
     refine pushout_const_equiv _ _ ⬝e _,
     fapply pushout.equiv,
       exact bool_equiv_unit_sum_unit⁻¹ᵉ,
       reflexivity,
       reflexivity,
       intro x, induction x: reflexivity,
-      reflexivity
+      intro x, induction x with u u: induction u; reflexivity
-  en
+  end
-d
+
+  section
   open prod.ops
+  /- products preserve pushouts -/
+
   definition pushout_prod_equiv_to [unfold 7] {A B C D : Type} {f : A → B} {g : A → C}
     (xd : pushout f g × D) : pushout (prod_functor f (@id D)) (prod_functor g id) :=
   begin
@@ -352,7 +348,99 @@ d
       { reflexivity },
       { reflexivity },
       { apply eq_pathover, apply hdeg_square,
-        exact ap_compose pushout_prod_equiv_from _ _ ⬝ ap02 _ !elim_glue ⬝ !elim_glue }}
+        refine ap_compose (pushout_prod_equiv_from ∘ pushout_prod_equiv_to) _ _ ⬝ _,
+        refine ap02 _ !ap_prod_mk_left ⬝ !ap_compose ⬝ _,
+        refine ap02 _ (!ap_prod_elim ⬝ !idp_con ⬝ !elim_glue) ⬝ _,
+        refine !elim_glue ⬝ !ap_prod_mk_left⁻¹ }}
+  end
+  end
+
+  /- interaction of pushout and sums -/
+
+  definition pushout_to_sum [unfold 8] {A B C : Type} {f : A → B} {g : A → C} (D : Type) (c₀ : C)
+    (x : pushout f g) : pushout (sum_functor f (@id D)) (sum.rec g (λd, c₀)) :=
+  begin
+    induction x with b c a,
+    { exact inl (sum.inl b) },
+    { exact inr c },
+    { exact glue (sum.inl a) }
+  end
+
+  definition pushout_from_sum [unfold 8] {A B C : Type} {f : A → B} {g : A → C} (D : Type) (c₀ : C)
+    (x : pushout (sum_functor f (@id D)) (sum.rec g (λd, c₀))) : pushout f g :=
+  begin
+    induction x with x c x,
+    { induction x with b d, exact inl b, exact inr c₀ },
+    { exact inr c },
+    { induction x with a d, exact glue a, reflexivity }
+
+  end
+
+  definition pushout_sum_equiv [constructor] {A B C : Type} (f : A → B) (g : A → C) (D : Type)
+    (c₀ : C) : pushout f g ≃ pushout (sum_functor f (@id D)) (sum.rec g (λd, c₀)) :=
+  begin
+    fapply equiv.MK,
+    { exact pushout_to_sum D c₀ },
+    { exact pushout_from_sum D c₀ },
+    { intro x, induction x with x c x,
+      { induction x with b d, reflexivity, esimp, exact (glue (sum.inr d))⁻¹ },
+      { reflexivity },
+      { apply eq_pathover_id_right,
+        refine ap_compose (pushout_to_sum D c₀) _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
+        induction x with a d: esimp,
+        { exact hdeg_square !elim_glue },
+        { exact square_of_eq !con.left_inv }}},
+    { intro x, induction x with b c a,
+      { reflexivity },
+      { reflexivity },
+      { apply eq_pathover_id_right, apply hdeg_square,
+        refine ap_compose (pushout_from_sum D c₀) _ _ ⬝ ap02 _ !elim_glue ⬝ !elim_glue }}
+  end
+
+  /- an induction principle for the cofiber of f : A → B if A is a pushout where the second map has a section.
+     The Pgluer is modified to get the right coherence
+     See https://github.com/HoTT/HoTT-Agda/blob/master/theorems/homotopy/elims/CofPushoutSection.agda
+  -/
+
+  open sigma.ops
+  definition cofiber_pushout_helper' {A : Type} {B : A → Type} {a₀₀ a₀₂ a₂₀ a₂₂ : A} {p₀₁ : a₀₀ = a₀₂}
+    {p₁₀ : a₀₀ = a₂₀} {p₂₁ : a₂₀ = a₂₂} {p₁₂ : a₀₂ = a₂₂} {s : square p₀₁ p₂₁ p₁₀ p₁₂}
+    {b₀₀ : B a₀₀} {b₂₀ b₂₀' : B a₂₀} {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {q₁₀ : b₀₀ =[p₁₀] b₂₀}
+    {q₀₁ : b₀₀ =[p₀₁] b₀₂} {q₂₁ : b₂₀' =[p₂₁] b₂₂} {q₁₂ : b₀₂ =[p₁₂] b₂₂} :
+    Σ(r : b₂₀' = b₂₀), squareover B s q₀₁ (r ▸ q₂₁) q₁₀ q₁₂ :=
+  begin
+    induction s,
+    induction q₀₁ using idp_rec_on,
+    induction q₂₁ using idp_rec_on,
+    induction q₁₀ using idp_rec_on,
+    induction q₁₂ using idp_rec_on,
+    exact ⟨idp, idso⟩
+  end
+
+  definition cofiber_pushout_helper {A B C D : Type} {f : A → B} {g : A → C} {h : pushout f g → D}
+    {P : cofiber h → Type} {Pbase : P (cofiber.base h)} {Pcod : Πd, P (cofiber.cod h d)}
+    (Pgluel : Π(b : B), Pbase =[cofiber.glue (inl b)] Pcod (h (inl b)))
+    (Pgluer : Π(c : C), Pbase =[cofiber.glue (inr c)] Pcod (h (inr c)))
+    (a : A) : Σ(p : Pbase = Pbase), squareover P (natural_square cofiber.glue (glue a))
+    (Pgluel (f a)) (p ▸ Pgluer (g a))
+    (pathover_ap P (λa, cofiber.base h) (apd (λa, Pbase) (glue a)))
+    (pathover_ap P (λa, cofiber.cod h (h a)) (apd (λa, Pcod (h a)) (glue a))) :=
+  !cofiber_pushout_helper'
+
+  definition cofiber_pushout_rec {A B C D : Type} {f : A → B} {g : A → C} {h : pushout f g → D}
+    {P : cofiber h → Type} (Pbase : P (cofiber.base h)) (Pcod : Πd, P (cofiber.cod h d))
+    (Pgluel : Π(b : B), Pbase =[cofiber.glue (inl b)] Pcod (h (inl b)))
+    (Pgluer : Π(c : C), Pbase =[cofiber.glue (inr c)] Pcod (h (inr c)))
+    (r : C → A) (p : Πa, r (g a) = a)
+    (x : cofiber h) : P x :=
+  begin
+    induction x with d x,
+    { exact Pbase },
+    { exact Pcod d },
+    { induction x with b c a,
+      { exact Pgluel b },
+      { exact (cofiber_pushout_helper Pgluel Pgluer (r c)).1 ▸ Pgluer c },
+      { apply pathover_pathover, rewrite [p a], exact (cofiber_pushout_helper Pgluel Pgluer a).2 }}
   end
 
 end pushout

homotopy/smash.hlean

@@ -3,21 +3,20 @@
 import homotopy.smash ..move_to_lib .pushout homotopy.red_susp
 
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
-     function red_susp
+     function red_susp unit
 
-  /- smash A (susp B) = susp (smash A B) <- this follows from associativity and smash with S¹ -/
+  /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (?) (notation means suspension, wedge, smash) -/
 
-  /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash),
+  /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/
-     and both are equivalent to the reduced join -/
 
-  /- To prove: associative -/
+  /- To prove: associative, A ∧ S¹ ≃ ΣA -/
-
-  /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
 
 variables {A B : Type*}
 
 namespace smash
 
+  /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
+
   theorem elim_gluel' {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
     (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a a' : A) :
     ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel' a a') = Pgl a ⬝ (Pgl a')⁻¹ :=
@@ -93,10 +92,10 @@ namespace pushout
      A + B <-- 2 --> 1 -/
   definition pushout_wedge_of_sum_equiv_unit : pushout (@wedge_of_sum A B) bool_of_sum ≃ unit :=
   begin
-    refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B ⬝e !pushout.symm)
+    refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B)
              _ _ ⬝e _,
       exact erfl,
-      reflexivity,
+      intro x, induction x: esimp,
       exact bool_of_sum_of_bool,
     apply pushout_of_equiv_right
   end
@@ -106,6 +105,25 @@ end pushout open pushout
 namespace smash
 
   variables (A B)
+
+  definition smash_punit_pequiv [constructor] : smash A punit ≃* punit :=
+  begin
+    fapply pequiv_of_equiv,
+    { fapply equiv.MK,
+      { exact λx, ⋆ },
+      { exact λx, pt },
+      { intro x, induction x, reflexivity },
+      { exact abstract begin intro x, induction x,
+        { induction b, exact gluel' pt a },
+        { exact gluel pt },
+        { exact gluer pt },
+        { apply eq_pathover_constant_left_id_right, apply square_of_eq_top,
+          exact whisker_right _ !idp_con⁻¹ },
+        { apply eq_pathover_constant_left_id_right, induction b,
+          refine !con.right_inv ⬝pv _, exact square_of_eq idp } end end }},
+    { reflexivity }
+  end
+
   definition smash_equiv_cofiber : smash A B ≃ cofiber (@prod_of_wedge A B) :=
   begin
     unfold [smash, cofiber, smash'], symmetry,
@@ -133,7 +151,7 @@ namespace smash
 
   /- commutativity -/
 
-  definition smash_flip (x : smash A B) : smash B A :=
+  definition smash_flip [unfold 3] (x : smash A B) : smash B A :=
   begin
     induction x,
     { exact smash.mk b a },
@@ -143,7 +161,7 @@ namespace smash
     { exact gluel b }
   end
 
-  definition smash_flip_smash_flip (x : smash A B) : smash_flip (smash_flip x) = x :=
+  definition smash_flip_smash_flip [unfold 3] (x : smash A B) : smash_flip (smash_flip x) = x :=
   begin
     induction x,
     { reflexivity },
@@ -157,7 +175,7 @@ namespace smash
       apply hrfl }
   end
 
-  definition smash_comm : smash A B ≃* smash B A :=
+  definition smash_comm [constructor] : smash A B ≃* smash B A :=
   begin
     fapply pequiv_of_equiv,
     { apply equiv.MK, do 2 exact smash_flip_smash_flip },
@@ -194,7 +212,7 @@ namespace smash
       exact ap_is_constant gluer loop ⬝ !con.right_inv }
   end
 
-  definition smash_pcircle_of_psusp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
+  definition smash_pcircle_of_red_susp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
     smash_pcircle_of_red_susp (red_susp_of_smash_pcircle (smash.mk a x)) = smash.mk a x :=
   begin
     induction x,
@@ -238,7 +256,7 @@ namespace smash
           esimp, exact !idp_con ⬝ !elim_loop },
         { exact sorry } end end },
       { intro x, induction x,
-        { exact smash_pcircle_of_psusp_of_smash_pcircle_pt a b },
+        { exact smash_pcircle_of_red_susp_of_smash_pcircle_pt a b },
         { exact gluel pt },
         { exact gluer pt },
         { apply eq_pathover_id_right,
@@ -255,18 +273,12 @@ namespace smash
           { exact whisker_right _ !con.right_inv },
           { apply eq_pathover_dep, refine !apd_con_fn ⬝pho _ ⬝hop !apd_con_fn⁻¹,
             refine ap (λx, concat2o x _) !rec_loop ⬝pho _ ⬝hop (ap011 concat2o (apd_compose1 (λa b, ap smash_pcircle_of_red_susp b) (circle_elim_constant equator_pt) loop) !apd_constant')⁻¹,
-            }
+            exact sorry }
 
           }}},
     { reflexivity }
   end
-print apd_constant
+
-print apd_compose2
-print apd_compose1
-print apd_con
-print eq_pathover_dep
---set_option pp.all true
-print smash.elim_gluer
   /- smash A S¹ = susp A -/
   open susp
 
@@ -301,17 +313,19 @@ print smash.elim_gluer
       refine ap02 _ (elim_loop north (merid a ⬝ (merid pt)⁻¹)) ⬝ph _,
       refine !ap_con ⬝ (!elim_merid ◾ (!ap_inv ⬝ !elim_merid⁻²)) ⬝ph _,
       -- make everything below this a lemma defined by path induction?
-      refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, refine !con.assoc⁻¹ ⬝ph _,
+      exact sorry,
-      apply whisker_bl, apply whisker_lb,
+      -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, refine !con.assoc⁻¹ ⬝ph _,
-      refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, apply hrfl
+      -- apply whisker_bl, apply whisker_lb,
-      refine !con_idp⁻¹ ⬝pv _, apply whisker_tl,
+      -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, apply hrfl
-      refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb, apply hrfl
+      -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl,
-      apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left,
+      -- refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb, apply hrfl
-      symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv,
+      -- apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left,
-      refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc,
+      -- symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv,
-      refine _ ⬝ whisker_right _ !inv_con_cancel_right⁻¹, refine _ ⬝ !con.right_inv⁻¹,
+      -- refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc,
-      refine !con.right_inv ◾ _, refine _ ◾ !con.right_inv,
+      -- refine _ ⬝ whisker_right _ !inv_con_cancel_right⁻¹, refine _ ⬝ !con.right_inv⁻¹,
-      refine !ap_mk_right ⬝ !con.right_inv end end }
+      -- refine !con.right_inv ◾ _, refine _ ◾ !con.right_inv,
+      -- refine !ap_mk_right ⬝ !con.right_inv
+      end end }
   end
 
   -- definition smash_pcircle_of_psusp_of_smash_pcircle_gluer_base (b : S¹*)
@@ -366,4 +380,3 @@ exit
   end
 
 end smash
--- (X × A) → Y ≃ X → A → Y