From 372ca7297c8c62976a0dfe4ad393532702555591 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 5 Jan 2017 20:02:41 +0100
Subject: [PATCH] finish proof that smash is the cofiber of the map from the
 wedge to the product

---
 homotopy/pushout.hlean | 220 ++++++++++++++++++-----------------------
 homotopy/smash.hlean   | 174 +++++++++++++-------------------
 move_to_lib.hlean      |  10 +-
 3 files changed, 174 insertions(+), 230 deletions(-)

diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean
index e83cf3f..a6f4c03 100644
--- a/homotopy/pushout.hlean
+++ b/homotopy/pushout.hlean
@@ -64,8 +64,6 @@ print apd10_ap_precompose_dependent
   definition is_pushout2_pushout : @is_pushout2 _ _ _ _ f g inl inr glue :=
   λX, to_is_equiv (pushout_arrow_equiv f g X ⬝e assoc_equiv_prod _)
 
-  -- set_option pp.implicit true
-  -- set_option pp.notation false
   definition is_equiv_of_is_pushout2_simple [constructor] {A B C D : Type.{u₁}}
             {f : A → B} {g : A → C} {h : B → D} {k : C → D} (p : h ∘ f ~ k ∘ g)
             {h' : B → D'} {k' : C → D'} (p' : h' ∘ f ~ k' ∘ g)
@@ -94,138 +92,110 @@ print apd10_ap_precompose_dependent
         refine apd10 !apd10_eq_of_homotopy (f a) ⬝ph _ ⬝hp apd10 !apd10_eq_of_homotopy⁻¹ (g a),
         refine ap_compose (pushout.elim h k p) _ _ ⬝pv _,
         refine aps (pushout.elim h k p) _ ⬝vp (!elim_glue ⬝ !ap_id⁻¹),
-esimp,   exact sorry
+        esimp,   exact sorry
         },
-
-      -- note q := @eq_of_is_contr _ H''
-      --   ⟨up ∘ pushout.elim h k p ∘ down ∘ (center' H').1,
-      --    (λb, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr1 (center' H').2 b),
-      --     λc, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr2 (center' H').2 c))⟩
-      --   ⟨up, (λx, idp, λx, idp)⟩,
-      -- exact ap down (ap10 q..1 d)
       }
   end
 
-  definition is_equiv_of_is_pushout2 [constructor] (H : is_pushout2 p) : D ≃ pushout f g :=
+
+--   definition is_equiv_of_is_pushout2 [constructor] (H : is_pushout2 p) : D ≃ pushout f g :=
+--   begin
+--     fapply equiv.MK,
+--     { exact down.{_ u₄} ∘ (cocone_of_map p _)⁻¹ᶠ ⟨(up ∘ inl, up ∘ inr), λa, ap up (glue a)⟩ },
+--     { exact pushout.elim h k p },
+--     { intro x, exact sorry
+
+-- },
+--     { intro d, apply eq_of_fn_eq_fn (equiv_lift D), esimp, revert d,
+--       apply ap10,
+--       apply eq_of_fn_eq_fn (equiv.mk _ (H (lift.{_ (max u₁ u₂ u₃)} D))),
+--       fapply sigma_eq,
+--       { esimp, fapply prod_eq,
+--           apply eq_of_homotopy, intro b, apply ap up, esimp,
+--         exact ap (pushout.elim h k p ∘ down.{_ u₄})
+--                    (pushout.inv_left p H ⟨(up ∘ inl, up ∘ inr), λa, ap up (glue a)⟩ b),
+
+--         exact sorry },
+--       { exact sorry },
+
+--       -- note q := @eq_of_is_contr _ H''
+--       --   ⟨up ∘ pushout.elim h k p ∘ down ∘ (center' H').1,
+--       --    (λb, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr1 (center' H').2 b),
+--       --     λc, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr2 (center' H').2 c))⟩
+--       --   ⟨up, (λx, idp, λx, idp)⟩,
+--       -- exact ap down (ap10 q..1 d)
+--       }
+--   end
+
+  definition pushout_compose_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
+    induction x with d y b,
+    { exact inl d },
+    { induction y with b c a,
+      { exact inl (h b) },
+      { exact inr c },
+      { exact glue a }},
+    { reflexivity }
+  end
+
+  definition pushout_compose_from [unfold 8] {A B C D : Type} {f : A → B} {g : A → C} {h : B → D}
+    (x : pushout (h ∘ f) g) : pushout h (@inl _ _ _ f g) :=
+  begin
+    induction x with d c a,
+    { exact inl d },
+    { exact inr (inr c) },
+    { exact glue (f a) ⬝ ap inr (glue a) }
+  end
+
+  definition pushout_compose [constructor] {A B C D : Type} (f : A → B) (g : A → C) (h : B → D) :
+    pushout h (@inl _ _ _ f g) ≃ pushout (h ∘ f) g :=
   begin
     fapply equiv.MK,
-    { exact down.{_ u₄} ∘ (cocone_of_map p _)⁻¹ᶠ ⟨(up ∘ inl, up ∘ inr), λa, ap up (glue a)⟩ },
-    { exact pushout.elim h k p },
-    { intro x, exact sorry
-
-},
-    { intro d, apply eq_of_fn_eq_fn (equiv_lift D), esimp, revert d,
-      apply ap10,
-      apply eq_of_fn_eq_fn (equiv.mk _ (H (lift.{_ (max u₁ u₂ u₃)} D))),
-      fapply sigma_eq,
-      { esimp, fapply prod_eq,
-          apply eq_of_homotopy, intro b, apply ap up, esimp,
-        exact ap (pushout.elim h k p ∘ down.{_ u₄})
-                   (pushout.inv_left p H ⟨(up ∘ inl, up ∘ inr), λa, ap up (glue a)⟩ b),
-
-        exact sorry },
-      { exact sorry },
-
-      -- note q := @eq_of_is_contr _ H''
-      --   ⟨up ∘ pushout.elim h k p ∘ down ∘ (center' H').1,
-      --    (λb, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr1 (center' H').2 b),
-      --     λc, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr2 (center' H').2 c))⟩
-      --   ⟨up, (λx, idp, λx, idp)⟩,
-      -- exact ap down (ap10 q..1 d)
-      }
+    { exact pushout_compose_to },
+    { exact pushout_compose_from },
+    { intro x, induction x with d c a,
+      { reflexivity },
+      { reflexivity },
+      { apply eq_pathover_id_right, apply hdeg_square,
+        refine ap_compose pushout_compose_to _ _ ⬝ ap02 _ !elim_glue ⬝ _,
+        refine !ap_con ⬝ !elim_glue ◾ !ap_compose'⁻¹ ⬝ !idp_con ⬝ _, esimp, apply elim_glue }},
+    { intro x, induction x with d y b,
+      { reflexivity },
+      { induction y with b c a,
+        { exact glue b },
+        { reflexivity },
+        { apply eq_pathover, refine ap_compose pushout_compose_from _ _ ⬝ph _,
+          esimp, refine ap02 _ !elim_glue ⬝ !elim_glue ⬝ph _, apply square_of_eq, reflexivity }},
+      { apply eq_pathover_id_right, esimp,
+        refine ap_compose pushout_compose_from _ _ ⬝ ap02 _ !elim_glue ⬝ph _, apply square_of_eq, reflexivity }}
   end
 
-
-  -- definition is_equiv_of_is_pushout2 [constructor] (H : is_pushout2 p) : D ≃ pushout f g :=
-  -- begin
-  --   note H' := H (lift.{_ u₄} (pushout f g)),
-  --   note bla := equiv.mk _ H',
-  --   fapply equiv.MK,
-  --   { exact down ∘ (center' H').1 },
-  --   { exact pushout.elim h k p },
-  --   { intro x, induction x with b c a,
-  --     { exact ap down (prod.pr1 (center' H').2 b) },
-  --     { exact ap down (prod.pr2 (center' H').2 c) },
-  --     { apply eq_pathover_id_right,
-  --       refine ap_compose (down ∘ (center' H').1) _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
-  --       refine ap_compose down _ _ ⬝ph _ ⬝hp ((ap_compose' down up _)⁻¹ ⬝ !ap_id),
-  --       refine aps down _, }},
-  --   { intro d,
-  --     note H'' := H (up ∘ h) (up ∘ k) (λa, ap up.{_ (max u₁ u₂ u₃)} (p a)),
-  --     note q := @eq_of_is_contr _ H''
-  --       ⟨up ∘ pushout.elim h k p ∘ down ∘ (center' H').1,
-  --        (λb, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr1 (center' H').2 b),
-  --         λc, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr2 (center' H').2 c))⟩
-  --       ⟨up, (λx, idp, λx, idp)⟩,
-  --     exact ap down (ap10 q..1 d)
-  --     }
-  -- end
+  definition pushout_compose' {A B C D : Type} (f : A → B) (g : A → C) (h : B → D) :
+    pushout (@inl _ _ _ f g) h ≃ pushout g (h ∘ f) :=
+  calc
+    pushout (@inl _ _ _ f g) h ≃ pushout h (@inl _ _ _ f g) : pushout.symm
+      ... ≃ pushout (h ∘ f) g : pushout_compose
+      ... ≃ pushout g (h ∘ f) : pushout.symm
 
 
-  -- definition is_pushout_pushout : @is_pushout _ _ _ _ f g inl inr glue :=
-  -- begin
-  --   intro X h k p,
-  --   fapply is_contr.mk,
-  --   { refine ⟨pushout.elim h k p, (λb, idp, λc, idp), λa, hdeg_square (elim_glue h k p a)⟩ },
-  --   { intro v, induction v with l v, induction v with v s, induction v with q r,
-  --     fapply sigma_eq,
-  --     esimp, apply eq_of_homotopy, intro x, induction x with b c a,
-  --     { exact (q b)⁻¹ },
-  --     { exact (r c)⁻¹ },
-  --     { apply eq_pathover, exact !elim_glue ⬝ph (s a)⁻¹ʰ },
-  --   }
-  -- end
-  -- definition is_pushout_of_is_equiv (e : D ≃ pushout f g)
-  --   : is_pushout
-
-  -- variables {f g}
-  -- definition is_equiv_of_is_pushout [constructor] (H : is_pushout p) : D ≃ pushout f g :=
-  -- begin
-  --   note H' := H (up ∘ inl) (up ∘ inr) (λa, ap up.{_ u₄} (@glue _ _ _ f g a)),
-  --   fapply equiv.MK,
-  --   { exact down ∘ (center' H').1 },
-  --   { exact pushout.elim h k p },
-  --   { intro x, induction x with b c a,
-  --     { exact ap down (prod.pr1 (center' H').2 b) },
-  --     { exact ap down (prod.pr2 (center' H').2 c) },
-  --     { apply eq_pathover_id_right,
-  --       refine ap_compose (down ∘ (center' H').1) _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
-  --       refine ap_compose down _ _ ⬝ph _ ⬝hp ((ap_compose' down up _)⁻¹ ⬝ !ap_id),
-  --       refine aps down _, }},
-  --   { intro d,
-  --     note H'' := H (up ∘ h) (up ∘ k) (λa, ap up.{_ (max u₁ u₂ u₃)} (p a)),
-  --     note q := @eq_of_is_contr _ H''
-  --       ⟨up ∘ pushout.elim h k p ∘ down ∘ (center' H').1,
-  --        (λb, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr1 (center' H').2 b),
-  --         λc, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr2 (center' H').2 c))⟩
-  --       ⟨up, (λx, idp, λx, idp)⟩,
-  --     exact ap down (ap10 q..1 d)
-  --     }
-  -- end
-
-  -- set_option pp.universes true
-  -- set_option pp.abbreviations false
-  -- definition is_equiv_of_is_pushout [constructor] (H : is_pushout p) (H : is_pushout p') : D ≃ D' :=
-  -- begin
-  --   note H' := H (up ∘ inl) (up ∘ inr) (λa, ap up.{_ u₄} (@glue _ _ _ f g a)),
-  --   fapply equiv.MK,
-  --   { exact down ∘ (center' H').1 },
-  --   { exact pushout.elim h k p },
-  --   { intro x, induction x with b c a,
-  --     { exact ap down (prod.pr1 (center' H').2 b) },
-  --     { exact ap down (prod.pr2 (center' H').2 c) },
-  --     { -- apply eq_pathover_id_right,
-  --       -- refine ap_compose (center' H').1 _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
-  --       exact sorry }},
-  --   { intro d,
-  --     note H'' := H (up ∘ h) (up ∘ k) (λa, ap up.{_ (max u₁ u₂ u₃)} (p a)),
-  --     note q := @eq_of_is_contr _ H''
-  --       ⟨up ∘ pushout.elim h k p ∘ down ∘ (center' H').1,
-  --        (λb, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr1 (center' H').2 b),
-  --         λc, ap (up ∘ pushout.elim h k p ∘ down) (prod.pr2 (center' H').2 c))⟩
-  --       ⟨up, (λx, idp, λx, idp)⟩,
-  --     exact ap down (ap10 q..1 d)
-  --     }
-  -- end
+  definition pushout_compose_equiv {A B C D E : Type} (f : A → B) {g : A → C} {h : B → D} {hf : A → D}
+    {k : B → E} (e : E ≃ pushout f g) (p : k ~ e⁻¹ᵉ ∘ inl) (q : h ∘ f ~ hf) :
+    pushout h k ≃ pushout hf g :=
+  begin
+    refine _ ⬝e pushout_compose f g h ⬝e _,
+    { fapply pushout.equiv,
+        reflexivity,
+        reflexivity,
+        exact e,
+        reflexivity,
+        exact homotopy_of_homotopy_inv_post e _ _ p },
+    { fapply pushout.equiv,
+        reflexivity,
+        reflexivity,
+        reflexivity,
+        exact q,
+        reflexivity },
+  end
 
 end pushout
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index bb79785..486ef75 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -1,8 +1,8 @@
 -- Authors: Floris van Doorn
 
-import homotopy.smash ..move_to_lib
+import homotopy.smash ..move_to_lib .pushout
 
-open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge
+open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc function
 
   /- smash A (susp B) = susp (smash A B) <- this follows from associativity and smash with S¹ -/
 
@@ -13,9 +13,9 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w
 
   /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
 
-namespace smash
+variables {A B : Type*}
 
-  variables {A B : Type*}
+namespace smash
 
   definition prod_of_wedge [unfold 3] (v : pwedge A B) : A × B :=
   begin
@@ -25,7 +25,71 @@ namespace smash
     { reflexivity }
   end
 
+  definition wedge_of_sum [unfold 3] (v : A + B) : pwedge A B :=
+  begin
+    induction v with a b,
+    { exact pushout.inl a },
+    { exact pushout.inr b }
+  end
+
+
+  definition prod_of_wedge_of_sum [unfold 3] (v : A + B) : prod_of_wedge (wedge_of_sum v) = prod_of_sum v :=
+  begin
+    induction v with a b,
+    { reflexivity },
+    { reflexivity }
+  end
+
+end smash open smash
+
+namespace pushout
+
+  definition eq_inl_pushout_wedge_of_sum [unfold 3] (v : pwedge A B) :
+    inl pt = inl v :> pushout wedge_of_sum bool_of_sum :=
+  begin
+    induction v with a b,
+    { exact glue (sum.inl pt) ⬝ (glue (sum.inl a))⁻¹, },
+    { exact ap inl (glue ⋆) ⬝ glue (sum.inr pt) ⬝ (glue (sum.inr b))⁻¹, },
+    { apply eq_pathover_constant_left,
+      refine !con.right_inv ⬝pv _ ⬝vp !con_inv_cancel_right⁻¹, exact square_of_eq idp }
+  end
+
   variables (A B)
+  definition eq_inr_pushout_wedge_of_sum [unfold 3] (b : bool) :
+    inl pt = inr b :> pushout (@wedge_of_sum A B) bool_of_sum :=
+  begin
+    induction b,
+    { exact glue (sum.inl pt) },
+    { exact ap inl (glue ⋆) ⬝ glue (sum.inr pt) }
+  end
+
+  definition is_contr_pushout_wedge_of_sum : is_contr (pushout (@wedge_of_sum A B) bool_of_sum) :=
+  begin
+    apply is_contr.mk (pushout.inl pt),
+    intro x, induction x with v b w,
+    { apply eq_inl_pushout_wedge_of_sum },
+    { apply eq_inr_pushout_wedge_of_sum },
+    { apply eq_pathover_constant_left_id_right,
+      induction w with a b,
+      { apply whisker_rt, exact vrfl },
+      { apply whisker_rt, exact vrfl }}
+  end
+
+end pushout open pushout
+
+namespace smash
+
+  variables (A B)
+  definition smash_equiv_cofiber : smash A B ≃ cofiber (@prod_of_wedge A B) :=
+  begin
+    unfold [smash, cofiber, smash'], symmetry,
+    refine !pushout.symm ⬝e _,
+    fapply pushout_compose_equiv wedge_of_sum,
+    { symmetry, apply equiv_unit_of_is_contr, apply is_contr_pushout_wedge_of_sum },
+    { intro x, reflexivity },
+    { apply prod_of_wedge_of_sum }
+  end
+
   definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B :=
   begin
     fconstructor,
@@ -33,108 +97,10 @@ namespace smash
     { reflexivity }
   end
 
-  variables {A B}
-  attribute pcofiber [constructor]
-  definition pcofiber_of_smash [unfold 3] (x : smash A B) : pcofiber (@pprod_of_pwedge A B) :=
-  begin
-    induction x,
-    { exact pushout.inr (a, b) },
-    { exact pushout.inl ⋆ },
-    { exact pushout.inl ⋆ },
-    { symmetry, exact pushout.glue (pushout.inl a) },
-    { symmetry, exact pushout.glue (pushout.inr b) }
-  end
-
-  -- move
-  definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X}
-    (p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) :=
-  by induction p; reflexivity
-
-  definition smash_of_pcofiber_glue [unfold 3] (x : pwedge A B) :
-    Point (smash A B) = smash.mk (prod_of_wedge x).1 (prod_of_wedge x).2  :=
-  begin
-    induction x with a b: esimp,
-    { apply gluel' },
-    { apply gluer' },
-    { apply eq_pathover_constant_left, refine _ ⬝hp (ap_eq_ap011 smash.mk _ _ _)⁻¹,
-      rewrite [ap_compose' prod.pr1, ap_compose' prod.pr2],
-      -- TODO: define elim_glue for wedges and remove k in krewrite
-      krewrite [pushout.elim_glue], esimp, apply vdeg_square,
-      exact !con.right_inv ⬝ !con.right_inv⁻¹ }
-  end
-
-  definition smash_of_pcofiber [unfold 3] (x : pcofiber (pprod_of_pwedge A B)) : smash A B :=
-  begin
-    induction x with x x,
-    { exact smash.mk pt pt },
-    { exact smash.mk x.1 x.2 },
-    { exact smash_of_pcofiber_glue x }
-  end
-
-  set_option pp.binder_types true
-  -- maybe useful lemma:
-  open function pushout
-  definition pushout_glue_natural {A B C D E : Type} {f : A → B} {g : A → C} (a : A)
-    {h₁ : B → D} {k₁ : C → D} (p₁ : h₁ ∘ f ~ k₁ ∘ g)
-    {h₂ : B → E} {k₂ : C → E} (p₂ : h₂ ∘ f ~ k₂ ∘ g) :
-    @square (pushout (pushout.elim h₁ k₁ p₁) (pushout.elim h₂ k₂ p₂)) _ _ _ _
-      (pushout.glue (inl (f a))) (pushout.glue (inr (g a)))
-      (ap pushout.inl (p₁ a)) (ap pushout.inr (p₂ a)) :=
-  begin
-    apply square_of_eq, symmetry,
-    refine _ ⬝ (ap_con_eq_con_ap (pushout.glue) (pushout.glue a)) ⬝ _,
-    apply whisker_right, exact sorry,
-    apply whisker_left, exact sorry
-  end
-
-  definition pcofiber_of_smash_of_pcofiber (x : pcofiber (pprod_of_pwedge A B)) :
-    pcofiber_of_smash (smash_of_pcofiber x) = x :=
-  begin
-    induction x with x x,
-    { refine (pushout.glue pt)⁻¹ },
-    { induction x with a b, reflexivity },
-    { apply eq_pathover_id_right, esimp,
-      refine ap_compose' pcofiber_of_smash smash_of_pcofiber (cofiber.glue x) ⬝ph _,
-      refine ap02 _ !cofiber.elim_glue' ⬝ph _,
-      induction x,
-      { refine (!ap_con ⬝ !elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻² ⬝ !inv_inv)) ⬝ph _,
-        apply whisker_tl, apply hrfl },
-      { esimp, refine (!ap_con ⬝ !elim_gluer ◾ (!ap_inv ⬝ !elim_gluer⁻² ⬝ !inv_inv)) ⬝ph _,
-        apply square_of_eq, esimp, apply whisker_right, apply inverse2,
-        refine _ ⬝ (ap_con_eq_con_ap (pushout.glue) (wedge.glue A B))⁻¹ ⬝ _,
-        { apply whisker_left, refine _ ⬝ (ap_compose' pushout.inr _ _)⁻¹,
-          exact ap02 _ !pushout.elim_glue⁻¹ },
-        { refine whisker_right _ _ ⬝ !idp_con, apply ap_constant }},
-      { exact sorry }}
-  end
-
-  definition smash_of_pcofiber_of_smash (x : smash A B) :
-    smash_of_pcofiber (pcofiber_of_smash x) = x :=
-  begin
-    induction x,
-    { reflexivity },
-    { apply gluel },
-    { apply gluer },
-    { apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _,
-      refine ap02 _ !elim_gluel ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _,
-      esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right _ !inv_con_inv_right⁻¹,
-      exact !inv_con_cancel_right⁻¹ },
-    { apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _,
-      refine ap02 _ !elim_gluer ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _,
-      esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right _ !inv_con_inv_right⁻¹,
-      exact !inv_con_cancel_right⁻¹ },
-  end
-
-  variables (A B)
   definition smash_pequiv_pcofiber [constructor] : smash A B ≃* pcofiber (pprod_of_pwedge A B) :=
   begin
-    fapply pequiv_of_equiv,
-    { fapply equiv.MK,
-      { apply pcofiber_of_smash },
-      { apply smash_of_pcofiber },
-      { exact pcofiber_of_smash_of_pcofiber },
-      { exact smash_of_pcofiber_of_smash }},
-    { symmetry, exact pushout.glue (Point (pwedge A B)) }
+    apply pequiv_of_equiv (smash_equiv_cofiber A B),
+    exact (cofiber.glue pt)⁻¹
   end
 
   variables {A B}
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 8273be0..08b4665 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -5,8 +5,11 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
      is_trunc function sphere
 
-attribute pwedge [constructor]
+attribute equiv_unit_of_is_contr [constructor]
+attribute pwedge pushout.symm pushout.equiv pushout.is_equiv_functor [constructor]
 attribute is_succ_add_right is_succ_add_left is_succ_bit0 [constructor]
+attribute pushout.functor [unfold 16]
+attribute pushout.transpose [unfold 6]
 
 namespace eq
 
@@ -16,6 +19,11 @@ namespace eq
   definition id_compose {A B : Type} (f : A → B) : id ∘ f ~ f :=
   by reflexivity
 
+  -- move
+  definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X}
+    (p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) :=
+  by induction p; reflexivity
+
 end eq
 
 namespace cofiber