Mostly formalize the pentagon of the smash product, fix the order of the arguments in the adjunction

homotopy/pushout.hlean

@@ -1,5 +1,5 @@
 
-import ..algebra.exactness homotopy.cofiber homotopy.wedge
+import ..algebra.exactness homotopy.cofiber homotopy.wedge homotopy.smash
 
 open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool cofiber
 
@@ -811,4 +811,78 @@ namespace pushout
 
   end
 
+  variables {A B : Type*}
+  open smash
+
+  definition prod_of_wedge [unfold 3] (v : wedge A B) : A × B :=
+  begin
+    induction v with a b ,
+    { exact (a, pt) },
+    { exact (pt, b) },
+    { reflexivity }
+  end
+
+  definition wedge_of_sum [unfold 3] (v : A + B) : wedge 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
+
+  definition eq_inl_pushout_wedge_of_sum [unfold 3] (v : wedge 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
+
+  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,
+      intro x, induction x,
+      reflexivity, reflexivity,
+      exact bool_of_sum_of_bool,
+    apply pushout_of_equiv_right
+  end
+
+
 end pushout

homotopy/smash.hlean

@@ -9,10 +9,8 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w
 
   /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/
 
-  /- To prove: A ∧ S¹ ≃ ΣA -/
+  /- associativity and A ∧ S¹ ≃ ΣA is proven in smash_adjoint -/
-
+variables {A A' A'' B B' B'' C C' D E F : Type*}
-  /- associativity is proven in smash_adjoint -/
-variables {A A' B B' C C' D E F : Type*}
 
 namespace smash
 
@@ -233,6 +231,8 @@ namespace smash
     reflexivity
   end
 
+  infixr ` ∧~ `:78 := smash_functor_phomotopy
+
   /- a more explicit proof, if we ever need it -/
   -- definition smash_functor_homotopy [unfold 11] {f f' : A →* C} {g g' : B →* D}
   --   (h₁ : f ~* f') (h₂ : g ~* g') : f ∧→ g ~ f' ∧→ g' :=
@@ -317,6 +317,17 @@ namespace smash
     exact !smash_functor_phomotopy_refl⁻¹
   end
 
+  definition smash_functor_eq_of_phomotopy_left (g : B →* D) {f f' : A →* C}
+    (p : f ~* f') : ap (λf, smash_functor f g) (eq_of_phomotopy p) =
+    eq_of_phomotopy (smash_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 !smash_functor_phomotopy_refl⁻¹
+  end
+
   /- the functorial action preserves compositions, the interchange law -/
   definition smash_functor_pcompose_homotopy [unfold 11] {C D E F : Type}
     (f' : C → E) (f : A → C) (g' : D → F) (g : B → D) :
@@ -348,7 +359,11 @@ namespace smash
   end
 
   definition smash_functor_split (f : A →* C) (g : B →* D) :
-    f ∧→ g ~* (pid C) ∧→ g ∘* f ∧→ (pid B)  :=
+    f ∧→ g ~* f ∧→ pid D ∘* pid A ∧→ g :=
+  smash_functor_phomotopy !pcompose_pid⁻¹* !pid_pcompose⁻¹* ⬝* !smash_functor_pcompose
+
+  definition smash_functor_split_rev (f : A →* C) (g : B →* D) :
+    f ∧→ g ~* pid C ∧→ g ∘* f ∧→ pid B :=
   smash_functor_phomotopy !pid_pcompose⁻¹* !pcompose_pid⁻¹* ⬝* !smash_functor_pcompose
 
   /- An alternative proof which doesn't start by applying inductions, so which is more explicit -/
@@ -429,6 +444,337 @@ namespace smash
   !smash_functor_pcompose⁻¹* ⬝* smash_functor_phomotopy p q ⬝* !smash_functor_pcompose
   end
 
+
+  /- f ∧ g is a pointed equivalence if f and g are -/
+  definition smash_functor_using_pushout [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D :=
+  begin
+    fapply pushout.functor (sum_functor f g) (prod_functor f g) id,
+    { intro v, induction v with a b,
+      exact prod_eq idp (respect_pt g),
+      exact prod_eq (respect_pt f) idp },
+    { intro v, induction v with a b: reflexivity }
+  end
+
+  definition smash_functor_homotopy_pushout_functor (f : A →* C) (g : B →* D) :
+    f ∧→ g ~ smash_functor_using_pushout f g :=
+  begin
+    intro x, induction x,
+    { reflexivity },
+    { reflexivity },
+    { reflexivity },
+    { apply eq_pathover, refine !elim_gluel ⬝ph _ ⬝hp !pushout.elim_glue⁻¹,
+      apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ },
+    { apply eq_pathover, refine !elim_gluer ⬝ph _ ⬝hp !pushout.elim_glue⁻¹,
+      apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ }
+  end
+
+  local attribute is_equiv_sum_functor [instance]
+  definition smash_pequiv [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D :=
+  begin
+    fapply pequiv_of_pmap (f ∧→ g),
+    refine @homotopy_closed _ _ _ _ _ (smash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ,
+    apply pushout.is_equiv_functor
+  end
+
+  infixr ` ∧≃ `:80 := smash_pequiv
+
+
+  definition smash_pequiv_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B :=
+  f ∧≃ pequiv.rfl
+
+  definition smash_pequiv_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D :=
+  pequiv.rfl ∧≃ g
+
+  /- f ∧ g is constant if f is constant -/
+  definition smash_functor_pconst_left_homotopy [unfold 6] {B' : Type} (f : B → B') (x : A ∧ B) :
+    (pconst A A' ∧→ 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 smash_functor_pconst_left (f : B →* B') : pconst A A' ∧→ f ~* pconst (A ∧ B) (A' ∧ B') :=
+  begin
+    induction B' with B', induction f with f f₀, esimp at *, induction f₀,
+    fapply phomotopy.mk,
+    { exact smash_functor_pconst_left_homotopy f },
+    { rexact con.right_inv (gluer (f pt)) }
+  end
+
+  definition smash_functor_pconst_left_phomotopy {f f' : B →* B'} (p : f ~* f') :
+    phomotopy.refl (pconst A A') ∧~ p ⬝* smash_functor_pconst_left f' = smash_functor_pconst_left f :=
+  begin
+    induction p using phomotopy_rec_idp,
+    exact !smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans
+  end
+
+  /- This makes smash_functor into a pointed map (B →* B') →* (A ∧ B →* A ∧ B') -/
+
+  definition smash_functor_left [constructor] (A A' B : Type*) :
+    ppmap A A' →* ppmap (A ∧ B) (A' ∧ B) :=
+  pmap.mk (λf, f ∧→ pid B) (eq_of_phomotopy (smash_functor_pconst_left (pid B)))
+
+  /- We want to show that smash_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 {A B C : Type} {g : B → C} {f : A → B} {a₁ a₂ : A} {b₀ : B}
+    {p : f ~ λa, b₀} {q : Πa, g (f a) = g b₀} (r : (λa, ap g (p a)) ~ q) :
+    cube (hrfl ⬝hp (r a₁)⁻¹) hrfl
+         (my_squarel (q a₁) (q a₂)) (aps g (my_squarel (p a₁) (p a₂)))
+         (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (r a₁) ◾ (r a₂)⁻²)⁻¹)
+           (hrfl ⬝hp (r a₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) :=
+  begin
+    induction r using homotopy.rec_on_idp, induction p using homotopy.rec_on_idp_left, exact idc
+  end
+
+  private definition my_cube_fillerr {B C : Type} {g : B → C} {b₀ bl br : B}
+    {pl : b₀ = bl} {pr : b₀ = br} {ql : g b₀ = g bl} {qr : g b₀ = g br}
+    (sl : ap g pl = ql) (sr : ap g pr = qr) :
+    cube (hrfl ⬝hp sr⁻¹) hrfl
+         (my_squarer ql qr) (aps g (my_squarer pl pr))
+         (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ sl ◾ sl⁻²)⁻¹)
+         (hrfl ⬝hp sr⁻²⁻¹ ⬝hp !ap_inv⁻¹) :=
+  begin
+    induction sr, induction sl, induction pr, induction pl, exact idc
+  end
+
+  definition smash_functor_pcompose_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 (smash_functor_pcompose_homotopy f' (λ a, a₀') g' g x)
+    idp
+    (smash_functor_pconst_left_homotopy (λ a, g' (g a)) x)
+    (ap (smash_functor' (pmap.mk f' (refl (f' a₀'))) (pmap.mk g' (refl (g' (g b₀)))))
+      (smash_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 smash_functor_pcompose_pconst2 (f' : A' →* A'') (g' : B' →* B'') (g : B →* B') :
+    phsquare (smash_functor_pcompose f' (pconst A A') g' g)
+             (smash_functor_pconst_left (g' ∘* g))
+             (smash_functor_phomotopy (pcompose_pconst f') phomotopy.rfl)
+             (pwhisker_left (f' ∧→ g') (smash_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 !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹,
+    fapply phomotopy_eq,
+    { intro x, refine eq_of_square _ ⬝ !con_idp,
+      exact smash_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 ⬝ _,
+      exact sorry, -- TODO: FIX, the proof below should work (with some small changes)
+      -- refine _ ⬝ whisker_left _ _,
+      -- rotate 2, refine ap (whisker_left _) _, symmetry, exact !idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con,
+      -- symmetry, apply whisker_left_idp
+      }
+  end
+
+  /- a version where the left maps are identities -/
+  definition smash_functor_pcompose_pconst2_pid (f' : A' →* A'') :
+    phsquare (smash_functor_pcompose_pid B f' (pconst A A'))
+             (smash_functor_pconst_left (pid B))
+             (pcompose_pconst f' ∧~ phomotopy.rfl)
+             (pwhisker_left (f' ∧→ pid B) (smash_functor_pconst_left (pid B)) ⬝*
+               pcompose_pconst (f' ∧→ pid B)) :=
+  (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv**
+  smash_functor_pcompose_pconst2 f' (pid B) (pid B)
+
+  /- a small rewrite of the previous -/
+  -- definition smash_functor_pcompose_pid_pconst' (f' : A' →* A'') :
+  --   pwhisker_left (f' ∧→ pid B) (smash_functor_pconst_left (pid B)) ⬝*
+  --   pcompose_pconst (f' ∧→ pid B) =
+  --   (smash_functor_pcompose_pid B f' (pconst A A'))⁻¹* ⬝*
+  --   (pcompose_pconst f' ∧~ phomotopy.rfl ⬝*
+  --   smash_functor_pconst_left (pid B)) :=
+  -- begin
+  --   apply eq_symm_trans_of_trans_eq,
+  --   exact smash_functor_pcompose_pid_pconst f'
+  -- end
+
+  /- if f' is constant -/
+  definition smash_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 (smash_functor_pcompose_homotopy (λa', a₀'') f g' g x)
+    idp
+    (smash_functor_pconst_left_homotopy (λ a, g' (g a)) x)
+    (smash_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 (smash_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 (smash_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 smash_functor_pcompose_pconst1 (f : A →* A') (g' : B' →* B'') (g : B →* B') :
+    phsquare (smash_functor_pcompose (pconst A' A'') f g' g)
+             (smash_functor_pconst_left (g' ∘* g))
+             (pconst_pcompose f ∧~ phomotopy.rfl)
+             (pwhisker_right (f ∧→ g) (smash_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 !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹,
+    fapply phomotopy_eq,
+    { intro x, refine eq_of_square (smash_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 smash_functor_pcompose_pconst1_pid (f : A →* A') :
+    phsquare (smash_functor_pcompose_pid B (pconst A' A'') f)
+             (smash_functor_pconst_left (pid B))
+             (pconst_pcompose f ∧~ phomotopy.rfl)
+             (pwhisker_right (f ∧→ pid B) (smash_functor_pconst_left (pid B)) ⬝*
+               pconst_pcompose (f ∧→ pid B)) :=
+  (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv**
+  smash_functor_pcompose_pconst1 f (pid B) (pid B)
+
+  /- Using these lemmas we show that smash_functor_left is natural in all arguments -/
+
+  definition smash_functor_left_natural_left (f : A' →* A) :
+    psquare (smash_functor_left A B C) (smash_functor_left A' B C)
+            (ppcompose_right f) (ppcompose_right (f ∧→ pid C)) :=
+  begin
+    refine _⁻¹*,
+    fapply phomotopy_mk_ppmap,
+    { intro g, exact smash_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 !smash_functor_eq_of_phomotopy_left ⬝
+        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
+      apply smash_functor_pcompose_pconst1_pid }
+  end
+
+  definition smash_functor_left_natural_middle (f : B →* B') :
+    psquare (smash_functor_left A B C) (smash_functor_left A B' C)
+            (ppcompose_left f) (ppcompose_left (f ∧→ pid C)) :=
+  begin
+    refine _⁻¹*,
+    fapply phomotopy_mk_ppmap,
+    { exact smash_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 !smash_functor_eq_of_phomotopy_left ⬝
+        !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
+      apply smash_functor_pcompose_pconst2_pid }
+  end
+
+  definition smash_functor_left_natural_right (f : C →* C') :
+    psquare (smash_functor_left A B C) (ppcompose_right (pid A ∧→ f))
+            (smash_functor_left A B C') (ppcompose_left (pid B ∧→ f)) :=
+  begin
+    refine _⁻¹*,
+    fapply phomotopy_mk_ppmap,
+    { intro g, exact smash_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 _ !smash_functor_pcompose_pconst1⁻¹ʰ**) ⬝h**
+        (!smash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !smash_functor_pcompose_pconst2 ⬝vp** _,
+      refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl,
+      refine idp ◾** !refl_trans ⬝ !trans_left_inv }
+  end
+
+
+  /- the following is not really used, but a symmetric version of the natural equivalence
+     smash_functor_left -/
   /- f ∧ g is constant if g is constant -/
   definition smash_functor_pconst_right_homotopy [unfold 6] {C : Type} (f : A → C) (x : A ∧ B) :
     (pmap_of_map f pt ∧→ pconst B D) x = pt :=
@@ -474,36 +820,7 @@ namespace smash
      exchange, or directly. We need to show that these two proofs result in the same pointed
      homotopy. First we do the case where g is constant -/
 
-  private definition my_squarel {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₂ = a₃) :
+  definition smash_functor_pcompose_pconst4_homotopy {A B C D E F : Type}
-    square (p₁ ⬝ p₂⁻¹) p₂⁻¹ p₁ idp :=
-  proof square_of_eq idp qed
-
-  private definition my_squarer {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₁ = a₂) :
-    square (p₁ ⬝ p₁⁻¹) p₂⁻¹ p₂ idp :=
-  proof square_of_eq (con.right_inv p₁ ⬝ (con.right_inv p₂)⁻¹) qed
-
-  private definition my_cube_fillerl {A B C : Type} {g : B → C} {f : A → B} {a₁ a₂ : A} {b₀ : B}
-    {p : f ~ λa, b₀} {q : Πa, g (f a) = g b₀} (r : (λa, ap g (p a)) ~ q) :
-    cube (hrfl ⬝hp (r a₁)⁻¹) hrfl
-         (my_squarel (q a₁) (q a₂)) (aps g (my_squarel (p a₁) (p a₂)))
-         (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (r a₁) ◾ (r a₂)⁻²)⁻¹)
-           (hrfl ⬝hp (r a₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) :=
-  begin
-    induction r using homotopy.rec_on_idp, induction p using homotopy.rec_on_idp_left, exact idc
-  end
-
-  private definition my_cube_fillerr {B C : Type} {g : B → C} {b₀ bl br : B}
-    {pl : b₀ = bl} {pr : b₀ = br} {ql : g b₀ = g bl} {qr : g b₀ = g br}
-    (sl : ap g pl = ql) (sr : ap g pr = qr) :
-    cube (hrfl ⬝hp sr⁻¹) hrfl
-         (my_squarer ql qr) (aps g (my_squarer pl pr))
-         (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ sl ◾ sl⁻²)⁻¹)
-         (hrfl ⬝hp sr⁻²⁻¹ ⬝hp !ap_inv⁻¹) :=
-  begin
-    induction sr, induction sl, induction pr, induction pl, exact idc
-  end
-
-  definition smash_functor_pcompose_pconst_homotopy {A B C D E F : Type}
     (a₀ : A) (b₀ : B) (d₀ : D) (f' : C → E) (f : A → C) (g : D → F)
     (x : pointed.MK A a₀ ∧ pointed.MK B b₀) :
     square (smash_functor_pcompose_homotopy f' f g (λ a, d₀) x)
@@ -540,7 +857,7 @@ namespace smash
       apply my_cube_fillerr end end }
   end
 
-  definition smash_functor_pcompose_pconst (f' : C →* E) (f : A →* C) (g : D →* F) :
+  definition smash_functor_pcompose_pconst4 (f' : C →* E) (f : A →* C) (g : D →* F) :
     phsquare (smash_functor_pcompose f' f g (pconst B D))
              (smash_functor_pconst_right (f' ∘* f))
              (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g))
@@ -554,7 +871,7 @@ namespace smash
     refine !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹,
     fapply phomotopy_eq,
     { intro x, refine eq_of_square _ ⬝ !con_idp,
-      exact smash_functor_pcompose_pconst_homotopy a₀ b₀ d₀ f' f g x, },
+      exact smash_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,
@@ -568,29 +885,29 @@ namespace smash
   end
 
   /- a version where the left maps are identities -/
-  definition smash_functor_pid_pcompose_pconst (g : D →* F) :
+  definition smash_functor_pcompose_pconst4_pid (g : D →* F) :
     phsquare (smash_functor_pid_pcompose A g (pconst B D))
              (smash_functor_pconst_right (pid A))
              (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g))
              (pwhisker_left (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝*
                pcompose_pconst (pid A ∧→ g)) :=
   (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv**
-  smash_functor_pcompose_pconst (pid A) (pid A) g
+  smash_functor_pcompose_pconst4 (pid A) (pid A) g
 
   /- a small rewrite of the previous -/
-  definition smash_functor_pid_pcompose_pconst' (g : D →* F) :
+  -- definition smash_functor_pid_pcompose_pconst' (g : D →* F) :
-    pwhisker_left (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝*
+  --   pwhisker_left (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝*
-    pcompose_pconst (pid A ∧→ g) =
+  --   pcompose_pconst (pid A ∧→ g) =
-    (smash_functor_pid_pcompose A g (pconst B D))⁻¹* ⬝*
+  --   (smash_functor_pid_pcompose A g (pconst B D))⁻¹* ⬝*
-    (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g) ⬝*
+  --   (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g) ⬝*
-    smash_functor_pconst_right (pid A)) :=
+  --   smash_functor_pconst_right (pid A)) :=
-  begin
+  -- begin
-    apply eq_symm_trans_of_trans_eq,
+  --   apply eq_symm_trans_of_trans_eq,
-    exact smash_functor_pid_pcompose_pconst g
+  --   exact smash_functor_pid_pcompose_pconst g
-  end
+  -- end
 
   /- if g' is constant -/
-  definition smash_functor_pconst_pcompose_homotopy [unfold 13] {A B C D E F : Type}
+  definition smash_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 (smash_functor_pcompose_homotopy f' f (λ a, x₀) g x)
@@ -635,7 +952,7 @@ namespace smash
       exact rfl2 end end },
   end
 
-  definition smash_functor_pconst_pcompose (f' : C →* E) (f : A →* C) (g : B →* D) :
+  definition smash_functor_pcompose_pconst3 (f' : C →* E) (f : A →* C) (g : B →* D) :
     phsquare (smash_functor_pcompose f' f (pconst D F) g)
              (smash_functor_pconst_right (f' ∘* f))
              (smash_functor_phomotopy phomotopy.rfl (pconst_pcompose g))
@@ -648,7 +965,7 @@ namespace smash
     esimp at *, induction f'₀, induction f₀, induction g₀,
     refine !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹,
     fapply phomotopy_eq,
-    { intro x, refine eq_of_square (smash_functor_pconst_pcompose_homotopy a₀ b₀ x₀ f' f g x) },
+    { intro x, refine eq_of_square (smash_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 ⬝
@@ -658,14 +975,14 @@ namespace smash
   end
 
   /- a version where the left maps are identities -/
-  definition smash_functor_pid_pconst_pcompose (g : B →* D) :
+  definition smash_functor_pcompose_pconst3_pid (g : B →* D) :
     phsquare (smash_functor_pid_pcompose A (pconst D F) g)
              (smash_functor_pconst_right (pid A))
              (smash_functor_phomotopy phomotopy.rfl (pconst_pcompose g))
              (pwhisker_right (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝*
                pconst_pcompose (pid A ∧→ g)) :=
   (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv**
-  smash_functor_pconst_pcompose (pid A) (pid A) g
+  smash_functor_pcompose_pconst3 (pid A) (pid A) g
 
   /- Using these lemmas we show that smash_functor_right is natural in all arguments -/
   definition smash_functor_right_natural_right (f : C →* C') :
@@ -679,7 +996,7 @@ namespace smash
         !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ ,
       refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_functor_eq_of_phomotopy ⬝
         !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
-      apply smash_functor_pid_pcompose_pconst }
+      apply smash_functor_pcompose_pconst4_pid }
   end
 
   definition smash_functor_right_natural_middle (f : B' →* B) :
@@ -693,7 +1010,7 @@ namespace smash
         !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ ,
       refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_functor_eq_of_phomotopy ⬝
         !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
-      apply smash_functor_pid_pconst_pcompose }
+      apply smash_functor_pcompose_pconst3_pid }
   end
 
   definition smash_functor_right_natural_left (f : A →* A') :
@@ -709,129 +1026,16 @@ namespace smash
       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 _ !smash_functor_pconst_pcompose⁻¹ʰ**) ⬝h**
+      refine (phmove_bot_of_left _ !smash_functor_pcompose_pconst3⁻¹ʰ**) ⬝h**
-        (!smash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !smash_functor_pcompose_pconst ⬝vp** _,
+        (!smash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !smash_functor_pcompose_pconst4 ⬝vp** _,
       refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl,
       refine idp ◾** !refl_trans ⬝ !trans_left_inv }
   end
 
-  /- f ∧ g is a pointed equivalence if f and g are -/
-  definition smash_functor_using_pushout [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D :=
-  begin
-    fapply pushout.functor (sum_functor f g) (prod_functor f g) id,
-    { intro v, induction v with a b,
-      exact prod_eq idp (respect_pt g),
-      exact prod_eq (respect_pt f) idp },
-    { intro v, induction v with a b: reflexivity }
-  end
-
-  definition smash_functor_homotopy_pushout_functor (f : A →* C) (g : B →* D) :
-    f ∧→ g ~ smash_functor_using_pushout f g :=
-  begin
-    intro x, induction x,
-    { reflexivity },
-    { reflexivity },
-    { reflexivity },
-    { apply eq_pathover, refine !elim_gluel ⬝ph _ ⬝hp !pushout.elim_glue⁻¹,
-      apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ },
-    { apply eq_pathover, refine !elim_gluer ⬝ph _ ⬝hp !pushout.elim_glue⁻¹,
-      apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ }
-  end
-
-  local attribute is_equiv_sum_functor [instance]
-  definition smash_pequiv [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D :=
-  begin
-    fapply pequiv_of_pmap (f ∧→ g),
-    refine @homotopy_closed _ _ _ _ _ (smash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ,
-    apply pushout.is_equiv_functor
-  end
-
-  definition smash_pequiv_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B :=
-  smash_pequiv f pequiv.rfl
-
-  definition smash_pequiv_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D :=
-  smash_pequiv pequiv.rfl g
-
   /- A ∧ B ≃* pcofiber (pprod_of_wedge A B) -/
 
-  definition prod_of_wedge [unfold 3] (v : wedge A B) : A × B :=
-  begin
-    induction v with a b ,
-    { exact (a, pt) },
-    { exact (pt, b) },
-    { reflexivity }
-  end
-
-  definition wedge_of_sum [unfold 3] (v : A + B) : wedge 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 : wedge 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
-
-  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,
-      intro x, induction x,
-      reflexivity, reflexivity,
-      exact bool_of_sum_of_bool,
-    apply pushout_of_equiv_right
-  end
-
-end pushout open pushout
-
-namespace smash
-
   variables (A B)
+  open pushout
 
   definition smash_equiv_cofiber : smash A B ≃ cofiber (@prod_of_wedge A B) :=
   begin

homotopy/smash_adjoint.hlean

@@ -1,8 +1,8 @@
 -- Authors: Floris van Doorn
--- in collaboration with Egbert, Stefano, Robin, Ulrik
+-- informal proofs in collaboration with Egbert, Stefano, Robin, Ulrik
 
 /- the adjunction between the smash product and pointed maps -/
-import .smash .susp ..pointed ..move_to_lib
+import .smash .susp ..pointed ..move_to_lib ..pyoneda
 
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
      function unit sigma susp sphere
@@ -12,62 +12,59 @@ namespace smash
   variables {A A' B B' C C' X X' : Type*}
 
   /- we start by defining the unit of the adjunction -/
-  definition pinl [constructor] (A : Type*) {B : Type*} (b : B) : A →* A ∧ B :=
+  definition pinr [constructor] {A : Type*} (B : Type*) (a : A) : B →* A ∧ B :=
   begin
     fapply pmap.mk,
-    { intro a, exact smash.mk a b },
+    { intro b, exact smash.mk a b },
-    { exact gluer' b pt }
+    { exact gluel' a pt }
   end
 
-  definition pinl_phomotopy {b b' : B} (p : b = b') : pinl A b ~* pinl A b' :=
+  definition pinr_phomotopy {a a' : A} (p : a = a') : pinr B a ~* pinr B a' :=
   begin
     fapply phomotopy.mk,
-    { exact ap010 (pmap.to_fun ∘ pinl A) p },
+    { exact ap010 (pmap.to_fun ∘ pinr B) p },
     { induction p, apply idp_con }
   end
 
   definition smash_pmap_unit_pt [constructor] (A B : Type*)
-    : pinl A pt ~* pconst A (A ∧ B) :=
+    : pinr B pt ~* pconst B (A ∧ B) :=
   begin
     fapply phomotopy.mk,
-    { intro a, exact gluel' a pt },
+    { intro b, exact gluer' b pt },
-    { rexact con.right_inv (gluel pt) ⬝ (con.right_inv (gluer pt))⁻¹ }
+    { rexact con.right_inv (gluer pt) ⬝ (con.right_inv (gluel pt))⁻¹ }
   end
 
-  /- We chose an unfortunate order of arguments, but it might be bothersome to change it-/
+  definition smash_pmap_unit [constructor] (A B : Type*) : A →* ppmap B (A ∧ B) :=
-  definition smash_pmap_unit [constructor] (A B : Type*) : B →* ppmap A (A ∧ B) :=
   begin
     fapply pmap.mk,
-    { exact pinl A },
+    { exact pinr B },
     { apply eq_of_phomotopy, exact smash_pmap_unit_pt A B }
   end
 
-  /- The unit is natural in the second argument -/
+  /- The unit is natural in the first argument -/
-  definition smash_functor_pid_pinl' [constructor] {A B C : Type*} (b : B) (f : B →* C) :
+  definition smash_functor_pid_pinr' [constructor] (B : Type*) (f : A →* A') (a : A) :
-    pinl A (f b) ~* smash_functor (pid A) f ∘* pinl A b :=
+    pinr B (f a) ~* smash_functor f (pid B) ∘* pinr B a :=
   begin
     fapply phomotopy.mk,
-    { intro a, reflexivity },
+    { intro b, reflexivity },
     { refine !idp_con ⬝ _,
-      induction C with C c₀, induction f with f f₀, esimp at *,
+      induction A' with A' a₀', induction f with f f₀, esimp at *,
-      induction f₀, rexact functor_gluer'2 (@id A) f b pt }
+      induction f₀, rexact functor_gluel'2 f (@id B) a pt }
   end
 
-  definition smash_pmap_unit_pt_natural [constructor] (f : B →* C) :
+  definition smash_pmap_unit_pt_natural [constructor] (B : Type*) (f : A →* A') :
-    smash_functor_pid_pinl' pt f ⬝*
+    smash_functor_pid_pinr' B f pt ⬝* pwhisker_left (smash_functor f (pid B)) (smash_pmap_unit_pt A B) ⬝*
-      pwhisker_left (smash_functor (pid A) f) (smash_pmap_unit_pt A B) ⬝*
+      pcompose_pconst (f ∧→ (pid B)) = pinr_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A' B :=
-      pcompose_pconst (smash_functor (pid A) f) =
-      pinl_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A C :=
   begin
-    induction f with f f₀, induction C with C c₀, esimp at *,
+    induction f with f f₀, induction A' with A' a₀', esimp at *,
     induction f₀, refine _ ⬝ !refl_trans⁻¹,
     refine !trans_refl ⬝ _,
     fapply phomotopy_eq',
-    { intro a, refine !idp_con ⬝ _,
+    { intro b, refine !idp_con ⬝ _,
-      rexact functor_gluel'2 (pid A) f a pt },
+      rexact functor_gluer'2 f (pid B) b pt },
     { refine whisker_right_idp _ ⬝ph _,
       refine ap (λx, _ ⬝ x) _ ⬝ph _,
-      rotate 1, rexact (functor_gluel'2_same (pid A) f pt),
+      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 _,
@@ -80,16 +77,16 @@ namespace smash
       apply whisker_tl,
       apply vdeg_square,
       refine whisker_right _ !ap_inv ⬝ _, apply inv_con_eq_of_eq_con,
-      rexact functor_gluer'2_same (pmap_of_map id (Point A)) (pmap_of_map f pt) pt }
+      rexact functor_gluel'2_same (pmap_of_map f pt) (pmap_of_map id (Point B)) pt }
   end
 
-  definition smash_pmap_unit_natural (f : B →* C) :
+  definition smash_pmap_unit_natural (B : Type*) (f : A →* A') :
-    smash_pmap_unit A C ∘* f ~*
+    psquare (smash_pmap_unit A B) (smash_pmap_unit A' B) f (ppcompose_left (f ∧→ pid B)) :=
-    ppcompose_left (smash_functor (pid A) f) ∘* smash_pmap_unit A B :=
   begin
-    induction A with A a₀, induction B with B b₀, induction C with C c₀,
+    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,
-    { esimp [pcompose], intro b, exact smash_functor_pid_pinl' b (pmap_of_map f b₀) },
+    { intro a, exact smash_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⁻¹,
@@ -97,23 +94,26 @@ namespace smash
       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 _ ⬝ smash_pmap_unit_pt_natural (pmap_of_map f b₀) ⬝ _,
+      refine _ ⬝ smash_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 counit -/
-  definition smash_pmap_counit_map [unfold 3] (af : A ∧ (ppmap A B)) : B :=
+  definition smash_pmap_counit_map [unfold 3] (fb : ppmap B C ∧ B) : C :=
   begin
-    induction af with a f a f,
+    induction fb with f b f b,
-    { exact f a },
+    { exact f b },
     { exact pt },
     { exact pt },
-    { reflexivity },
+    { exact respect_pt f },
-    { exact respect_pt f }
+    { reflexivity }
   end
 
-  definition smash_pmap_counit [constructor] (A B : Type*) : A ∧ (ppmap A B) →* B :=
+  definition smash_pmap_counit [constructor] (B C : Type*) : ppmap B C ∧ B →* C :=
   begin
     fapply pmap.mk,
     { exact smash_pmap_counit_map },
@@ -121,35 +121,35 @@ namespace smash
   end
 
   /- The counit is natural in both arguments -/
-  definition smash_pmap_counit_natural_right (g : B →* C) : g ∘* smash_pmap_counit A B ~*
+  definition smash_pmap_counit_natural_right (B : Type*) (g : C →* C') :
-    smash_pmap_counit A C ∘* smash_functor (pid A) (ppcompose_left g) :=
+    psquare (smash_pmap_counit B C) (smash_pmap_counit B C') (ppcompose_left g ∧→ pid B) g :=
   begin
-    symmetry,
+    apply ptranspose,
     fapply phomotopy.mk,
-    { intro af, induction af with a f a f,
+    { intro fb, induction fb with f b f b,
       { reflexivity },
       { exact (respect_pt g)⁻¹ },
       { exact (respect_pt g)⁻¹ },
       { apply eq_pathover,
-        refine ap_compose (smash_pmap_counit A C) _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹,
+        refine ap_compose (smash_pmap_counit B C') _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹,
         refine ap02 _ !functor_gluel ⬝ph _ ⬝hp ap02 _ !elim_gluel⁻¹,
-        refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _⁻¹ʰ,
+        refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _,
-        apply square_of_eq_bot, refine !idp_con ⬝ _,
-        induction C with C c₀, induction g with g g₀, esimp at *,
-        induction g₀, refine ap02 _ !eq_of_phomotopy_refl },
-      { apply eq_pathover,
-        refine ap_compose (smash_pmap_counit A C) _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹,
-        refine ap02 _ !functor_gluer ⬝ph _ ⬝hp ap02 _ !elim_gluer⁻¹,
-        refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _,
         refine !idp_con ⬝ph _, apply square_of_eq,
-        refine !idp_con ⬝ !con_inv_cancel_right⁻¹ }},
+        refine !idp_con ⬝ !con_inv_cancel_right⁻¹ },
+      { apply eq_pathover,
+        refine ap_compose (smash_pmap_counit B C') _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹,
+        refine ap02 _ !functor_gluer ⬝ph _ ⬝hp ap02 _ !elim_gluer⁻¹,
+        refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _⁻¹ʰ,
+        apply square_of_eq_bot, refine !idp_con ⬝ _,
+        induction C' with C' c₀', induction g with g g₀, esimp at *,
+        induction g₀, refine ap02 _ !eq_of_phomotopy_refl }},
     { refine !idp_con ⬝ !idp_con ⬝ _, refine _ ⬝ !ap_compose',
       refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, refine !idp_con⁻¹ }
   end
 
-  definition smash_pmap_counit_natural_left (g : A →* A') :
+  definition smash_pmap_counit_natural_left (g : B →* B') :
-    smash_pmap_counit A' B ∘* g ∧→ (pid (ppmap A' B)) ~*
+    psquare (pid (ppmap B' C) ∧→ g) (smash_pmap_counit B C)
-    smash_pmap_counit A B ∘* (pid A) ∧→ (ppcompose_right g) :=
+            (ppcompose_right g ∧→ pid B) (smash_pmap_counit B' C) :=
   begin
     fapply phomotopy.mk,
     { intro af, induction af with a f a f,
@@ -157,23 +157,23 @@ namespace smash
       { reflexivity },
       { reflexivity },
       { apply eq_pathover, apply hdeg_square,
-        refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ (!elim_gluel ⬝ !idp_con) ⬝
+        refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluel ⬝ !ap_con ⬝
-          !elim_gluel ⬝ _,
+          !ap_compose'⁻¹ ◾ !elim_gluel ⬝ _,
         refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluel ⬝ !ap_con ⬝
-          !ap_compose'⁻¹ ◾ !elim_gluel ⬝ !con_idp ⬝ _)⁻¹,
+          !ap_compose'⁻¹ ◾ !elim_gluel ⬝ !idp_con)⁻¹ },
-        refine !to_fun_eq_of_phomotopy ⬝ _, reflexivity },
       { apply eq_pathover, apply hdeg_square,
-        refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝
+        refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ (!elim_gluer ⬝ !idp_con) ⬝
-          !ap_compose'⁻¹ ◾ !elim_gluer ⬝ _,
+          !elim_gluer ⬝ _,
         refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝
-          !ap_compose'⁻¹ ◾ !elim_gluer ⬝ !idp_con)⁻¹ }},
+          !ap_compose'⁻¹ ◾ !elim_gluer ⬝ !con_idp ⬝ _)⁻¹,
+        refine !to_fun_eq_of_phomotopy ⬝ _, reflexivity }},
     { refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _ ⬝ !ap_ap011⁻¹, esimp,
-      refine !to_fun_eq_of_phomotopy ⬝ _, exact !ap_constant⁻¹, }
+      refine !to_fun_eq_of_phomotopy ⬝ _, exact !ap_constant⁻¹ }
   end
 
   /- The unit-counit laws -/
   definition smash_pmap_unit_counit (A B : Type*) :
-    smash_pmap_counit A (A ∧ B) ∘* smash_functor (pid A) (smash_pmap_unit A B) ~* pid (A ∧ B) :=
+    smash_pmap_counit B (A ∧ B) ∘* smash_pmap_unit A B ∧→ pid B ~* pid (A ∧ B) :=
   begin
     fapply phomotopy.mk,
     { intro x,
@@ -184,27 +184,27 @@ namespace smash
       { apply eq_pathover_id_right,
         refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ph _,
         refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _,
-        refine !ap_eq_of_phomotopy ⬝ph _,
+        refine !idp_con ⬝ph _,
         apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ },
       { apply eq_pathover_id_right,
         refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ph _,
         refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _,
-        refine !idp_con ⬝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 (gluer pt))⁻¹ }
+         rexact (con.right_inv (gluel pt))⁻¹ }
   end
 
   definition smash_pmap_counit_unit_pt [constructor] (f : A →* B) :
-    smash_pmap_counit A B ∘* pinl A f ~* f :=
+    smash_pmap_counit A B ∘* pinr A f ~* f :=
   begin
     fapply phomotopy.mk,
     { intro a, reflexivity },
-    { refine !idp_con ⬝ !elim_gluer'⁻¹ }
+    { refine !idp_con ⬝ !elim_gluel'⁻¹ }
   end
 
   definition smash_pmap_counit_unit (A B : Type*) :
-    ppcompose_left (smash_pmap_counit A B) ∘* smash_pmap_unit A (ppmap A B) ~* pid (ppmap A B) :=
+    ppcompose_left (smash_pmap_counit A B) ∘* smash_pmap_unit (ppmap A B) A ~* pid (ppmap A B) :=
   begin
     fapply phomotopy_mk_ppmap,
     { intro f, exact smash_pmap_counit_unit_pt f },
@@ -214,9 +214,9 @@ namespace smash
       refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ ◾** !phomotopy_of_eq_of_phomotopy⁻¹,
       refine _ ⬝ !trans_refl⁻¹,
       fapply phomotopy_eq,
-      { intro a, esimp, refine !elim_gluel'⁻¹ },
+      { intro a, esimp, refine !elim_gluer'⁻¹ },
       { esimp, refine whisker_right _ !whisker_right_idp ⬝ _ ⬝ !idp_con⁻¹,
-        refine whisker_right _ !elim_gluel'_same⁻² ⬝ _ ⬝ !elim_gluer'_same⁻¹⁻²,
+        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 ⬝ _,
@@ -224,10 +224,10 @@ namespace smash
   end
 
   /- The underlying (unpointed) functions of the equivalence A →* (B →* C) ≃* A ∧ B →* C) -/
-  definition smash_elim [constructor] (f : A →* ppmap B C) : B ∧ A →* C :=
+  definition smash_elim [constructor] (f : A →* ppmap B C) : A ∧ B →* C :=
-  smash_pmap_counit B C ∘* smash_functor (pid B) f
+  smash_pmap_counit B C ∘* f ∧→ pid B
 
-  definition smash_elim_inv [constructor] (g : A ∧ B →* C) : B →* ppmap A C :=
+  definition smash_elim_inv [constructor] (g : A ∧ B →* C) : A →* ppmap B C :=
   ppcompose_left g ∘* smash_pmap_unit A B
 
   /- They are inverses, constant on the constant function and natural -/
@@ -235,7 +235,7 @@ namespace smash
   begin
     refine !pwhisker_right !ppcompose_left_pcompose ⬝* _,
     refine !passoc ⬝* _,
-    refine !pwhisker_left !smash_pmap_unit_natural⁻¹* ⬝* _,
+    refine !pwhisker_left !smash_pmap_unit_natural ⬝* _,
     refine !passoc⁻¹* ⬝* _,
     refine !pwhisker_right !smash_pmap_counit_unit ⬝* _,
     apply pid_pcompose
@@ -243,7 +243,7 @@ namespace smash
 
   definition smash_elim_right_inv (g : A ∧ B →* C) : smash_elim (smash_elim_inv g) ~* g :=
   begin
-    refine !pwhisker_left !smash_functor_pid_pcompose ⬝* _,
+    refine !pwhisker_left !smash_functor_pcompose_pid ⬝* _,
     refine !passoc⁻¹* ⬝* _,
     refine !pwhisker_right !smash_pmap_counit_natural_right⁻¹* ⬝* _,
     refine !passoc ⬝* _,
@@ -252,13 +252,13 @@ namespace smash
   end
 
   definition smash_elim_pconst (A B C : Type*) :
-    smash_elim (pconst B (ppmap A C)) ~* pconst (A ∧ B) C :=
+    smash_elim (pconst A (ppmap B C)) ~* pconst (A ∧ B) C :=
   begin
-    refine pwhisker_left _ (smash_functor_pconst_right (pid A)) ⬝* !pcompose_pconst
+    refine pwhisker_left _ (smash_functor_pconst_left (pid B)) ⬝* !pcompose_pconst
   end
 
   definition smash_elim_inv_pconst (A B C : Type*) :
-    smash_elim_inv (pconst (A ∧ B) C) ~* pconst B (ppmap A C) :=
+    smash_elim_inv (pconst (A ∧ B) C) ~* pconst A (ppmap B C) :=
   begin
     fapply phomotopy_mk_ppmap,
     { intro f, apply pconst_pcompose },
@@ -268,10 +268,10 @@ namespace smash
       apply pconst_pcompose_phomotopy_pconst }
   end
 
-  definition smash_elim_natural_right {A B C C' : Type*} (f : C →* C')
+  definition smash_elim_natural_right (f : C →* C') (g : A →* ppmap B C) :
-    (g : B →* ppmap A C) : f ∘* smash_elim g ~* smash_elim (ppcompose_left f ∘* g) :=
+    f ∘* smash_elim g ~* smash_elim (ppcompose_left f ∘* g) :=
   begin
-    refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*,
+    refine _ ⬝* pwhisker_left _ !smash_functor_pcompose_pid⁻¹*,
     refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc,
     apply smash_pmap_counit_natural_right
   end
@@ -283,27 +283,27 @@ namespace smash
     exact !ppcompose_left_pcompose⁻¹*
   end
 
-  definition smash_elim_natural_left (f : A →* A') (g : B →* B')
+  definition smash_elim_natural_left (f : A →* A') (g : B →* B') (h : A' →* ppmap B' C) :
-    (h : B' →* ppmap A' C) : smash_elim h ∘* (f ∧→ g) ~* smash_elim (ppcompose_right f ∘* h ∘* g) :=
+    smash_elim h ∘* (f ∧→ g) ~* smash_elim (ppcompose_right g ∘* h ∘* f) :=
   begin
-    refine !smash_functor_pid_pcompose ⬝ph* _,
+    refine !smash_functor_pcompose_pid ⬝ph* _,
     refine _ ⬝v* !smash_pmap_counit_natural_left,
-    refine smash_functor_psquare (pvrefl f) !pid_pcompose⁻¹*
+    refine smash_functor_psquare !pid_pcompose⁻¹* (phrefl g)
   end
 
-  definition smash_elim_phomotopy {f f' : A →* ppmap B C}
+  definition smash_elim_phomotopy {f f' : A →* ppmap B C} (p : f ~* f') :
-    (p : f ~* f') : smash_elim f ~* smash_elim f' :=
+    smash_elim f ~* smash_elim f' :=
   begin
     apply pwhisker_left,
-    exact smash_functor_phomotopy phomotopy.rfl p
+    exact smash_functor_phomotopy p phomotopy.rfl
   end
 
-  definition smash_elim_inv_phomotopy {f f' : A ∧ B →* C}
+  definition smash_elim_inv_phomotopy {f f' : A ∧ B →* C} (p : f ~* f') :
-    (p : f ~* f') : smash_elim_inv f ~* smash_elim_inv f' :=
+    smash_elim_inv f ~* smash_elim_inv f' :=
   pwhisker_right _ (ppcompose_left_phomotopy p)
 
-  definition smash_elim_eq_of_phomotopy {f f' : A →* ppmap B C}
+  definition smash_elim_eq_of_phomotopy {f f' : A →* ppmap B C} (p : f ~* f') :
-    (p : f ~* f') : ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) :=
+    ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) :=
   begin
     induction p using phomotopy_rec_idp,
     refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
@@ -325,38 +325,46 @@ namespace smash
   end
 
   /- The pointed maps of the equivalence A →* (B →* C) ≃* A ∧ B →* C -/
-  definition smash_pelim [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (B ∧ A) C :=
+  definition smash_pelim (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (A ∧ B) C :=
-  ppcompose_left (smash_pmap_counit B C) ∘* smash_functor_right B A (ppmap B C)
+  ppcompose_left (smash_pmap_counit B C) ∘* smash_functor_left A (ppmap B C) B
 
-  definition smash_pelim_inv [constructor] (A B C : Type*) :
+  definition smash_pelim_inv (A B C : Type*) :
-    ppmap (B ∧ A) C →* ppmap A (ppmap B C) :=
+    ppmap (A ∧ B) C →* ppmap A (ppmap B C) :=
   pmap.mk smash_elim_inv (eq_of_phomotopy !smash_elim_inv_pconst)
 
   /- The forward function is natural in all three arguments -/
+  definition smash_pelim_natural_left (B C : Type*) (f : A' →* A) :
+    psquare (smash_pelim A B C) (smash_pelim A' B C)
+            (ppcompose_right f) (ppcompose_right (f ∧→ pid B)) :=
+  smash_functor_left_natural_left f ⬝h* !ppcompose_left_ppcompose_right
+
+  definition smash_pelim_natural_middle (A C : Type*) (f : B' →* B) :
+    psquare (smash_pelim A B C) (smash_pelim A B' C)
+            (ppcompose_left (ppcompose_right f)) (ppcompose_right (pid A ∧→ f)) :=
+  pwhisker_tl _ !ppcompose_left_ppcompose_right ⬝*
+  (!smash_functor_left_natural_right⁻¹* ⬝pv*
+  smash_functor_left_natural_middle (ppcompose_right f) ⬝h*
+  ppcompose_left_psquare !smash_pmap_counit_natural_left)
+
   definition smash_pelim_natural_right (f : C →* C') :
     psquare (smash_pelim A B C) (smash_pelim A B C')
             (ppcompose_left (ppcompose_left f)) (ppcompose_left f) :=
-  smash_functor_right_natural_right (ppcompose_left f) ⬝h*
+  smash_functor_left_natural_middle (ppcompose_left f) ⬝h*
-  ppcompose_left_psquare (smash_pmap_counit_natural_right f)
+  ppcompose_left_psquare (smash_pmap_counit_natural_right _ f)
-
-  definition smash_pelim_natural_left (B C : Type*) (f : A' →* A) :
-    psquare (smash_pelim A B C) (smash_pelim A' B C)
-            (ppcompose_right f) (ppcompose_right (pid B ∧→ f)) :=
-  smash_functor_right_natural_middle f ⬝h* !ppcompose_left_ppcompose_right
-
-  definition smash_pelim_natural_middle (A C : Type*) (g : B' →* B) :
-    psquare (smash_pelim A B C) (smash_pelim A B' C)
-            (ppcompose_left (ppcompose_right g)) (ppcompose_right (g ∧→ pid A)) :=
-  pwhisker_tl _ !ppcompose_left_ppcompose_right ⬝*
-  (!smash_functor_right_natural_left⁻¹* ⬝pv*
-  smash_functor_right_natural_right (ppcompose_right g) ⬝h*
-  ppcompose_left_psquare !smash_pmap_counit_natural_left)
 
   definition smash_pelim_natural_lm (C : Type*) (f : A' →* A) (g : B' →* B) :
     psquare (smash_pelim A B C) (smash_pelim A' B' C)
-            (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (g ∧→ f)) :=
+            (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (f ∧→ g)) :=
   smash_pelim_natural_left B C f ⬝v* smash_pelim_natural_middle A' C g ⬝hp*
-  ppcompose_right_phomotopy proof !smash_functor_split qed ⬝* !ppcompose_right_pcompose
+  ppcompose_right_phomotopy (smash_functor_split f g) ⬝* !ppcompose_right_pcompose
+
+  definition smash_pelim_pid (B C : Type*) :
+    smash_pelim (ppmap B C) B C !pid ~* smash_pmap_counit B C :=
+  pwhisker_left _ !smash_functor_pid ⬝* !pcompose_pid
+
+  definition smash_pelim_inv_pid (A B : Type*) :
+    smash_pelim_inv A B (A ∧ B) !pid ~* smash_pmap_unit A B :=
+  pwhisker_right _ !ppcompose_left_pid ⬝* !pid_pcompose
 
   /- The equivalence (note: the forward function of smash_adjoint_pmap is smash_pelim_inv) -/
   definition is_equiv_smash_elim [constructor] (A B C : Type*) : is_equiv (@smash_elim A B C) :=
@@ -368,29 +376,22 @@ namespace smash
   end
 
   definition smash_adjoint_pmap_inv [constructor] (A B C : Type*) :
-    ppmap B (ppmap A C) ≃* ppmap (A ∧ B) C :=
+    ppmap A (ppmap B C) ≃* ppmap (A ∧ B) C :=
-  pequiv_of_pmap (smash_pelim B A C) (is_equiv_smash_elim B A C)
+  pequiv_of_pmap (smash_pelim A B C) (is_equiv_smash_elim A B C)
 
   definition smash_adjoint_pmap [constructor] (A B C : Type*) :
-    ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) :=
+    ppmap (A ∧ B) C ≃* ppmap A (ppmap B C) :=
   (smash_adjoint_pmap_inv A B C)⁻¹ᵉ*
 
   /- The naturality of the equivalence is a direct consequence of the earlier naturalities -/
   definition smash_adjoint_pmap_natural_right_pt {A B C C' : Type*} (f : C →* C') (g : A ∧ B →* C) :
     ppcompose_left f ∘* smash_adjoint_pmap A B C g ~* smash_adjoint_pmap A B C' (f ∘* g) :=
-  begin
+  smash_elim_inv_natural_right f g
-    refine !passoc⁻¹* ⬝* pwhisker_right _ _,
-    exact !ppcompose_left_pcompose⁻¹*
-  end
 
   definition smash_adjoint_pmap_inv_natural_right_pt {A B C C' : Type*} (f : C →* C')
-    (g : B →* ppmap A C) : f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* g ~*
+    (g : A →* ppmap B C) : f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* g ~*
     (smash_adjoint_pmap A B C')⁻¹ᵉ* (ppcompose_left f ∘* g) :=
-  begin
+  smash_elim_natural_right f g
-    refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*,
-    refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc,
-    apply smash_pmap_counit_natural_right
-  end
 
    definition smash_adjoint_pmap_inv_natural_right [constructor] {A B C C' : Type*} (f : C →* C') :
     ppcompose_left f ∘* smash_adjoint_pmap_inv A B C ~*
@@ -404,161 +405,244 @@ namespace smash
 
   definition smash_adjoint_pmap_natural_lm (C : Type*) (f : A →* A') (g : B →* B') :
     psquare (smash_adjoint_pmap A' B' C) (smash_adjoint_pmap A B C)
-            (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right f) ∘* ppcompose_right g) :=
+            (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) :=
-  proof (!smash_pelim_natural_lm)⁻¹ʰ* qed
+  (smash_pelim_natural_lm C f g)⁻¹ʰ*
+
+  definition smash_elim_inv_natural_middle (f : B' →* B)
+    (g : A ∧ B →* C) : ppcompose_right f ∘* smash_elim_inv g ~* smash_elim_inv (g ∘* pid A ∧→ f) :=
+  !pcompose_pid⁻¹* ⬝* !passoc ⬝* phomotopy_of_eq (smash_adjoint_pmap_natural_lm C (pid A) f g)
+
+  definition smash_pmap_unit_natural_left (f : B →* B') :
+    ppcompose_left (pid A ∧→ f) ∘* smash_pmap_unit A B ~*
+    ppcompose_right f ∘* smash_pmap_unit A B' :=
+  begin
+    refine pwhisker_left _ !smash_pelim_inv_pid⁻¹* ⬝* _ ⬝* pwhisker_left _ !smash_pelim_inv_pid,
+    refine !smash_elim_inv_natural_right ⬝* _ ⬝* !smash_elim_inv_natural_middle⁻¹*,
+    refine pap smash_elim_inv (!pcompose_pid ⬝* !pid_pcompose⁻¹*),
+  end
 
   /- Corollary: associativity of smash -/
 
-  definition smash_assoc_elim_equiv (A B C X : Type*) :
+  definition smash_assoc_elim_pequiv (A B C X : Type*) :
     ppmap (A ∧ (B ∧ C)) X ≃* ppmap ((A ∧ B) ∧ C) X :=
   calc
-    ppmap (A ∧ (B ∧ C)) X ≃* ppmap (B ∧ C) (ppmap A X) : smash_adjoint_pmap A (B ∧ C) X
+    ppmap (A ∧ (B ∧ C)) X
-    ... ≃* ppmap C (ppmap B (ppmap A X)) : smash_adjoint_pmap B C (ppmap A X)
+        ≃* ppmap A (ppmap (B ∧ C) X)     : smash_adjoint_pmap A (B ∧ C) X
-    ... ≃* ppmap C (ppmap (A ∧ B) X) : pequiv_ppcompose_left (smash_adjoint_pmap_inv A B X)
+    ... ≃* ppmap A (ppmap B (ppmap C X)) : pequiv_ppcompose_left (smash_adjoint_pmap B C X)
-    ... ≃* ppmap ((A ∧ B) ∧ C) X : smash_adjoint_pmap_inv (A ∧ B) C X
+    ... ≃* ppmap (A ∧ B) (ppmap C X)     : smash_adjoint_pmap_inv A B (ppmap C X)
+    ... ≃* ppmap ((A ∧ B) ∧ C) X         : smash_adjoint_pmap_inv (A ∧ B) C X
 
-  definition smash_assoc_elim_equiv_fn (A B C X : Type*) (f : A ∧ (B ∧ C) →* X) :
+  -- definition smash_assoc_elim_pequiv_fn (A B C X : Type*) (f : A ∧ (B ∧ C) →* X) :
-    (A ∧ B) ∧ C →* X :=
+  --   (A ∧ B) ∧ C →* X :=
-  smash_elim (ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ* (smash_elim_inv (smash_elim_inv f)))
+  -- smash_elim (ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ* (smash_elim_inv (smash_elim_inv f)))
 
-  definition smash_assoc_elim_natural_right (A B C : Type*) (f : X →* X') :
-    psquare (smash_assoc_elim_equiv A B C X) (smash_assoc_elim_equiv A B C X')
-            (ppcompose_left f) (ppcompose_left f) :=
-  !smash_adjoint_pmap_natural_right ⬝h*
-  !smash_adjoint_pmap_natural_right ⬝h*
-  ppcompose_left_psquare !smash_adjoint_pmap_inv_natural_right ⬝h*
-  !smash_adjoint_pmap_inv_natural_right
-
-  /-
-    We could prove the following two pointed homotopies by applying smash_assoc_elim_natural_right
-    to g, but we give a more explicit proof
-  -/
-  definition smash_assoc_elim_natural_right_pt {A B C X X' : Type*} (f : X →* X')
-    (g : A ∧ (B ∧ C) →* X) :
-    f ∘* smash_assoc_elim_equiv A B C X g ~* smash_assoc_elim_equiv A B C X' (f ∘* g) :=
-  begin
-    refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _,
-    apply smash_elim_phomotopy,
-    refine !passoc⁻¹* ⬝* _,
-    refine pwhisker_right _ !smash_adjoint_pmap_inv_natural_right ⬝* _,
-    refine !passoc ⬝* _,
-    apply pwhisker_left,
-    refine !smash_adjoint_pmap_natural_right_pt ⬝* _,
-    apply smash_elim_inv_phomotopy,
-    refine !smash_adjoint_pmap_natural_right_pt
-  end
-
-  definition smash_assoc_elim_inv_natural_right_pt {A B C X X' : Type*} (f : X →* X')
-    (g : (A ∧ B) ∧ C →* X) :
-    f ∘* (smash_assoc_elim_equiv A B C X)⁻¹ᵉ* g ~* (smash_assoc_elim_equiv A B C X')⁻¹ᵉ* (f ∘* g) :=
-  begin
-    refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _,
-    apply smash_elim_phomotopy,
-    refine !passoc⁻¹* ⬝* _,
-    refine pwhisker_right _ !smash_pmap_counit_natural_right ⬝* _,
-    refine !passoc ⬝* _,
-    apply pwhisker_left,
-    refine !smash_functor_pid_pcompose⁻¹* ⬝* _,
-    apply smash_functor_phomotopy phomotopy.rfl,
-    refine !passoc⁻¹* ⬝* _,
-    refine pwhisker_right _ (smash_adjoint_pmap_natural_right f) ⬝* _,
-    refine !passoc ⬝* _,
-    apply pwhisker_left,
-    apply smash_elim_inv_natural_right
-  end
-
-  definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C :=
-  begin
-    fapply pequiv.MK,
-    { exact !smash_assoc_elim_equiv⁻¹ᵉ* !pid },
-    { exact !smash_assoc_elim_equiv !pid },
-    { refine !smash_assoc_elim_inv_natural_right_pt ⬝* _,
-      refine pap !smash_assoc_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _,
-      apply phomotopy_of_eq, apply to_left_inv !smash_assoc_elim_equiv },
-    { refine !smash_assoc_elim_natural_right_pt ⬝* _,
-      refine pap !smash_assoc_elim_equiv !pcompose_pid ⬝* _,
-      apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_equiv }
-  end
-
-  /- the associativity of smash is natural in all arguments -/
   definition smash_assoc_elim_natural_left (X : Type*)
-    (f : A →* A') (g : B →* B') (h : C →* C') :
+    (f : A' →* A) (g : B' →* B) (h : C' →* C) :
-    psquare (smash_assoc_elim_equiv A' B' C' X) (smash_assoc_elim_equiv A B C X)
+    psquare (smash_assoc_elim_pequiv A B C X) (smash_assoc_elim_pequiv A' B' C' X)
             (ppcompose_right (f ∧→ g ∧→ h)) (ppcompose_right ((f ∧→ g) ∧→ h)) :=
   begin
-    refine !smash_adjoint_pmap_natural_lm ⬝h* _ ⬝h*
+    refine !smash_adjoint_pmap_natural_lm ⬝h*
-      (!ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare !smash_pelim_natural_lm) ⬝h*
+    (!ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare !smash_adjoint_pmap_natural_lm) ⬝h*
-      !smash_pelim_natural_lm,
+    _ ⬝h* !smash_pelim_natural_lm,
-    refine !ppcompose_left_ppcompose_right⁻¹* ⬝ph* _,
+    refine pwhisker_right _ (ppcompose_left_phomotopy !ppcompose_left_ppcompose_right⁻¹* ⬝*
-    refine _ ⬝hp* pwhisker_right _ (ppcompose_left_phomotopy !ppcompose_left_ppcompose_right⁻¹* ⬝*
       !ppcompose_left_pcompose) ⬝* !passoc ⬝* pwhisker_left _ !ppcompose_left_ppcompose_right⁻¹* ⬝*
-      !passoc⁻¹*,
+      !passoc⁻¹* ⬝ph* _,
-    refine _ ⬝v* !smash_adjoint_pmap_natural_lm,
+    refine _ ⬝hp* !ppcompose_left_ppcompose_right⁻¹*,
-    refine !smash_adjoint_pmap_natural_right
+    refine !smash_pelim_natural_right ⬝v* !smash_pelim_natural_lm
   end
 
+  definition smash_assoc_elim_natural_right (A B C : Type*) (f : X →* X') :
+    psquare (smash_assoc_elim_pequiv A B C X) (smash_assoc_elim_pequiv A B C X')
+            (ppcompose_left f) (ppcompose_left f) :=
+  !smash_adjoint_pmap_natural_right ⬝h*
+  ppcompose_left_psquare !smash_adjoint_pmap_natural_right ⬝h*
+  !smash_adjoint_pmap_inv_natural_right ⬝h*
+  !smash_adjoint_pmap_inv_natural_right
+
+  definition smash_assoc_elim_natural_right_pt (f : X →* X') (g : A ∧ (B ∧ C) →* X) :
+    f ∘* smash_assoc_elim_pequiv A B C X g ~* smash_assoc_elim_pequiv A B C X' (f ∘* g) :=
+  phomotopy_of_eq (smash_assoc_elim_natural_right A B C f g)
+
+  definition smash_assoc_elim_inv_natural_right_pt (f : X →* X') (g : (A ∧ B) ∧ C →* X) :
+    f ∘* (smash_assoc_elim_pequiv A B C X)⁻¹ᵉ* g ~*
+    (smash_assoc_elim_pequiv A B C X')⁻¹ᵉ* (f ∘* g) :=
+  phomotopy_of_eq ((smash_assoc_elim_natural_right A B C f)⁻¹ʰ* g)
+
+  definition smash_assoc (A B C : Type*) : (A ∧ B) ∧ C ≃* A ∧ (B ∧ C) :=
+  pyoneda (smash_assoc_elim_pequiv A B C) (λX X' f, smash_assoc_elim_natural_right A B C f)
+  -- begin
+  --   fapply pequiv.MK,
+  --   { exact !smash_assoc_elim_pequiv !pid },
+  --   { exact !smash_assoc_elim_pequiv⁻¹ᵉ* !pid },
+  --   { refine !smash_assoc_elim_natural_right_pt ⬝* _,
+  --     refine pap !smash_assoc_elim_pequiv !pcompose_pid ⬝* _,
+  --     apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_pequiv },
+  --   { refine !smash_assoc_elim_inv_natural_right_pt ⬝* _,
+  --     refine pap !smash_assoc_elim_pequiv⁻¹ᵉ* !pcompose_pid ⬝* _,
+  --     apply phomotopy_of_eq, apply to_left_inv !smash_assoc_elim_pequiv }
+  -- end
+
+  definition pcompose_smash_assoc {A B C X : Type*} (f : A ∧ (B ∧ C) →* X) :
+    f ∘* smash_assoc A B C ~* smash_assoc_elim_pequiv A B C X f :=
+  smash_assoc_elim_natural_right_pt f !pid ⬝* pap !smash_assoc_elim_pequiv !pcompose_pid
+
+  definition pcompose_smash_assoc_pinv {A B C X : Type*} (f : (A ∧ B) ∧ C →* X) :
+    f ∘* (smash_assoc A B C)⁻¹ᵉ* ~* (smash_assoc_elim_pequiv A B C X)⁻¹ᵉ* f :=
+  smash_assoc_elim_inv_natural_right_pt f !pid ⬝* pap !smash_assoc_elim_pequiv⁻¹ᵉ* !pcompose_pid
+
+  /- the associativity of smash is natural in all arguments -/
   definition smash_assoc_natural (f : A →* A') (g : B →* B') (h : C →* C') :
-    psquare (smash_assoc A B C) (smash_assoc A' B' C') (f ∧→ (g ∧→ h)) ((f ∧→ g) ∧→ h) :=
+    psquare (smash_assoc A B C) (smash_assoc A' B' C') ((f ∧→ g) ∧→ h) (f ∧→ (g ∧→ h)) :=
   begin
-    refine !smash_assoc_elim_inv_natural_right_pt ⬝* _,
+    refine !pcompose_smash_assoc ⬝* _,
-    refine pap !smash_assoc_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
+    refine pap !smash_assoc_elim_pequiv !pid_pcompose⁻¹* ⬝* _,
-    rexact phomotopy_of_eq ((smash_assoc_elim_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
+    rexact phomotopy_of_eq (smash_assoc_elim_natural_left _ f g h !pid)⁻¹
+  end
+
+  /- we prove the pentagon for the associativity -/
+  definition smash_assoc_elim_left_pequiv (A B C D X : Type*) :
+    ppmap (D ∧ (A ∧ (B ∧ C))) X ≃* ppmap (D ∧ ((A ∧ B) ∧ C)) X :=
+  calc     ppmap (D ∧ (A ∧ (B ∧ C))) X
+        ≃* ppmap D (ppmap (A ∧ (B ∧ C)) X) : smash_adjoint_pmap D (A ∧ (B ∧ C)) X
+    ... ≃* ppmap D (ppmap ((A ∧ B) ∧ C) X) : pequiv_ppcompose_left (smash_assoc_elim_pequiv A B C X)
+    ... ≃* ppmap (D ∧ ((A ∧ B) ∧ C)) X     : smash_adjoint_pmap_inv D ((A ∧ B) ∧ C) X
+
+  definition smash_assoc_elim_right_pequiv (A B C D X : Type*) :
+    ppmap ((A ∧ (B ∧ C)) ∧ D) X ≃* ppmap (((A ∧ B) ∧ C) ∧ D) X :=
+  calc     ppmap ((A ∧ (B ∧ C)) ∧ D) X
+        ≃* ppmap (A ∧ (B ∧ C)) (ppmap D X) : smash_adjoint_pmap (A ∧ (B ∧ C)) D X
+    ... ≃* ppmap ((A ∧ B) ∧ C) (ppmap D X) : smash_assoc_elim_pequiv A B C (ppmap D X)
+    ... ≃* ppmap (((A ∧ B) ∧ C) ∧ D) X     : smash_adjoint_pmap_inv ((A ∧ B) ∧ C) D X
+
+  definition smash_assoc_elim_right_natural_right (A B C D : Type*) (f : X →* X') :
+    psquare (smash_assoc_elim_right_pequiv A B C D X) (smash_assoc_elim_right_pequiv A B C D X')
+            (ppcompose_left f) (ppcompose_left f) :=
+  smash_adjoint_pmap_natural_right f ⬝h*
+  smash_assoc_elim_natural_right A B C (ppcompose_left f) ⬝h*
+  smash_adjoint_pmap_inv_natural_right f
+
+  definition smash_assoc_smash_functor (A B C D : Type*) :
+    smash_assoc A B C ∧→ pid D ~* !smash_assoc_elim_right_pequiv (pid _) :=
+  begin
+    symmetry,
+    refine pap (!smash_adjoint_pmap_inv ∘* !smash_assoc_elim_pequiv) !smash_pelim_inv_pid ⬝* _,
+    refine pap !smash_adjoint_pmap_inv !pcompose_smash_assoc⁻¹* ⬝* _,
+    refine pwhisker_left _ !smash_functor_pcompose_pid ⬝* _,
+    refine !passoc⁻¹* ⬝* _,
+    exact pwhisker_right _ !smash_pmap_unit_counit ⬝* !pid_pcompose,
+  end
+
+  definition ppcompose_right_smash_assoc (A B C X : Type*) :
+    ppcompose_right (smash_assoc A B C) ~* smash_assoc_elim_pequiv A B C X :=
+  sorry -- one hole left
+
+  definition smash_functor_smash_assoc (A B C D : Type*) :
+    pid A ∧→ smash_assoc B C D ~* !smash_assoc_elim_left_pequiv (pid _) :=
+  begin
+    symmetry,
+    refine pap (!smash_adjoint_pmap_inv ∘* ppcompose_left _) !smash_pelim_inv_pid ⬝* _,
+    refine pap !smash_adjoint_pmap_inv (pwhisker_right _ !ppcompose_right_smash_assoc⁻¹* ⬝*
+      !smash_pmap_unit_natural_left⁻¹*) ⬝* _,
+    refine phomotopy_of_eq (smash_adjoint_pmap_inv_natural_right (pid A ∧→ smash_assoc B C D)
+      !smash_pmap_unit)⁻¹ ⬝* _,
+    refine pwhisker_left _ _ ⬝* !pcompose_pid,
+    apply smash_pmap_unit_counit
+  end
+
+  definition smash_assoc_pentagon (A B C D : Type*) :
+    smash_assoc A B (C ∧ D) ∘* smash_assoc (A ∧ B) C D ~*
+    pid A ∧→ smash_assoc B C D ∘* smash_assoc A (B ∧ C) D ∘* smash_assoc A B C ∧→ pid D :=
+  begin
+    refine !pcompose_smash_assoc ⬝* _,
+    refine pap (!smash_adjoint_pmap_inv ∘* !smash_adjoint_pmap_inv ∘*
+      ppcompose_left !smash_adjoint_pmap)
+      (phomotopy_of_eq (to_left_inv !smash_adjoint_pmap_inv _)) ⬝* _,
+    refine pap (!smash_adjoint_pmap_inv ∘* !smash_adjoint_pmap_inv)
+      (phomotopy_of_eq (!smash_pelim_natural_right _)) ⬝* _,
+    symmetry,
+    refine !smash_functor_smash_assoc ◾* pwhisker_left _ !smash_assoc_smash_functor ⬝* _,
+    refine !passoc⁻¹* ⬝* _,
+    refine phomotopy_of_eq (smash_assoc_elim_right_natural_right A B C D _ _) ⬝*
+           pap !smash_assoc_elim_right_pequiv (!pcompose_pid ⬝* !pcompose_smash_assoc) ⬝* _,
+    apply phomotopy_of_eq,
+    apply ap (!smash_adjoint_pmap_inv ∘ !smash_adjoint_pmap_inv ∘ !smash_adjoint_pmap_inv),
+    refine ap (ppcompose_left _ ∘ !smash_adjoint_pmap) (to_left_inv !smash_adjoint_pmap_inv _) ⬝ _,
+    refine ap (ppcompose_left _) (to_left_inv !smash_adjoint_pmap_inv _) ⬝ _,
+    refine ap (ppcompose_left _ ∘ ppcompose_left _) (to_left_inv !smash_adjoint_pmap_inv _) ⬝ _,
+    refine ap (ppcompose_left _) ((ppcompose_left_pcompose _ _ _)⁻¹ ⬝
+      ppcompose_left_phomotopy !pinv_pcompose_cancel_left _) ⬝ _,
+    refine (ppcompose_left_pcompose _ _ _)⁻¹ ⬝
+      ppcompose_left_phomotopy !pinv_pcompose_cancel_left _ ⬝ _,
+    exact ppcompose_left_pcompose _ _ _,
   end
 
   /- Corollary 2: smashing with a suspension -/
-  definition smash_susp_elim_equiv (A B X : Type*) :
+  definition smash_susp_elim_pequiv (A B X : Type*) :
-    ppmap (A ∧ susp B) X ≃* ppmap (susp (A ∧ B)) X :=
+    ppmap (⅀ A ∧ B) X ≃* ppmap (⅀ (A ∧ B)) X :=
   calc
-    ppmap (A ∧ susp B) X ≃* ppmap (susp B) (ppmap A X) : smash_adjoint_pmap A (susp B) X
+    ppmap (⅀ A ∧ B) X ≃* ppmap (⅀ A) (ppmap B X) : smash_adjoint_pmap (⅀ A) B X
-    ... ≃* ppmap B (Ω (ppmap A X)) : susp_adjoint_loop B (ppmap A X)
+    ... ≃* ppmap A (Ω (ppmap B X)) : susp_adjoint_loop A (ppmap B X)
-    ... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_ppmap_commute A X)
+    ... ≃* ppmap A (ppmap B (Ω X)) : pequiv_ppcompose_left (loop_ppmap_commute B X)
     ... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X)
-    ... ≃* ppmap (susp (A ∧ B)) X : susp_adjoint_loop (A ∧ B) X
+    ... ≃* ppmap (⅀ (A ∧ B)) X : susp_adjoint_loop (A ∧ B) X
 
   definition smash_susp_elim_natural_right (A B : Type*) (f : X →* X') :
-    psquare (smash_susp_elim_equiv A B X) (smash_susp_elim_equiv A B X')
+    psquare (smash_susp_elim_pequiv A B X) (smash_susp_elim_pequiv A B X')
             (ppcompose_left f) (ppcompose_left f) :=
   smash_adjoint_pmap_natural_right f ⬝h*
   susp_adjoint_loop_natural_right (ppcompose_left f) ⬝h*
-  ppcompose_left_psquare (loop_pmap_commute_natural_right A f) ⬝h*
+  ppcompose_left_psquare (loop_pmap_commute_natural_right B f) ⬝h*
   (smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h*
   (susp_adjoint_loop_natural_right f)⁻¹ʰ*
 
   definition smash_susp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) :
-    psquare (smash_susp_elim_equiv A B X) (smash_susp_elim_equiv A' B' X)
+    psquare (smash_susp_elim_pequiv A B X) (smash_susp_elim_pequiv A' B' X)
-            (ppcompose_right (f ∧→ susp_functor g)) (ppcompose_right (susp_functor (f ∧→ g))) :=
+            (ppcompose_right (⅀→ f ∧→ g)) (ppcompose_right (susp_functor (f ∧→ g))) :=
   begin
-    refine smash_adjoint_pmap_natural_lm X f (susp_functor g) ⬝h*
+    refine smash_adjoint_pmap_natural_lm X (⅀→ f) g ⬝h*
            _ ⬝h* _ ⬝h*
            (smash_adjoint_pmap_natural_lm (Ω X) f g)⁻¹ʰ* ⬝h*
            (susp_adjoint_loop_natural_left (f ∧→ g))⁻¹ʰ*,
     rotate 2,
-    exact !ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare (loop_pmap_commute_natural_left X f),
+    exact !ppcompose_left_ppcompose_right ⬝v*
-    exact susp_adjoint_loop_natural_left g ⬝v* susp_adjoint_loop_natural_right (ppcompose_right f)
+      ppcompose_left_psquare (loop_pmap_commute_natural_left X g),
+    exact susp_adjoint_loop_natural_left f ⬝v* susp_adjoint_loop_natural_right (ppcompose_right g)
   end
 
-  definition smash_susp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) :=
+  definition susp_smash_rev (A B : Type*) : ⅀ (A ∧ B) ≃* ⅀ A ∧ B :=
+  pyoneda (smash_susp_elim_pequiv A B) (λX X' f, smash_susp_elim_natural_right A B f)
+  -- begin
+  --   fapply pequiv.MK,
+  --   { exact !smash_susp_elim_pequiv⁻¹ᵉ* !pid },
+  --   { exact !smash_susp_elim_pequiv !pid },
+  --   { refine phomotopy_of_eq (!smash_susp_elim_natural_right⁻¹ʰ* _) ⬝* _,
+  --     refine pap !smash_susp_elim_pequiv⁻¹ᵉ* !pcompose_pid ⬝* _,
+  --     apply phomotopy_of_eq, apply to_left_inv !smash_susp_elim_pequiv },
+  --   { refine phomotopy_of_eq (!smash_susp_elim_natural_right _) ⬝* _,
+  --     refine pap !smash_susp_elim_pequiv !pcompose_pid ⬝* _,
+  --     apply phomotopy_of_eq, apply to_right_inv !smash_susp_elim_pequiv }
+  -- end
+
+  definition susp_smash_rev_natural (f : A →* A') (g : B →* B') :
+    psquare (susp_smash_rev A B) (susp_smash_rev A' B') (⅀→ (f ∧→ g)) (⅀→ f ∧→ g) :=
   begin
-    fapply pequiv.MK,
+    refine phomotopy_of_eq (smash_susp_elim_natural_right _ _ _ _) ⬝* _,
-    { exact !smash_susp_elim_equiv⁻¹ᵉ* !pid },
+    refine pap !smash_susp_elim_pequiv (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
-    { exact !smash_susp_elim_equiv !pid },
+    rexact phomotopy_of_eq (smash_susp_elim_natural_left _ f g !pid)⁻¹
-    { refine phomotopy_of_eq (!smash_susp_elim_natural_right⁻¹ʰ* _) ⬝* _,
-      refine pap !smash_susp_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _,
-      apply phomotopy_of_eq, apply to_left_inv !smash_susp_elim_equiv },
-    { refine phomotopy_of_eq (!smash_susp_elim_natural_right _) ⬝* _,
-      refine pap !smash_susp_elim_equiv !pcompose_pid ⬝* _,
-      apply phomotopy_of_eq, apply to_right_inv !smash_susp_elim_equiv }
   end
 
-  definition smash_susp_natural (f : A →* A') (g : B →* B') :
+  definition susp_smash (A B : Type*) : ⅀ A ∧ B ≃* ⅀ (A ∧ B) :=
-    psquare (smash_susp A B) (smash_susp A' B') (f ∧→ (susp_functor g)) (susp_functor (f ∧→ g)) :=
+  (susp_smash_rev A B)⁻¹ᵉ*
-  begin
+
-    refine phomotopy_of_eq (!smash_susp_elim_natural_right⁻¹ʰ* _) ⬝* _,
+  definition smash_susp (A B : Type*) : A ∧ ⅀ B ≃* ⅀ (A ∧ B) :=
-    refine pap !smash_susp_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
+  calc A ∧ ⅀ B
-    rexact phomotopy_of_eq ((smash_susp_elim_natural_left _ f g)⁻¹ʰ* !pid)⁻¹
+            ≃* ⅀ B ∧ A  : smash_comm A (⅀ B)
-  end
+        ... ≃* ⅀(B ∧ A) : susp_smash B A
+        ... ≃* ⅀(A ∧ B) : susp_pequiv (smash_comm B A)
+
+  definition susp_smash_move (A B : Type*) : ⅀ A ∧ B ≃* A ∧ ⅀ B :=
+  susp_smash A B ⬝e* (smash_susp A B)⁻¹ᵉ*
 
-print axioms smash_susp_natural
   definition smash_iterate_susp (n : ℕ) (A B : Type*) :
     A ∧ iterate_susp n B ≃* iterate_susp n (A ∧ B) :=
   begin
@@ -568,11 +652,11 @@ print axioms smash_susp_natural
   end
 
   definition smash_sphere (A : Type*) (n : ℕ) : A ∧ sphere n ≃* iterate_susp n A :=
-  smash_pequiv pequiv.rfl (sphere_pequiv_iterate_susp n) ⬝e*
+  pequiv.rfl ∧≃ (sphere_pequiv_iterate_susp n) ⬝e*
   smash_iterate_susp n A pbool ⬝e*
   iterate_susp_pequiv n (smash_pbool_pequiv A)
 
-  definition smash_pcircle (A : Type*) : A ∧ pcircle ≃* susp A :=
+  definition smash_pcircle (A : Type*) : A ∧ S¹* ≃* susp A :=
   smash_sphere A 1
 
   definition sphere_smash_sphere (n m : ℕ) : sphere n ∧ sphere m ≃* sphere (n+m) :=

pointed.hlean

@@ -33,6 +33,12 @@ namespace pointed
   --     apply equiv_eq_closed_right, exact !idp_con⁻¹ }
   -- end
 
+  definition ppcompose_left_pid [constructor] (A B : Type*) : ppcompose_left (pid B) ~* pid (ppmap A B) :=
+  phomotopy_mk_ppmap (λf, pid_pcompose f) (!trans_refl ⬝ !phomotopy_of_eq_of_phomotopy⁻¹)
+
+  definition ppcompose_right_pid [constructor] (A B : Type*) : ppcompose_right (pid A) ~* pid (ppmap A B) :=
+  phomotopy_mk_ppmap (λf, pcompose_pid f) (!trans_refl ⬝ !phomotopy_of_eq_of_phomotopy⁻¹)
+
   /- remove some duplicates: loop_ppmap_commute, loop_ppmap_pequiv, loop_ppmap_pequiv', pfunext -/
   definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
   (loop_ppmap_commute X Y)⁻¹ᵉ*