diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index 58659c7..67a1ad9 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -736,18 +736,18 @@ namespace smash
   end
 
   local attribute is_equiv_sum_functor [instance]
-  definition smash_pequiv_smash [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D :=
+  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_smash_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B :=
-  smash_pequiv_smash f pequiv.rfl
+  definition smash_pequiv_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B :=
+  smash_pequiv f pequiv.rfl
 
-  definition smash_pequiv_smash_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D :=
-  smash_pequiv_smash pequiv.rfl g
+  definition smash_pequiv_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D :=
+  smash_pequiv pequiv.rfl g
 
   /- A ∧ B ≃* pcofiber (pprod_of_pwedge A B) -/
 
diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean
index 1c129a0..f1330f2 100644
--- a/homotopy/smash_adjoint.hlean
+++ b/homotopy/smash_adjoint.hlean
@@ -5,8 +5,7 @@
 import .smash .susp
 
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
-     function red_susp unit sigma susp
-
+     function unit sigma susp sphere
 
 namespace smash
 
@@ -430,10 +429,11 @@ namespace smash
   !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
+    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) :
+  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 ⬝* _,
@@ -480,7 +480,7 @@ namespace smash
   end
 
   /- the associativity of smash is natural in all arguments -/
-  definition smash_assoc_elim_equiv_natural_left (X : Type*)
+  definition smash_assoc_elim_natural_left (X : Type*)
     (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)
             (ppcompose_right (f ∧→ g ∧→ h)) (ppcompose_right ((f ∧→ g) ∧→ h)) :=
@@ -501,7 +501,7 @@ namespace smash
   begin
     refine !smash_assoc_elim_inv_natural_right_pt ⬝* _,
     refine pap !smash_assoc_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
-    rexact phomotopy_of_eq ((smash_assoc_elim_equiv_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
+    rexact phomotopy_of_eq ((smash_assoc_elim_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
   end
 
   /- Corollary 2: smashing with a suspension -/
@@ -514,13 +514,7 @@ namespace smash
     ... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X)
     ... ≃* ppmap (psusp (A ∧ B)) X : psusp_adjoint_loop' (A ∧ B) X
 
-  definition loop_pmap_commute_natural_right (A : Type*) (f : X →* X') :
-    psquare (loop_pmap_commute A X) (loop_pmap_commute A X')
-            (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) :=
-  sorry
-
-
-  definition smash_psusp_elim_equiv_natural_right (A B : Type*) (f : X →* X') :
+  definition smash_psusp_elim_natural_right (A B : Type*) (f : X →* X') :
     psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A B X')
             (ppcompose_left f) (ppcompose_left f) :=
   smash_adjoint_pmap_natural_right f ⬝h*
@@ -529,4 +523,56 @@ namespace smash
   (smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h*
   (psusp_adjoint_loop_natural_right f)⁻¹ʰ*
 
+  definition smash_psusp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) :
+    psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A' B' X)
+            (ppcompose_right (f ∧→ psusp_functor g)) (ppcompose_right (psusp_functor (f ∧→ g))) :=
+  begin
+    refine smash_adjoint_pmap_natural_lm X f (psusp_functor g) ⬝h*
+           _ ⬝h* _ ⬝h*
+           (smash_adjoint_pmap_natural_lm (Ω X) f g)⁻¹ʰ* ⬝h*
+           (psusp_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 psusp_adjoint_loop_natural_left g ⬝v* psusp_adjoint_loop_natural_right (ppcompose_right f)
+  end
+
+  definition smash_psusp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) :=
+  begin
+    fapply pequiv.MK2,
+    { exact !smash_psusp_elim_equiv⁻¹ᵉ* !pid },
+    { exact !smash_psusp_elim_equiv !pid },
+    { refine phomotopy_of_eq (!smash_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _,
+      refine pap !smash_psusp_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _,
+      apply phomotopy_of_eq, apply to_left_inv !smash_psusp_elim_equiv },
+    { refine phomotopy_of_eq (!smash_psusp_elim_natural_right _) ⬝* _,
+      refine pap !smash_psusp_elim_equiv !pcompose_pid ⬝* _,
+      apply phomotopy_of_eq, apply to_right_inv !smash_psusp_elim_equiv }
+  end
+
+  definition smash_psusp_natural (f : A →* A') (g : B →* B') :
+    psquare (smash_psusp A B) (smash_psusp A' B') (f ∧→ (psusp_functor g)) (psusp_functor (f ∧→ g)) :=
+  begin
+    refine phomotopy_of_eq (!smash_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _,
+    refine pap !smash_psusp_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
+    rexact phomotopy_of_eq ((smash_psusp_elim_natural_left _ f g)⁻¹ʰ* !pid)⁻¹
+  end
+
+  definition smash_iterate_psusp (n : ℕ) (A B : Type*) : A ∧ iterate_psusp n B ≃* iterate_psusp n (A ∧ B) :=
+  begin
+    induction n with n e,
+    { reflexivity },
+    { exact smash_psusp A (iterate_psusp n B) ⬝e* psusp_pequiv e }
+  end
+
+  definition smash_sphere (A : Type*) (n : ℕ) : A ∧ psphere n ≃* iterate_psusp n A :=
+  smash_pequiv pequiv.rfl (psphere_pequiv_iterate_psusp n) ⬝e*
+  smash_iterate_psusp n A pbool ⬝e*
+  iterate_psusp_pequiv n (smash_pbool_pequiv A)
+
+  definition sphere_smash_sphere (n m : ℕ) : psphere n ∧ psphere m ≃* psphere (n+m) :=
+  smash_sphere (psphere n) m ⬝e*
+  iterate_psusp_pequiv m (psphere_pequiv_iterate_psusp n) ⬝e*
+  iterate_psusp_iterate_psusp_rev m n pbool ⬝e*
+  (psphere_pequiv_iterate_psusp (n + m))⁻¹ᵉ*
+
 end smash
diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean
index 17c0da3..a481e46 100644
--- a/homotopy/susp.hlean
+++ b/homotopy/susp.hlean
@@ -134,4 +134,25 @@ namespace susp
             (ppcompose_right (psusp_functor f)) (ppcompose_right f) :=
   loop_psusp_pintro_natural_left f
 
+  definition iterate_psusp_iterate_psusp_rev (n m : ℕ) (A : Type*) :
+    iterate_psusp n (iterate_psusp m A) ≃* iterate_psusp (m + n) A :=
+  begin
+    induction n with n e,
+    { reflexivity },
+    { exact psusp_pequiv e }
+  end
+
+  definition iterate_psusp_pequiv [constructor] (n : ℕ) {X Y : Type*} (f : X ≃* Y) :
+    iterate_psusp n X ≃* iterate_psusp n Y :=
+  begin
+    induction n with n e,
+    { exact f },
+    { exact psusp_pequiv e }
+  end
+
+  open algebra nat
+  definition iterate_psusp_iterate_psusp (n m : ℕ) (A : Type*) :
+    iterate_psusp n (iterate_psusp m A) ≃* iterate_psusp (n + m) A :=
+  iterate_psusp_iterate_psusp_rev n m A ⬝e* pequiv_of_eq (ap (λk, iterate_psusp k A) (add.comm m n))
+
 end susp
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 64194ec..f33b397 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -3,7 +3,7 @@
 import homotopy.sphere2 homotopy.cofiber homotopy.wedge
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
-     is_trunc function sphere unit sum prod
+     is_trunc function sphere unit sum prod bool
 
 definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m :=
 !add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹
@@ -913,6 +913,14 @@ end category
 
 namespace sphere
 
+  definition psphere_pequiv_iterate_psusp (n : ℕ) : psphere n ≃* iterate_psusp n pbool :=
+  begin
+    induction n with n e,
+    { exact psphere_pequiv_pbool },
+    { exact psusp_pequiv e }
+  end
+
+
   -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) :
   --   f ~* pconst (S* n) (S* m) :=
   -- begin
diff --git a/pointed.hlean b/pointed.hlean
index e74b29d..33dc9c0 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -445,15 +445,15 @@ namespace pointed
   definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p
   definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p
 
-  definition phsquare.mk (p : Πx, square (p₁₀ x) (p₁₂ x) (p₀₁ x) (p₂₁ x))
-    (q : cube (square_of_eq (to_homotopy_pt p₁₀)) (square_of_eq (to_homotopy_pt p₁₂))
-              (square_of_eq (to_homotopy_pt p₀₁)) (square_of_eq (to_homotopy_pt p₂₁))
-              (p pt) ids) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ :=
-  begin
-    fapply phomotopy_eq,
-    { intro x, apply eq_of_square (p x) },
-    { generalize p pt, intro r, exact sorry }
-  end
+  -- definition phsquare.mk (p : Πx, square (p₁₀ x) (p₁₂ x) (p₀₁ x) (p₂₁ x))
+  --   (q : cube (square_of_eq (to_homotopy_pt p₁₀)) (square_of_eq (to_homotopy_pt p₁₂))
+  --             (square_of_eq (to_homotopy_pt p₀₁)) (square_of_eq (to_homotopy_pt p₂₁))
+  --             (p pt) ids) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ :=
+  -- begin
+  --   fapply phomotopy_eq,
+  --   { intro x, apply eq_of_square (p x) },
+  --   { generalize p pt, intro r, exact sorry }
+  -- end
 
 
   definition phhconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) :
@@ -596,6 +596,18 @@ namespace pointed
     exact !pwhisker_right_refl⁻¹
   end
 
+  definition phomotopy_of_eq_pcompose_left {A B C : Type*} (g : B →* C) {f f' : A →* B}
+    (p : f = f') : phomotopy_of_eq (ap (λf, g ∘* f) p) = pwhisker_left g (phomotopy_of_eq p) :=
+  begin
+    induction p, exact !pwhisker_left_refl⁻¹
+  end
+
+  definition phomotopy_of_eq_pcompose_right {A B C : Type*} {g g' : B →* C} (f : A →* B)
+    (p : g = g') : phomotopy_of_eq (ap (λg, g ∘* f) p) = pwhisker_right f (phomotopy_of_eq p) :=
+  begin
+    induction p, exact !pwhisker_right_refl⁻¹
+  end
+
   definition ap1_phomotopy_refl {X Y : Type*} (f : X →* Y) :
     ap1_phomotopy (phomotopy.refl f) = phomotopy.refl (Ω→ f) :=
   begin
@@ -878,6 +890,94 @@ namespace pointed
   definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
   (loop_pmap_commute X Y)⁻¹ᵉ*
 
+  definition loop_phomotopy [constructor] {A B : Type*} (f : A →* B) : Type* :=
+  pointed.MK (f ~* f) phomotopy.rfl
+
+  definition ppcompose_left_loop_phomotopy [constructor] {A B C : Type*} (g : B →* C) {f : A →* B}
+    {h : A →* C} (p : g ∘* f ~* h) : loop_phomotopy f →* loop_phomotopy h :=
+  pmap.mk (λq, p⁻¹* ⬝* pwhisker_left g q ⬝* p)
+    (idp ◾** !pwhisker_left_refl ◾** idp ⬝ !trans_refl ◾** idp ⬝ !trans_left_inv)
+
+  definition ppcompose_left_loop_phomotopy' [constructor] {A B C : Type*} (g : B →* C) (f : A →* B)
+    : loop_phomotopy f →* loop_phomotopy (g ∘* f) :=
+  pmap.mk (λq, pwhisker_left g q) !pwhisker_left_refl
+
+  definition ppcompose_left_loop_phomotopy_refl {A B C : Type*} (g : B →* C) (f : A →* B)
+    : ppcompose_left_loop_phomotopy g phomotopy.rfl ~* ppcompose_left_loop_phomotopy' g f :=
+  phomotopy.mk (λq, !refl_symm ◾** idp ◾** idp ⬝ !refl_trans ◾** idp ⬝ !trans_refl)
+    begin
+      esimp, exact sorry
+    end
+
+  definition loop_ppmap_pequiv' [constructor] (A B : Type*) :
+    Ω(ppmap A B) ≃* loop_phomotopy (pconst A B) :=
+  pequiv_of_equiv (pmap_eq_equiv _ _) idp
+
+  -- definition loop_ppmap (A B : Type*) : pointed.MK (pconst A B ~* pconst A B) phomotopy.rfl ≃*
+  --   pointed.MK (Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl) ⟨homotopy.rfl, idp⟩ :=
+  -- pequiv_of_equiv !phomotopy.sigma_char _
+
+  definition ppmap_loop_pequiv' [constructor] (A B : Type*) :
+    loop_phomotopy (pconst A B) ≃* ppmap A (Ω B) :=
+  pequiv_of_equiv (!phomotopy.sigma_char ⬝e !pmap.sigma_char⁻¹ᵉ) idp
+
+  definition loop_ppmap_pequiv [constructor] (A B : Type*) : Ω(ppmap A B) ≃* ppmap A (Ω B) :=
+  loop_ppmap_pequiv' A B ⬝e* ppmap_loop_pequiv' A B
+
+  definition loop_ppmap_pequiv'_natural_right' {X X' : Type} (x₀ : X) (A : Type*) (f : X → X') :
+    psquare (loop_ppmap_pequiv' A _) (loop_ppmap_pequiv' A _)
+            (Ω→ (ppcompose_left (pmap_of_map f x₀)))
+            (ppcompose_left_loop_phomotopy' (pmap_of_map f x₀) !pconst) :=
+  begin
+    fapply phomotopy.mk,
+    { esimp, esimp [pmap_eq_equiv], intro p,
+     refine _ ⬝ ap011 (λx y, phomotopy_of_eq (ap1_gen _ x y _))
+                 proof !eq_of_phomotopy_refl⁻¹ qed proof !eq_of_phomotopy_refl⁻¹ qed,
+     refine _ ⬝ ap phomotopy_of_eq !ap1_gen_idp_left⁻¹,
+     exact !phomotopy_of_eq_pcompose_left⁻¹ },
+    { refine _ ⬝ !idp_con⁻¹, exact sorry }
+  end
+
+  definition loop_ppmap_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') :
+    psquare (loop_ppmap_pequiv' A X) (loop_ppmap_pequiv' A X')
+            (Ω→ (ppcompose_left f)) (ppcompose_left_loop_phomotopy f !pcompose_pconst) :=
+  begin
+    induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀,
+    apply psquare_of_phomotopy,
+    exact sorry
+    -- fapply phomotopy.mk,
+    -- { esimp, esimp [pmap_eq_equiv], intro p, },
+    -- { }
+  end
+
+  definition ppmap_loop_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') :
+    psquare (ppmap_loop_pequiv' A X) (ppmap_loop_pequiv' A X')
+            (ppcompose_left_loop_phomotopy f !pcompose_pconst) (ppcompose_left (Ω→ f)) :=
+  begin
+    exact sorry
+  end
+
+  definition loop_pmap_commute_natural_right_direct {X X' : Type*} (A : Type*) (f : X →* X') :
+    psquare (loop_ppmap_pequiv A X) (loop_ppmap_pequiv A X')
+            (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) :=
+  begin
+    induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀,
+--    refine _ ⬝* _ ◾* _, rotate 4,
+    fapply phomotopy.mk,
+    { intro p, esimp, esimp [pmap_eq_equiv, pcompose_pconst], exact sorry },
+    { exact sorry }
+  end
+
+  definition loop_pmap_commute_natural_left {A A' : Type*} (X : Type*) (f : A' →* A) :
+    psquare (loop_pmap_commute A X) (loop_pmap_commute A' X)
+            (Ω→ (ppcompose_right f)) (ppcompose_right f) :=
+  sorry
+
+  definition loop_pmap_commute_natural_right {X X' : Type*} (A : Type*) (f : X →* X') :
+    psquare (loop_pmap_commute A X) (loop_pmap_commute A X')
+            (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) :=
+  loop_ppmap_pequiv'_natural_right A f ⬝h* ppmap_loop_pequiv'_natural_right A f
+
   /-
     Do we want to use a structure of homotopies between pointed homotopies? Or are equalities fine?
     If we set up things more generally, we could define this as
@@ -885,7 +985,8 @@ namespace pointed
   -/
   structure phomotopy2 {A B : Type*} {f g : A →* B} (p q : f ~* g) : Type :=
     (homotopy_eq : p ~ q)
-    (homotopy_pt_eq : whisker_right (respect_pt g) (homotopy_eq pt) ⬝ to_homotopy_pt q = to_homotopy_pt p)
+    (homotopy_pt_eq : whisker_right (respect_pt g) (homotopy_eq pt) ⬝ to_homotopy_pt q =
+      to_homotopy_pt p)
 
   /- this sets it up more generally, for illustrative purposes -/
   structure ppi' (A : Type*) (P : A → Type) (p : P pt) :=
@@ -894,12 +995,13 @@ namespace pointed
   attribute ppi'.to_fun [coercion]
   definition ppi_homotopy' {A : Type*} {P : A → Type} {x : P pt} (f g : ppi' A P x) : Type :=
   ppi' A (λa, f a = g a) (ppi'.resp_pt f ⬝ (ppi'.resp_pt g)⁻¹)
-  definition ppi_homotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x} (p q : ppi_homotopy' f g) : Type :=
+  definition ppi_homotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x}
+    (p q : ppi_homotopy' f g) : Type :=
   ppi_homotopy' p q
 
-  infix ` ~*2 `:50 := phomotopy2
+  -- infix ` ~*2 `:50 := phomotopy2
 
-  variables {A B : Type*} {f g : A →* B} (p q : f ~* g)
+  -- variables {A B : Type*} {f g : A →* B} (p q : f ~* g)
 
   -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q :=
   -- sorry