more pushout lemmas, continue with smash of the circle

homotopy/pushout.hlean

@@ -2,7 +2,7 @@
 
 import ..move_to_lib
 
-open eq function is_trunc sigma prod sigma.ops lift is_equiv equiv
+open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool
 
 namespace pushout
 
@@ -33,6 +33,8 @@ namespace pushout
   definition is_pushout2 [reducible] : Type :=
   Π(X : Type.{max u₁ u₂ u₃ u₄}), is_equiv (cocone_of_map p X)
 
+  section
+  open sigma.ops
   protected definition inv_left (H : is_pushout2 p) {X : Type} (v : cocone p X) :
     (cocone_of_map p X)⁻¹ᶠ v ∘ h ~ prod.pr1 v.1 :=
   ap10 (ap prod.pr1 (right_inv (cocone_of_map p X) v)..1)
@@ -40,6 +42,7 @@ namespace pushout
   protected definition inv_right (H : is_pushout2 p) {X : Type} (v : cocone p X) :
     (cocone_of_map p X)⁻¹ᶠ v ∘ k ~ prod.pr2 v.1 :=
   ap10 (ap prod.pr2 (right_inv (cocone_of_map p X) v)..1)
+  end
 
   section
     local attribute is_pushout [reducible]
@@ -50,11 +53,6 @@ namespace pushout
     definition is_prop_is_pushout2 : is_prop (is_pushout2 p) :=
     _
   end
-print ap_ap10
-print apd10_ap
-print apd10
-print ap10
-print apd10_ap_precompose_dependent
 
   definition ap_eq_apd10_ap {A B : Type} {C : B → Type} (f : A → Πb, C b) {a a' : A} (p : a = a') (b : B)
     : ap (λa, f a b) p = apd10 (ap f p) b :=
@@ -127,7 +125,7 @@ print apd10_ap_precompose_dependent
 --       }
 --   end
 
-  definition pushout_compose_to [unfold 8] {A B C D : Type} {f : A → B} {g : A → C} {h : B → D}
+  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
     induction x with d y b,
@@ -139,7 +137,7 @@ print apd10_ap_precompose_dependent
     { reflexivity }
   end
 
-  definition pushout_compose_from [unfold 8] {A B C D : Type} {f : A → B} {g : A → C} {h : B → D}
+  definition pushout_vcompose_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,
@@ -148,42 +146,45 @@ print apd10_ap_precompose_dependent
     { 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) :
+  definition pushout_vcompose [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 pushout_compose_to },
-    { exact pushout_compose_from },
+    { exact pushout_vcompose_to },
+    { exact pushout_vcompose_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_compose pushout_vcompose_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 _,
+        { apply eq_pathover, refine ap_compose pushout_vcompose_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 }}
+        refine ap_compose pushout_vcompose_from _ _ ⬝ ap02 _ !elim_glue ⬝ph _, apply square_of_eq,
+        reflexivity }}
   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) :=
+  definition pushout_hcompose {A B C D : Type} (f : A → B) (g : A → C) (h : C → D) :
+    pushout (@inr _ _ _ f g) h ≃ pushout f (h ∘ g) :=
   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
+    pushout (@inr _ _ _ f g) h ≃ pushout h (@inr _ _ _ f g) : pushout.symm
+      ... ≃ pushout h (@inl _ _ _ g f) :
+              pushout.equiv _ _ _ _ erfl erfl (pushout.symm f g) (λa, idp) (λa, idp)
+      ... ≃ pushout (h ∘ g) f : pushout_vcompose
+      ... ≃ pushout f (h ∘ g) : pushout.symm
 
 
-  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) :
+  definition pushout_vcompose_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 _,
+    refine _ ⬝e pushout_vcompose f g h ⬝e _,
     { fapply pushout.equiv,
         reflexivity,
         reflexivity,
@@ -198,4 +199,160 @@ print apd10_ap_precompose_dependent
         reflexivity },
   end
 
+  definition pushout_hcompose_equiv {A B C D E : Type} {f : A → B} (g : A → C) {h : C → E}
+    {hg : A → E} {k : C → D} (e : D ≃ pushout f g) (p : k ~ e⁻¹ᵉ ∘ inr) (q : h ∘ g ~ hg) :
+    pushout k h ≃ pushout f hg :=
+  calc
+    pushout k h ≃ pushout h k : pushout.symm
+      ... ≃ 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
+    induction x with b c a,
+    { exact g (f⁻¹ b) },
+    { exact c },
+    { exact ap g (left_inv f a) }
+  end
+
+  definition pushout_of_equiv_left [constructor] {A B C : Type} (f : A ≃ B) (g : A → C) :
+    pushout f g ≃ C :=
+  begin
+    fapply equiv.MK,
+    { exact pushout_of_equiv_left_to },
+    { exact inr },
+    { intro c, reflexivity },
+    { intro x, induction x with b c a,
+      { exact (glue (f⁻¹ b))⁻¹ ⬝ ap inl (right_inv f b) },
+      { reflexivity },
+      { apply eq_pathover_id_right, refine ap_compose inr _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
+        apply move_top_of_left, apply move_left_of_bot,
+        refine ap02 _ (adj f _) ⬝ !ap_compose⁻¹ ⬝pv _ ⬝vp !ap_compose,
+        apply natural_square_tr }}
+  end
+
+  definition pushout_of_equiv_right [constructor] {A B C : Type} (f : A → B) (g : A ≃ C) :
+    pushout f g ≃ B :=
+  calc
+    pushout f g ≃ pushout g f : pushout.symm f g
+            ... ≃ B           : pushout_of_equiv_left g f
+
+  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 _ ⋆) :=
+  begin
+    induction x with b c a,
+    { exact inl (sum.inl b) },
+    { exact inl (sum.inr c) },
+    { exact glue (sum.inl a) ⬝ (glue (sum.inr ⋆))⁻¹ }
+  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₀) :=
+  begin
+    induction x with v u v,
+    { induction v with b c, exact inl b, exact inr c },
+    { exact inr 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 _ ⋆) :=
+  begin
+    fapply equiv.MK,
+    { exact pushout_const_equiv_to },
+    { exact pushout_const_equiv_from },
+    { intro x, induction x with v u v,
+      { 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},
+        { induction u, exact square_of_eq idp }}},
+    { intro x, induction x with b c 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⁻²) }}
+  end
+
+  -- 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
+
+  definition psum_of_pbool [constructor] (A B : Type*) : pbool →* (A +* B) :=
+  pmap.mk (sum_of_bool A B) idp
+
+  -- move to wedge
+  definition wedge_equiv_pushout_sum [constructor] (A B : Type*) :
+    wedge A B ≃ pushout (sum_of_bool A B) (const bool ⋆) :=
+  begin
+    refine pushout_const_equiv _ _ ⬝e _,
+    fapply pushout.equiv,
+      exact bool_equiv_unit_sum_unit⁻¹ᵉ,
+      reflexivity,
+      reflexivity,
+      intro x, induction x: reflexivity,
+      reflexivity
+  en
+d
+  open prod.ops
+  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
+    induction xd with x d, induction x with b c a,
+    { exact inl (b, d) },
+    { exact inr (c, d) },
+    { exact glue (a, d) }
+  end
+
+  definition pushout_prod_equiv_from [unfold 7] {A B C D : Type} {f : A → B} {g : A → C}
+    (x : pushout (prod_functor f (@id D)) (prod_functor g id)) : pushout f g × D :=
+  begin
+    induction x with bd cd ad,
+    { exact (inl bd.1, bd.2) },
+    { exact (inr cd.1, cd.2) },
+    { exact prod_eq (glue ad.1) idp }
+  end
+
+  definition pushout_prod_equiv {A B C D : Type} (f : A → B) (g : A → C) :
+    pushout f g × D ≃ pushout (prod_functor f (@id D)) (prod_functor g id) :=
+  begin
+    fapply equiv.MK,
+    { exact pushout_prod_equiv_to },
+    { exact pushout_prod_equiv_from },
+    { intro x, induction x with bd cd ad,
+      { induction bd, reflexivity },
+      { induction cd, reflexivity },
+      { induction ad with a d, apply eq_pathover_id_right, apply hdeg_square,
+        refine ap_compose pushout_prod_equiv_to _ _ ⬝ ap02 _ !elim_glue ⬝ _, esimp,
+        exact !ap_prod_elim ⬝ !idp_con ⬝ !elim_glue }},
+    { intro xd, induction xd with x d, induction x with b c a,
+      { reflexivity },
+      { reflexivity },
+      { apply eq_pathover, apply hdeg_square,
+        exact ap_compose pushout_prod_equiv_from _ _ ⬝ ap02 _ !elim_glue ⬝ !elim_glue }}
+  end
+
 end pushout

homotopy/smash.hlean

@@ -1,8 +1,9 @@
 -- Authors: Floris van Doorn
 
-import homotopy.smash ..move_to_lib .pushout
+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
+open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
+     function red_susp
 
   /- smash A (susp B) = susp (smash A B) <- this follows from associativity and smash with S¹ -/
 
@@ -17,6 +18,16 @@ variables {A B : Type*}
 
 namespace smash
 
+  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')⁻¹ :=
+  !ap_con ⬝ !elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻²)
+
+  theorem elim_gluer' {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
+    (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b b' : B) :
+    ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer' b b') = Pgr b ⬝ (Pgr b')⁻¹ :=
+  !ap_con ⬝ !elim_gluer ◾ (!ap_inv ⬝ !elim_gluer⁻²)
+
   definition prod_of_wedge [unfold 3] (v : pwedge A B) : A × B :=
   begin
     induction v with a b ,
@@ -75,6 +86,21 @@ namespace pushout
       { apply whisker_rt, exact vrfl }}
   end
 
+  definition bool_of_sum_of_bool {A B : Type*} (b : bool) : bool_of_sum (sum_of_bool A B b) = b :=
+  by induction b: reflexivity
+
+  /- a different proof, using pushout lemmas, and the fact that the wedge is the pushout of
+     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)
+             _ _ ⬝e _,
+      exact erfl,
+      reflexivity,
+      exact bool_of_sum_of_bool,
+    apply pushout_of_equiv_right
+  end
+
 end pushout open pushout
 
 namespace smash
@@ -84,7 +110,7 @@ namespace smash
   begin
     unfold [smash, cofiber, smash'], symmetry,
     refine !pushout.symm ⬝e _,
-    fapply pushout_compose_equiv wedge_of_sum,
+    fapply pushout_vcompose_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 }
@@ -138,9 +164,113 @@ namespace smash
     { reflexivity }
   end
 
+  /- smash A S¹ = red_susp A -/
+
+  definition circle_elim_constant [unfold 5] {A : Type} {a : A} {p : a = a} (r : p = idp) (x : S¹) :
+    circle.elim a p x = a :=
+  begin
+    induction x,
+    { reflexivity },
+    { apply eq_pathover_constant_right, apply hdeg_square, exact !elim_loop ⬝ r }
+  end
+
+
+  definition red_susp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : red_susp A :=
+  begin
+    induction x using smash.elim,
+    { induction b, exact base, exact equator a },
+    { exact base },
+    { exact base },
+    { reflexivity },
+    { exact circle_elim_constant equator_pt b }
+  end
+
+  definition smash_pcircle_of_red_susp [unfold 2] (x : red_susp A) : smash A S¹* :=
+  begin
+    induction x,
+    { exact pt },
+    { exact gluel' pt a ⬝ ap (smash.mk a) loop ⬝ gluel' a pt },
+    { refine !con.right_inv ◾ _ ◾ !con.right_inv,
+      exact ap_is_constant gluer loop ⬝ !con.right_inv }
+  end
+
+  definition smash_pcircle_of_psusp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
+    smash_pcircle_of_red_susp (red_susp_of_smash_pcircle (smash.mk a x)) = smash.mk a x :=
+  begin
+    induction x,
+    { exact gluel' pt a },
+    { exact abstract begin apply eq_pathover,
+      refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _,
+      refine ap02 _ (elim_loop pt (equator a)) ⬝ !elim_equator ⬝ph _,
+      -- make everything below this a lemma defined by path induction?
+      refine !con_idp⁻¹ ⬝pv _, refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb,
+      apply whisker_tl, apply hrfl end end }
+  end
+
+  definition concat2o [unfold 10] {A B : Type} {f g h : A → B} {q : f ~ g} {r : g ~ h} {a a' : A}
+    {p : a = a'} (s : q a =[p] q a') (t : r a =[p] r a') : q a ⬝ r a =[p] q a' ⬝ r a' :=
+  by induction p; exact idpo
+
+  definition apd_con_fn [unfold 10] {A B : Type} {f g h : A → B} {q : f ~ g} {r : g ~ h} {a a' : A}
+    (p : a = a') : apd (λa, q a ⬝ r a) p = concat2o (apd q p) (apd r p) :=
+  by induction p; reflexivity
+
+  -- definition apd_con_fn_constant [unfold 10] {A B : Type} {f : A → B} {b b' : B} {q : Πa, f a = b}
+  --   {r : b = b'} {a a' : A} (p : a = a') :
+  --   apd (λa, q a ⬝ r) p = concat2o (apd q p) (pathover_of_eq _ idp) :=
+  -- by induction p; reflexivity
+
+  theorem apd_constant' {A A' : Type} {B : A' → Type} {a₁ a₂ : A} {a' : A'} (b : B a')
+    (p : a₁ = a₂) : apd (λx, b) p = pathover_of_eq p idp :=
+  by induction p; reflexivity
+
+  definition smash_pcircle_pequiv_red [constructor] (A : Type*) : smash A S¹* ≃* red_susp A :=
+  begin
+    fapply pequiv_of_equiv,
+    { fapply equiv.MK,
+      { exact red_susp_of_smash_pcircle },
+      { exact smash_pcircle_of_red_susp },
+      { exact abstract begin intro x, induction x,
+        { reflexivity },
+        { apply eq_pathover, apply hdeg_square,
+          refine ap_compose red_susp_of_smash_pcircle _ _ ⬝ ap02 _ !elim_equator ⬝ _ ⬝ !ap_id⁻¹,
+          refine !ap_con ⬝ (!ap_con ⬝ !elim_gluel' ◾ !ap_compose'⁻¹) ◾ !elim_gluel' ⬝ _,
+          esimp, exact !idp_con ⬝ !elim_loop },
+        { exact sorry } end end },
+      { intro x, induction x,
+        { exact smash_pcircle_of_psusp_of_smash_pcircle_pt a b },
+        { exact gluel pt },
+        { exact gluer pt },
+        { apply eq_pathover_id_right,
+          refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _,
+          unfold [red_susp_of_smash_pcircle],
+          refine ap02 _ !elim_gluel ⬝ph _,
+          esimp, apply whisker_rt, exact vrfl },
+        { apply eq_pathover_id_right,
+          refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _,
+          unfold [red_susp_of_smash_pcircle],
+          -- not sure why so many implicit arguments are needed here...
+          refine ap02 _ (@smash.elim_gluer A S¹* _ (λa, circle.elim red_susp.base (equator a)) red_susp.base red_susp.base (λa, refl red_susp.base) (circle_elim_constant equator_pt) b) ⬝ph _,
+          apply square_of_eq, induction b,
+          { exact whisker_right _ !con.right_inv },
+          { apply eq_pathover_dep, refine !apd_con_fn ⬝pho _ ⬝hop !apd_con_fn⁻¹,
+            refine ap (λx, concat2o x _) !rec_loop ⬝pho _ ⬝hop (ap011 concat2o (apd_compose1 (λa b, ap smash_pcircle_of_red_susp b) (circle_elim_constant equator_pt) loop) !apd_constant')⁻¹,
+            }
+
+          }}},
+    { 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
 
+
   definition psusp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : psusp A :=
   begin
     induction x using smash.elim,
@@ -157,7 +287,7 @@ namespace smash
     induction x,
     { exact pt },
     { exact pt },
-    { exact gluel' pt a ⬝ ap (smash.mk a) loop ⬝ gluel' a pt },
+    { exact gluel' pt a ⬝ (ap (smash.mk a) loop ⬝ gluel' a pt) },
   end
 
  -- the definitions below compile, but take a long time to do so and have sorry's in them
@@ -171,6 +301,11 @@ namespace smash
       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 _,
+      apply whisker_bl, apply whisker_lb,
+      refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, apply hrfl
+      refine !con_idp⁻¹ ⬝pv _, apply whisker_tl,
+      refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb, apply hrfl
       apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left,
       symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv,
       refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc,

move_to_lib.hlean

@@ -192,6 +192,11 @@ end is_equiv
 
 namespace prod
 
+  definition ap_prod_elim {A B C : Type} {a a' : A} {b b' : B} (m : A → B → C)
+    (p : a = a') (q : b = b') : ap (prod.rec m) (prod_eq p q)
+    = (ap (m a) q) ⬝ (ap (λx : A, m x b') p) :=
+  by cases p; cases q; constructor
+
   open prod.ops
   definition prod_pathover_equiv {A : Type} {B C : A → Type} {a a' : A} (p : a = a')
     (x : B a × C a) (x' : B a' × C a') : x =[p] x' ≃ x.1 =[p] x'.1 × x.2 =[p] x'.2 :=