diff --git a/Cubical/Data/Nat/Base.agda b/Cubical/Data/Nat/Base.agda
index 87e9c4aa86..6aceb229e2 100644
--- a/Cubical/Data/Nat/Base.agda
+++ b/Cubical/Data/Nat/Base.agda
@@ -34,6 +34,11 @@ iter : ∀ {ℓ} {A : Type ℓ} → ℕ → (A → A) → A → A
 iter zero f z    = z
 iter (suc n) f z = f (iter n f z)
 
+iterswap : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (f : A → A) (z : A)
+  → iter n f (f z) ≡ f (iter n f z)
+iterswap zero f z _ = f z
+iterswap (suc n) f z i = f (iterswap n f z i)
+
 elim : ∀ {ℓ} {A : ℕ → Type ℓ}
   → A zero
   → ((n : ℕ) → A n → A (suc n))
diff --git a/Cubical/HITs/Join/CoHSpace.agda b/Cubical/HITs/Join/CoHSpace.agda
new file mode 100644
index 0000000000..8553b56ae5
--- /dev/null
+++ b/Cubical/HITs/Join/CoHSpace.agda
@@ -0,0 +1,350 @@
+{-
+This file contains a definition of the co-H-space structure on
+joins and a proof that it is equivalent to that on suspensions
+-}
+
+{-# OPTIONS --safe --lossy-unification #-}
+
+module Cubical.HITs.Join.CoHSpace where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Path
+
+open import Cubical.Data.Sigma renaming (fst to proj₁; snd to proj₂)
+open import Cubical.Data.Unit
+open import Cubical.Data.Nat
+open import Cubical.Data.Sum
+
+open import Cubical.HITs.Join
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Sn
+open import Cubical.HITs.Susp renaming (toSusp to σ)
+
+open import Cubical.HITs.SmashProduct
+open import Cubical.HITs.Pushout
+open import Cubical.Foundations.Pointed.Homogeneous
+
+open import Cubical.Homotopy.Loopspace
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+open Iso
+
+-- Standard loop in Ω (join A B)
+ℓ* : (A : Pointed ℓ) (B : Pointed ℓ')
+  → fst A → fst B → Ω (join∙ A B) .fst
+ℓ* A B a b = push (pt A) (pt B)
+           ∙ (push a (pt B) ⁻¹ ∙∙ push a b ∙∙ (push (pt A) b ⁻¹))
+
+ℓ*IdL : (A : Pointed ℓ) (B : Pointed ℓ')
+  → (b : fst B) → ℓ* A B (pt A) b ≡ refl
+ℓ*IdL A B b =
+  cong₂ _∙_ refl
+            (doubleCompPath≡compPath _ _ _
+            ∙ cong (push (pt A) (pt B) ⁻¹ ∙_) (rCancel _)
+            ∙ sym (rUnit _))
+  ∙ rCancel _
+
+ℓ*IdR : (A : Pointed ℓ) (B : Pointed ℓ')
+  → (a : typ A) → ℓ* A B a (pt B) ≡ refl
+ℓ*IdR A B a =
+    cong₂ _∙_ refl
+            (doubleCompPath≡compPath _ _ _
+            ∙ assoc _ _ _
+            ∙ cong (_∙ push (pt A) (pt B) ⁻¹) (rCancel _)
+            ∙ sym (lUnit _))
+  ∙ rCancel _
+
+-- Addition of functions join A B → C
+_+*_ : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+  (f g : join∙ A B →∙ C) → join∙ A B →∙ C
+fst (_+*_ {C = C} f g) (inl x) = pt C
+fst (_+*_ {C = C} f g) (inr x) = pt C
+fst (_+*_ {A = A} {B = B} f g) (push a b i) =
+  (Ω→ f .fst (ℓ* A B a b) ∙ Ω→ g .fst (ℓ* A B a b)) i
+snd (f +* g) = refl
+
+-- Inversion
+-* : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+     (f : join∙ A B →∙ C) → join∙ A B →∙ C
+fst (-* {C = C} f) (inl x) = pt C
+fst (-* {C = C} f) (inr x) = pt C
+fst (-* {A = A} {B} f) (push a b i) = Ω→ f .fst (ℓ* A B a b) (~ i)
+snd (-* f) = refl
+
+-- Iterated inversion
+-*^ : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+      (n : ℕ) (f : join∙ A B →∙ C)
+     → join∙ A B →∙ C
+-*^ n = iter n -*
+
+-- Neutral element
+0* : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+  → join∙ A B →∙ C
+0* = const∙ _ _
+
+-- Mapping space join∙ A B →∙ C is equivalent to Susp (A ⋀ B) →∙ C
+fromSusp≅fromJoin : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+   → Iso (Susp∙ (A ⋀ B) →∙ C) (join∙ A B →∙ C)
+fromSusp≅fromJoin {A = A} {B = B} =
+  post∘∙equiv (isoToEquiv SmashJoinIso , sym (push (pt A) (pt B)))
+
+-- Goal now: show that this is an equivalence of H-spaces
+
+-- Technical lemma
+Ω→ℓ⋀ : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+    (f : join∙ A B →∙ C)
+    (x : fst A) (y : fst B)
+  → Ω→ f .fst (ℓ* A B x y)
+   ≡ Ω→ (inv fromSusp≅fromJoin f) .fst (σ (A ⋀∙ B) (inr (x , y)))
+Ω→ℓ⋀ f x y =
+   (cong₃ _∙∙_∙∙_ (symDistr _ _)
+                  (cong-∙ (fst (inv fromSusp≅fromJoin f)) _ _ ∙ cong₂ _∙_ refl refl)
+                  refl
+  ∙ doubleCompPath≡compPath _ _ _
+  ∙ sym (assoc _ _ _)
+  ∙ cong (snd f ⁻¹ ∙_) (assoc _ _ _ ∙ assoc _ _ _)
+  ∙ sym (doubleCompPath≡compPath _ _ _)
+  ∙ cong₃ _∙∙_∙∙_
+      refl
+      (sym (assoc _ _ _)
+        ∙ cong₂ _∙_ refl
+          ((sym (assoc _ _ _) ∙ cong₂ _∙_ refl (rCancel _)) ∙ sym (rUnit _))
+        ∙ sym (cong-∙ (fst f) _ _))
+      refl) ⁻¹
+
+-- We'll show it for the inverse function
+-- Inverse function preseves neutral elements
+fromSusp≅fromJoin⁻Pres0* : (A : Pointed ℓ) (B : Pointed ℓ') {C : Pointed ℓ''}
+  → inv fromSusp≅fromJoin (const∙ (join∙ A B) C) ≡ const∙ _ _
+fromSusp≅fromJoin⁻Pres0* A B = ΣPathP (refl , (sym (rUnit refl)))
+
+-- Inverse function preseves +*
+fromSusp≅fromJoin⁻Pres+* : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+   → (f g : join∙ A B →∙ C)
+   → Iso.inv fromSusp≅fromJoin (f +* g)
+   ≡ ·Susp (A ⋀∙ B) (Iso.inv fromSusp≅fromJoin f)
+                     (Iso.inv fromSusp≅fromJoin g)
+fromSusp≅fromJoin⁻Pres+* {A = A} {B = B} f g =
+  ΣPathP ((funExt λ { north → refl
+                    ; south → refl
+                    ; (merid a i) j → main j a i})
+        , (sym (rUnit _)
+        ∙ cong sym (cong₂ _∙_ (cong (Ω→ f .fst) (ℓ*IdR A B (pt A)) ∙ Ω→ f .snd)
+                              (cong (Ω→ g .fst) (ℓ*IdR A B (pt A)) ∙ Ω→ g .snd))
+                 ∙ sym (rUnit _)))
+    where
+    main : cong (fst (f +* g) ∘ (SuspSmash→Join {A = A} {B = B})) ∘ merid
+           ≡ λ a → Ω→ (Iso.inv fromSusp≅fromJoin f) .fst (σ (A ⋀∙ B) a)
+                  ∙ Ω→ (Iso.inv fromSusp≅fromJoin g) .fst (σ (A ⋀∙ B) a)
+    main = ⋀→Homogeneous≡ (isHomogeneousPath _ _)
+           λ x y → cong-∙∙ (fst (f +* g)) _ _ _
+                  ∙ cong₃ _∙∙_∙∙_
+                    (cong sym (cong₂ _∙_ (cong (Ω→ f .fst) (ℓ*IdR A B x)
+                              ∙  Ω→ f .snd)
+                              (cong (Ω→ g .fst) (ℓ*IdR A B x)
+                              ∙  Ω→ g .snd)
+                              ∙ sym (rUnit refl)))
+                    refl
+                    (cong sym ((cong₂ _∙_ (cong (Ω→ f .fst) (ℓ*IdL A B y)
+                              ∙  Ω→ f .snd)
+                              (cong (Ω→ g .fst) (ℓ*IdL A B y)
+                              ∙  Ω→ g .snd)
+                              ∙ sym (rUnit refl))))
+                  ∙ sym (rUnit _)
+                  ∙ cong₂ _∙_ (Ω→ℓ⋀ f x y) (Ω→ℓ⋀ g x y)
+
+-- Inverse function preseves inversion
+fromSusp≅fromJoin⁻Pres-* :
+  {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+   → (f : join∙ A B →∙ C)
+   → inv fromSusp≅fromJoin (-* f)
+   ≡ -Susp (A ⋀∙ B) (inv fromSusp≅fromJoin f)
+fromSusp≅fromJoin⁻Pres-* {A = A} {B = B} {C = C} f =
+  ΣPathP ((funExt (λ { north → refl
+                     ; south → refl
+                     ; (merid a i) j → lem j a i}))
+        , sym (rUnit _)
+        ∙ (cong (Ω→ f .fst) (ℓ*IdR A B (pt A))
+         ∙ Ω→ f .snd))
+  where
+  lem : cong (fst (-* f) ∘ SuspSmash→Join) ∘ merid
+      ≡ λ a → cong (-Susp (A ⋀∙ B) (inv fromSusp≅fromJoin f) .fst) (merid a)
+  lem = ⋀→Homogeneous≡ (isHomogeneousPath _ _)
+         λ x y → cong-∙∙ (fst (-* f)) _ _ _
+               ∙∙ cong₃ _∙∙_∙∙_ ((cong (Ω→ f .fst) (ℓ*IdR A B x) ∙ Ω→ f .snd))
+                                refl
+                                (cong (Ω→ f .fst) (ℓ*IdL A B y) ∙ Ω→ f .snd)
+                ∙ cong₂ _∙_ (doubleCompPath≡compPath _ _ _
+                           ∙ (cong (sym (snd f) ∙_)
+                                   (cong (_∙ snd f)
+                               (cong sym (cong-∙ (fst f) _ _)
+                               ∙ symDistr _ _
+                               ∙ (cong₂ _∙_ (lUnit _
+                               ∙ cong₂ _∙_ (sym (rCancel _)) refl
+                                         ∙ sym (assoc _ _ _)) refl
+                               ∙ sym (assoc _ _ _))
+                               ∙ cong₂ _∙_
+                                   refl
+                                   (cong₂ _∙_ (sym (symDistr _ _)) refl)))
+                           ∙ (assoc _ _ _
+                           ∙ cong₂ _∙_ (assoc _ _ _ ∙ assoc _ _ _) refl)
+                           ∙ sym (assoc _ _ _))
+                           ∙ sym (assoc _ _ _)
+                           ∙ doubleCompPath≡compPath _ _ _ ⁻¹ --
+                           ∙ cong₃ _∙∙_∙∙_
+                             (sym (symDistr _ _))
+                              (cong sym (sym (cong-∙ (fst (inv fromSusp≅fromJoin f)) _ _)))
+                                refl)
+                  (sym ((cong (Ω→ (inv fromSusp≅fromJoin f) .fst)
+                        (rCancel (merid (inl tt))))
+                      ∙ ∙∙lCancel _))
+               ∙∙ sym (cong-∙ (-Susp (A ⋀∙ B)  (inv fromSusp≅fromJoin f) .fst) _ _)
+               ∙∙ rUnit _
+               ∙∙  Ω→-Susp _ (inv fromSusp≅fromJoin f) (inr (x , y)) --
+
+-- Same lemmas again, this time the other direction
+fromSusp≅fromJoinPres+* :
+  {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+   → (f g : Susp∙ (A ⋀ B) →∙ C)
+   → Iso.fun fromSusp≅fromJoin (·Susp (A ⋀∙ B) f g)
+   ≡ (Iso.fun fromSusp≅fromJoin f) +* (Iso.fun fromSusp≅fromJoin g)
+fromSusp≅fromJoinPres+* {A = A} {B = B} f g =
+  cong (fun fromSusp≅fromJoin)
+       (cong₂ (·Susp (A ⋀∙ B))
+              (sym (leftInv fromSusp≅fromJoin f))
+              (sym (leftInv fromSusp≅fromJoin g)))
+  ∙∙ sym (cong (fun fromSusp≅fromJoin)
+               (fromSusp≅fromJoin⁻Pres+*
+                 (fun fromSusp≅fromJoin f)
+                 (fun fromSusp≅fromJoin g)))
+  ∙∙ rightInv fromSusp≅fromJoin _
+
+fromSusp≅fromJoinPres-* :
+  {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+   → (f : Susp∙ (A ⋀ B) →∙ C)
+   → fun fromSusp≅fromJoin (-Susp (A ⋀∙ B) f)
+   ≡ -* (fun fromSusp≅fromJoin f)
+fromSusp≅fromJoinPres-* {A = A} {B = B} f  =
+    cong (fun fromSusp≅fromJoin ∘ -Susp (A ⋀∙ B))
+         (sym (leftInv fromSusp≅fromJoin f))
+  ∙ sym (cong (fun fromSusp≅fromJoin)
+           (fromSusp≅fromJoin⁻Pres-* (fun fromSusp≅fromJoin f)))
+  ∙ rightInv fromSusp≅fromJoin _
+
+fromSusp≅fromJoinPres0* : (A : Pointed ℓ) (B : Pointed ℓ') {C : Pointed ℓ''}
+   → fun fromSusp≅fromJoin (const∙ (Susp∙ (A ⋀ B)) C)
+   ≡ const∙ _ _
+fromSusp≅fromJoinPres0* A B = ΣPathP (refl , (sym (rUnit refl)))
+
+
+--- We use the above to transport the HSpace proofs from suspensions to joins
+module _ {ℓ ℓ' ℓ'' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''} where
+  private
+    P = isoToPath (fromSusp≅fromJoin {A = A} {B = B} {C = C})
+    ·Susp-+*-PathP : PathP (λ i → P i → P i → P i) (·Susp (A ⋀∙ B)) _+*_
+    ·Susp-+*-PathP  =
+      toPathP (funExt λ f → funExt λ g
+      → transportRefl _
+        ∙ (cong₂ _∘∙_ (cong₂ (·Susp (A ⋀∙ B))
+                             (cong₂ _∘∙_ (transportRefl f) refl)
+                             (cong₂ _∘∙_ (transportRefl g) refl)) refl)
+        ∙ fromSusp≅fromJoinPres+* (inv fromSusp≅fromJoin f) (inv fromSusp≅fromJoin g)
+        ∙ cong₂ _+*_ (rightInv fromSusp≅fromJoin f) (rightInv fromSusp≅fromJoin g))
+
+    ·Susp--*-PathP : PathP (λ i → P i → P i) (-Susp (A ⋀∙ B)) -*
+    ·Susp--*-PathP =
+      toPathP (funExt λ x → transportRefl _
+        ∙ cong₂ _∘∙_ (cong (-Susp (A ⋀∙ B)) (cong₂ _∘∙_ (transportRefl _) refl)) refl
+        ∙ fromSusp≅fromJoinPres-* (inv fromSusp≅fromJoin x)
+        ∙ cong -* (rightInv fromSusp≅fromJoin x))
+
+    ·Susp-0*-PathP : PathP (λ i → P i) (const∙ _ _) (const∙ _ _)
+    ·Susp-0*-PathP = symP (toPathP (cong₂ _∘∙_ (transportRefl _) refl
+                          ∙ ΣPathP (refl , (sym (rUnit _)))))
+
+  -- The laws
+  +*HSpace : Σ[ r ∈ ((f : join∙ A B →∙ C) → (f +* 0*) ≡ f) ]
+             Σ[ l ∈ ((f : join∙ A B →∙ C) → (0* +* f) ≡ f) ]
+             r 0* ≡ l 0*
+  +*HSpace =
+    transport (λ i
+      →  Σ[ r ∈ ((f : P i) → ·Susp-+*-PathP i f (·Susp-0*-PathP i) ≡ f) ]
+          Σ[ l ∈ ((f : P i) → ·Susp-+*-PathP i (·Susp-0*-PathP i) f ≡ f) ]
+           r (·Susp-0*-PathP i) ≡ l (·Susp-0*-PathP i))
+      ((·SuspIdR _) , (·SuspIdL _) , (sym (·SuspIdL≡·SuspIdR _)))
+
+  +*IdR : (f : join∙ A B →∙ C) → (f +* 0*) ≡ f
+  +*IdR = +*HSpace .fst
+
+  +*IdL : (f : join∙ A B →∙ C) → (0* +* f) ≡ f
+  +*IdL = +*HSpace .snd .fst
+
+  +*InvR : (f : join∙ A B →∙ C) → (f +* (-* f)) ≡ 0*
+  +*InvR = transport (λ i → (f : P i) → ·Susp-+*-PathP i f (·Susp--*-PathP i f)
+                                       ≡ ·Susp-0*-PathP i)
+                     (·SuspInvR _)
+
+  +*InvL : (f : join∙ A B →∙ C) → ((-* f) +* f) ≡ 0*
+  +*InvL = transport (λ i → (f : P i) → ·Susp-+*-PathP i (·Susp--*-PathP i f) f
+                                        ≡ ·Susp-0*-PathP i)
+                     (·SuspInvL _)
+
+  +*Assoc : (f g h : join∙ A B →∙ C) → (f +* (g +* h)) ≡ ((f +* g) +* h)
+  +*Assoc =
+    transport (λ i → (f g h : P i)
+                    → ·Susp-+*-PathP i f (·Susp-+*-PathP i g h)
+                    ≡ ·Susp-+*-PathP i (·Susp-+*-PathP i f g) h)
+              (·SuspAssoc _)
+
+  +*Comm : (Σ[ A' ∈ Pointed ℓ ] A ≃∙ Susp∙ (fst A'))
+         ⊎ (Σ[ B' ∈ Pointed ℓ' ] B ≃∙ Susp∙ (fst B'))
+    → (f g : join∙ A B →∙ C) → (f +* g) ≡ (g +* f)
+  +*Comm (inl (A' , e)) =
+    transport (λ i → (f g : P i)
+                   → ·Susp-+*-PathP i f g
+                    ≡ ·Susp-+*-PathP i g f)
+             (·SuspComm' _ (A' ⋀∙ B)
+                           (compEquiv∙ (⋀≃ e (idEquiv∙ B) , refl)
+                           (isoToEquiv SuspSmashCommIso , refl)))
+  +*Comm (inr (B' , e)) =
+    transport (λ i → (f g : P i)
+                   → ·Susp-+*-PathP i f g
+                    ≡ ·Susp-+*-PathP i g f)
+              (·SuspComm' _ (A ⋀∙ B')
+                (compEquiv∙
+                (compEquiv∙ (compEquiv∙ (⋀≃ (idEquiv∙ A) e , refl)
+                  (isoToEquiv ⋀CommIso , refl))
+                  (isoToEquiv SuspSmashCommIso , refl))
+                  (congSuspEquiv (isoToEquiv ⋀CommIso) , refl)))
+
+  -*² : (f : join∙ A B →∙ C) → -* (-* f) ≡ f
+  -*² f =
+    sym (+*IdR (-* (-* f)))
+    ∙ cong (-* (-* f) +*_) (sym (+*InvL f))
+    ∙ +*Assoc  _ _ _
+    ∙ cong (_+* f) ( +*InvL (-* f))
+    ∙ +*IdL f
+    where
+    help : (-* (-* f)) +* (-* f) ≡ f +* (-* f)
+    help = +*InvL (-* f) ∙ sym (+*InvR f)
+
+join-commFun-ℓ* : (A : Pointed ℓ) (B : Pointed ℓ') (a : fst A) (b : fst B)
+  → cong join-commFun (ℓ* A B a b)
+   ≡ (sym (push (pt B) (pt A)) ∙∙ sym (ℓ* B A b a) ∙∙ push (pt B) (pt A))
+join-commFun-ℓ* A B a b =
+    cong-∙ join-commFun (push (pt A) (pt B)) _
+  ∙ cong₂ _∙_ refl (cong-∙∙ join-commFun _ _ _)
+  ∙ sym (doubleCompPath≡compPath _ _ _
+      ∙ cong₂ _∙_ refl
+         (cong₂ _∙_ (symDistr _ _) refl
+        ∙ sym (assoc _ _ _) ∙ cong₂ _∙_ refl (lCancel _)
+        ∙ sym (rUnit _)))
diff --git a/Cubical/HITs/Join/Properties.agda b/Cubical/HITs/Join/Properties.agda
index ae82d7800d..dbe65e431e 100644
--- a/Cubical/HITs/Join/Properties.agda
+++ b/Cubical/HITs/Join/Properties.agda
@@ -447,6 +447,10 @@ join-commFun (inl x) = inr x
 join-commFun (inr x) = inl x
 join-commFun (push a b i) = push b a (~ i)
 
+join-commFun∙ : ∀ {ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} → join∙ A B →∙ join∙ B A
+proj₁ join-commFun∙ = join-commFun
+snd (join-commFun∙ {A = A} {B = B}) = push (pt B) (pt A) ⁻¹
+
 join-commFun² : ∀ {ℓ'} {A : Type ℓ} {B : Type ℓ'} (x : join A B)
                 → join-commFun (join-commFun x) ≡ x
 join-commFun² (inl x) = refl
@@ -703,3 +707,15 @@ module _ {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
   inv GaneaIso = join→GaneaFib
   rightInv GaneaIso = join→GaneaFib→join
   leftInv GaneaIso = GaneaFib→join→GaneaFib
+
+-- Pinch map
+joinPinch : ∀ {ℓ''} {A : Type ℓ} {B : Type ℓ'} (C : Pointed ℓ'')
+  → ((a : A) (b : B) → Ω C .fst) → join A B → fst C
+joinPinch C p (inl x) = pt C
+joinPinch C p (inr x) = pt C
+joinPinch C p (push a b i) = p a b i
+
+joinPinch∙ : ∀ {ℓ''} (A : Pointed ℓ) (B : Pointed ℓ') (C : Pointed ℓ'')
+  → ((a : typ A) (b : typ B) → Ω C .fst) → join∙ A B →∙ C
+proj₁ (joinPinch∙ A B C p) = joinPinch C p
+snd (joinPinch∙ A B C p) = refl
diff --git a/Cubical/HITs/SmashProduct/Base.agda b/Cubical/HITs/SmashProduct/Base.agda
index 2c591a2797..0793a3ce8a 100644
--- a/Cubical/HITs/SmashProduct/Base.agda
+++ b/Cubical/HITs/SmashProduct/Base.agda
@@ -200,7 +200,7 @@ prod→⋀^ zero A x = x
 prod→⋀^ (suc n) A x =
   inr ((prod→⋀^ n (predFinFamily∙ A) (fst x)) , (snd x))
 
-⋀→Homogeneous≡ : {A B : Pointed ℓ} {D : Type ℓ'}
+⋀→Homogeneous≡ : ∀ {ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {D : Type ℓ''}
   → {f g : A ⋀ B → D}
   → (isHomogeneous (D , f (inl tt)))
   → ((x : _) (y : _) → f (inr (x , y)) ≡ g (inr (x , y)))
@@ -1058,6 +1058,29 @@ module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} where
  Iso.rightInv SmashJoinIso = Join→SuspSmash→Join
  Iso.leftInv SmashJoinIso = SuspSmash→Join→SuspSmash
 
+-- Pointed versions
+Join→SuspSmash∙ : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
+  → join∙ A B →∙ Susp∙ (A ⋀ B)
+Join→SuspSmash∙ A B = Join→SuspSmash , refl
+
+SuspSmash→Join∙ : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
+  → Susp∙ (A ⋀ B) →∙ join∙ A B
+SuspSmash→Join∙ A B = SuspSmash→Join , push (pt A) (pt B) ⁻¹
+
+permute⋀JoinIso : ∀ {ℓ ℓ' ℓ''}
+  (A : Pointed ℓ) (B : Pointed ℓ') (C : Pointed ℓ'')
+  → Iso (join (A ⋀ B) (typ C)) (join (typ A) (B ⋀ C))
+permute⋀JoinIso A B C =
+  compIso (invIso (SmashJoinIso {A = A ⋀∙ B} {C}))
+   (compIso (congSuspIso (invIso SmashAssocIso))
+            (SmashJoinIso {A = A} {B ⋀∙ C}))
+
+permute⋀Join≃∙ : ∀ {ℓ ℓ' ℓ''}
+  (A : Pointed ℓ) (B : Pointed ℓ') (C : Pointed ℓ'')
+  → join∙ (A ⋀∙ B) C ≃∙ join∙ A (B ⋀∙ C)
+fst (permute⋀Join≃∙ A B C) = isoToEquiv (permute⋀JoinIso A B C)
+snd (permute⋀Join≃∙ A B C) = sym (push (pt A) (inl tt))
+
 -- Suspension commutes with smash products
 module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} where
 
diff --git a/Cubical/HITs/Sn/Multiplication.agda b/Cubical/HITs/Sn/Multiplication.agda
index 56899e9848..60f7007d1c 100644
--- a/Cubical/HITs/Sn/Multiplication.agda
+++ b/Cubical/HITs/Sn/Multiplication.agda
@@ -480,8 +480,7 @@ assoc⌣S {n = suc (suc n)} {m = m} {l} (merid a i) y z j =
 
 -- To state it: we'll need iterated negations
 -S^ : {k : ℕ} (n : ℕ) → S₊ k → S₊ k
--S^ zero x = x
--S^ (suc n) x = invSphere (-S^ n x)
+-S^ n = iter n invSphere
 
 -- The folowing is an explicit definition of -S^ (n · m) which is
 -- often easier to reason about
@@ -544,8 +543,11 @@ private
 
 -- Iterated path inversion
 sym^ : ∀ {ℓ} {A : Type ℓ} {x : A} (n : ℕ) → x ≡ x → x ≡ x
-sym^ zero p = p
-sym^ (suc n) p = sym (sym^ n p)
+sym^ n = iter n sym
+
+sym^-refl : ∀ {ℓ} {A : Type ℓ} {x : A} (n : ℕ) → sym^ {x = x} n refl ≡ refl
+sym^-refl zero = refl
+sym^-refl (suc n) = cong sym (sym^-refl n)
 
 -- Interaction between -S^ and sym^
 σS-S^ : {k : ℕ} (n : ℕ) (x : S₊ (suc k))
diff --git a/Cubical/HITs/Sn/Properties.agda b/Cubical/HITs/Sn/Properties.agda
index 91bf1fa440..6f9c89504d 100644
--- a/Cubical/HITs/Sn/Properties.agda
+++ b/Cubical/HITs/Sn/Properties.agda
@@ -23,6 +23,7 @@ open import Cubical.HITs.PropositionalTruncation as PT hiding (rec ; elim)
 open import Cubical.HITs.SmashProduct.Base
 open import Cubical.HITs.Pushout.Base
 open import Cubical.Homotopy.Connected
+open import Cubical.Homotopy.Loopspace
 open import Cubical.HITs.Join renaming (joinS¹S¹→S³ to joinS¹S¹→S3)
 open import Cubical.Data.Bool hiding (elim)
 
@@ -523,3 +524,11 @@ invSphere² (suc (suc n)) = invSusp²
                     ∙∙ (λ i → (σSn 1 (loop i)))
                     ∙∙ (rCancel (merid base))) j i)
 σ-invSphere (suc n) x = toSusp-invSusp (S₊∙ (suc n)) x
+
+-- Commutativity of ·→Ω with Sⁿ domain.
+EH-ΠΩ : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ} (f g : S₊∙ (suc n) →∙ Ω A)
+     → ·→Ω f g ≡ ·→Ω g f
+EH-ΠΩ {A = A} {n = n} =
+  subst (λ T → (f g : T →∙ Ω A) → ·→Ω f g ≡ ·→Ω g f)
+        (ua∙ (isoToEquiv (invIso (IsoSucSphereSusp n))) (IsoSucSphereSusp∙ n))
+        (Susp·→Ωcomm (S₊∙ n))
diff --git a/Cubical/HITs/Susp/Properties.agda b/Cubical/HITs/Susp/Properties.agda
index 98f7c2a2ab..2eb4919b25 100644
--- a/Cubical/HITs/Susp/Properties.agda
+++ b/Cubical/HITs/Susp/Properties.agda
@@ -380,6 +380,7 @@ toSusp-invSusp A (merid a i) j =
                 ▷ rUnit refl)))
 
 -- co-H-space structure
+
 ·Susp : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
         (f g : Susp∙ (typ A) →∙ B) → Susp∙ (typ A) →∙ B
 fst (·Susp A {B = B} f g) north = pt B
@@ -387,3 +388,221 @@ fst (·Susp A {B = B} f g) south = pt B
 fst (·Susp A {B = B} f g) (merid a i) =
   (Ω→ f .fst (toSusp A a) ∙ Ω→ g .fst (toSusp A a)) i
 snd (·Susp A f g) = refl
+
+-Susp : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+      → Susp∙ (typ A) →∙ B → Susp∙ (typ A) →∙ B
+fst (-Susp A {B = B} f) north = pt B
+fst (-Susp A {B = B} f) south = pt B
+fst (-Susp A {B = B} f) (merid a i) =
+  (Ω→ f .fst (toSusp A a) (~ i))
+snd (-Susp A f) = refl
+
+·Suspσ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (f g : Susp∙ (typ A) →∙ B)
+  → (a : typ A) → cong (·Susp A f g .fst) (toSusp A a)
+                  ≡ Ω→ f .fst (toSusp A a) ∙ Ω→ g .fst (toSusp A a)
+·Suspσ {A = A} f g a = cong-∙ (·Susp A f g .fst) (merid a) (merid (pt A) ⁻¹)
+  ∙ cong₂ _∙_ refl
+          (cong _⁻¹ (cong₂ _∙_
+                     (cong (Ω→ f .fst) (rCancel (merid (pt A))) ∙ Ω→ f .snd)
+                     (cong (Ω→ g .fst) (rCancel (merid (pt A))) ∙ Ω→ g .snd)
+                  ∙ sym (rUnit _)))
+  ∙ sym (rUnit _)
+
+·Suspσ' : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (f g : Susp∙ (typ A) →∙ B)
+  → (a : typ A) → Ω→ (·Susp A f g) .fst (toSusp A a)
+                  ≡ Ω→ f .fst (toSusp A a) ∙ Ω→ g .fst (toSusp A a)
+·Suspσ' f g a = sym (rUnit _) ∙ ·Suspσ f g a
+
+Ω→-Susp : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+        (f : Susp∙ (typ A) →∙ B)
+        (a : typ A)
+      → Ω→ (-Susp A f) .fst (toSusp A a) ≡ Ω→ f .fst (toSusp A a) ⁻¹
+Ω→-Susp A f a = sym (rUnit _)
+  ∙ cong-∙ (fst (-Susp A f)) (merid a) (merid (pt A) ⁻¹)
+  ∙ cong₂ _∙_ refl (cong (Ω→ f .fst) (rCancel (merid (pt A))) ∙ Ω→ f .snd)
+  ∙ sym (rUnit _)
+
+
+·SuspInvR : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+        (f : Susp∙ (typ A) →∙ B)
+     → ·Susp A f (-Susp A f) ≡ const∙ _ _
+fst (·SuspInvR A {B = B} f i) north = pt B
+fst (·SuspInvR A {B = B} f i) south = pt B
+fst (·SuspInvR A {B = B} f i) (merid a j) = main i j
+  where
+  main : (Ω→ f .fst (toSusp A a) ∙ Ω→ (-Susp A f) .fst (toSusp A a)) ≡ refl
+  main = cong₂ _∙_ refl (Ω→-Susp A f a) ∙ rCancel _
+snd (·SuspInvR A {B = B} f i) = refl
+
+·SuspInvL : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+        (f : Susp∙ (typ A) →∙ B)
+     → ·Susp A (-Susp A f) f ≡ const∙ _ _
+fst (·SuspInvL A {B = B} f i) north = pt B
+fst (·SuspInvL A {B = B} f i) south = pt B
+fst (·SuspInvL A {B = B} f i) (merid a j) = main i j
+  where
+  main :  Ω→ (-Susp A f) .fst (toSusp A a) ∙ Ω→ f .fst (toSusp A a) ≡ refl
+  main = cong₂ _∙_ (Ω→-Susp A f a) refl ∙ rCancel _
+snd (·SuspInvL A {B = B} f i) = refl
+
+·SuspAssoc : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+        (f g h : Susp∙ (typ A) →∙ B)
+     → ·Susp A f (·Susp A g h) ≡ ·Susp A (·Susp A f g) h
+·SuspAssoc A {B = B} f g h =
+  ΣPathP ((funExt (λ { north → refl
+                     ; south → refl
+                     ; (merid a i) j → main a j i}))
+    , refl)
+  where
+  main : (a : typ A) → Ω→ f .fst (toSusp A a)
+                      ∙ Ω→ (·Susp A g h) .fst (toSusp A a)
+                      ≡ Ω→ (·Susp A f g) .fst (toSusp A a)
+                      ∙ Ω→ h .fst (toSusp A a)
+  main a = cong₂ _∙_ refl (·Suspσ' g h a)
+         ∙ assoc _ _ _
+         ∙ cong₂ _∙_ (sym (·Suspσ' f g a)) refl
+
+·SuspIdR : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+        (f : Susp∙ (typ A) →∙ B)
+     → ·Susp A f (const∙ _ _) ≡ f
+·SuspIdR A f =
+     ΣPathP ((funExt
+     (λ { north → refl
+        ; south → refl
+        ; (merid a i) j → (cong₂ _∙_ refl (sym (rUnit refl))
+                         ∙ sym (rUnit (Ω→ f .fst (toSusp A a)))) j i}))
+     , refl)
+  ∙ Iso.rightInv (ΩSuspAdjointIso {A = A}) f
+
+
+·SuspIdL : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'} (f : Susp∙ (typ A) →∙ B)
+  → ·Susp A (const∙ _ _) f ≡ f
+·SuspIdL A f =
+   ΣPathP ((funExt
+     (λ { north → refl
+        ; south → refl
+        ; (merid a i) j → (cong₂ _∙_ (sym (rUnit refl)) refl
+                         ∙ sym (lUnit (Ω→ f .fst (toSusp A a)))) j i}))
+     , refl)
+  ∙ Iso.rightInv (ΩSuspAdjointIso {A = A}) f
+
+·SuspIdL≡·SuspIdR : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+  → ·SuspIdL A (const∙ _ B) ≡ ·SuspIdR A (const∙ _ B)
+·SuspIdL≡·SuspIdR A {B = B} =
+  cong₂ _∙_ (cong ΣPathP (ΣPathP (cong funExt (funExt
+                  (λ { north → refl
+                     ; south → refl
+                     ; (merid a i) k j
+                       → lem (pt B) (refl ∙ refl) (rUnit refl)
+                              (refl ∙ refl) (rUnit refl) k j i}))
+                     , refl)))
+            refl
+  where
+  lem : ∀ {ℓ} {A : Type ℓ} (x : A) (p : x ≡ x) (q : refl ≡ p)
+         (rr : x ≡ x) (q : refl ≡ rr)
+       → cong₂ _∙_ (sym q) (refl {x = rr}) ∙ sym (lUnit rr)
+        ≡ cong₂ _∙_ (refl {x = rr})  (sym q) ∙ sym (rUnit rr)
+  lem x = J> (J> refl)
+
+-Susp² : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'} (f : Susp∙ (typ A) →∙ B)
+  → -Susp A (-Susp A f) ≡ f
+-Susp² A f =
+    sym (·SuspAssoc A _ _ _
+      ∙ cong₂ (·Susp A) (·SuspInvR A f) refl
+      ∙ ·SuspIdL A _)
+  ∙ cong (·Susp A f) (·SuspInvR A (-Susp A f))
+  ∙ ·SuspIdR A f
+
+open import Cubical.Foundations.Pointed.Homogeneous
+·Susp≡·→Ω : ∀ {ℓ ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+  (f g : Susp∙ (typ A) →∙ Ω B)
+  → ·Susp A f g ≡ ·→Ω f g
+·Susp≡·→Ω A {B = B} f g =
+  →∙Homogeneous≡ (isHomogeneousPath _ _)
+    (funExt λ { north → rUnit refl
+                       ∙ cong₂ _∙_ (sym (snd f)) (sym (snd g))
+              ; south → rUnit refl
+                       ∙ cong₂ _∙_ (snd f ⁻¹ ∙ cong (fst f) (merid (pt A)))
+                                   (snd g ⁻¹ ∙ cong (fst g) (merid (pt A)))
+              ; (merid a i) j →
+                (cong₂ _∙_ (cong (sym (snd f) ∙∙_∙∙ snd f) (cong-∙ (fst f) _ _))
+                           (cong (sym (snd g) ∙∙_∙∙ snd g) (cong-∙ (fst g) _ _))
+                ◁ lem B _ (sym (snd f)) _
+                      (cong (fst f) (merid a))
+                      (cong (fst f) (merid (pt A)))
+                      _ (sym (snd g)) _
+                      (cong (fst g) (merid a))
+                      (cong (fst g) (merid (pt A)))) j i})
+  where
+  open import Cubical.Foundations.Path
+  lem : ∀ {ℓ} (A : Pointed ℓ) (⋆f : Ω A .fst) (sndf : refl ≡ ⋆f)
+              (⋆fs : Ω A .fst) (mfa mfb : ⋆f ≡ ⋆fs)
+              (⋆g : Ω A .fst) (sndg : refl ≡ ⋆g)
+              (⋆gs : Ω A .fst) (mga mgb : ⋆g ≡ ⋆gs)
+        → Square ((sndf ∙∙ mfa ∙ mfb ⁻¹ ∙∙ sym sndf)
+                  ∙ (sndg ∙∙ mga ∙ mgb ⁻¹ ∙∙ sym sndg))
+                 (cong₂ _∙_ mfa mga)
+                 (rUnit refl ∙ cong₂ _∙_ sndf sndg)
+                 (rUnit refl ∙ cong₂ _∙_ (sndf ∙ mfb) (sndg ∙ mgb))
+  lem A = J> (J> λ mfb → J> (J>
+    λ mgb → cong₂ _∙_ (sym (rUnit _) ∙ sym (lUnit (mfb ⁻¹)))
+                       (sym (rUnit _) ∙ sym (lUnit (mgb ⁻¹)))
+          ◁ flipSquare (sym (rUnit (rUnit refl))
+          ◁ (flipSquare (sym (symDistr mgb mfb)
+          ◁ flipSquare (compPath-filler' (mgb ∙ mfb) (rUnit refl)))
+          ▷ (cong (_∙ rUnit refl) (EH 0 mgb mfb)
+             ∙ lUnit _
+            ∙ (λ j → (λ i → rUnit refl (i ∧ j))
+                    ∙ (cong (λ x → rUnit x j) mfb
+                    ∙ cong (λ x → lUnit x j) mgb)
+                    ∙ λ i → rUnit refl (i ∨ j))
+            ∙ cong (rUnit refl ∙_)
+              (sym (rUnit _)
+              ∙ sym (cong₂Funct _∙_ mfb mgb)
+            ∙ (λ j → cong₂ _∙_ (lUnit mfb j) (lUnit mgb j))))))))
+
+Susp·→Ωcomm : ∀ {ℓ ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+  (f g : Susp∙ (typ A) →∙ Ω B) → ·→Ω f g ≡ ·→Ω g f
+Susp·→Ωcomm A {B = B} f g = isoInvInjective ΩSuspAdjointIso _ _
+  (cong fromSusp→toΩ (·Susp≡·→Ω _ f g ⁻¹)
+  ∙∙ help
+  ∙∙ cong fromSusp→toΩ (·Susp≡·→Ω _ g f))
+  where
+  help : Iso.inv ΩSuspAdjointIso (·Susp A f g)
+       ≡ Iso.inv ΩSuspAdjointIso (·Susp A g f)
+  help = →∙Homogeneous≡ (isHomogeneousPath _ _)
+    (funExt λ x → sym (rUnit _)
+                ∙ ·Suspσ f g x
+                ∙ EH 0 _ _
+                ∙ sym (·Suspσ g f x)
+                ∙ rUnit _)
+
+Susp·→Ωcomm' : ∀ {ℓ ℓ'} (A A' : Pointed ℓ)
+  → A ≃∙ Susp∙ (typ A') → {B : Pointed ℓ'}
+  (f g : A →∙ Ω B) → ·→Ω f g ≡ ·→Ω g f
+Susp·→Ωcomm' A A' e {B = B} =
+  Equiv∙J (λ A _ → (f g : A →∙ Ω B) → ·→Ω f g ≡ ·→Ω g f)
+    (Susp·→Ωcomm A') e
+
+·SuspComm : ∀ {ℓ ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+  (f g : Susp∙ (Susp (typ A)) →∙ B)
+  → ·Susp (Susp∙ (typ A)) f g ≡ ·Susp (Susp∙ (typ A)) g f
+·SuspComm A {B = B} f g = isoInvInjective ΩSuspAdjointIso _ _ cool
+  where
+  cool : Iso.inv ΩSuspAdjointIso (·Susp (Susp∙ (typ A)) f g)
+       ≡ Iso.inv ΩSuspAdjointIso (·Susp (Susp∙ (typ A)) g f)
+  cool = →∙Homogeneous≡ (isHomogeneousPath _ _)
+    (funExt λ x → sym (rUnit _)
+                ∙ ·Suspσ f g x
+                ∙ funExt⁻ (cong fst (Susp·→Ωcomm A
+                           (Iso.inv ΩSuspAdjointIso f) (Iso.inv ΩSuspAdjointIso g))) x
+                ∙ sym (·Suspσ g f x)
+                ∙ rUnit _)
+
+·SuspComm' : ∀ {ℓ ℓ'} (A A' : Pointed ℓ)
+  → A ≃∙ Susp∙ (typ A') → {B : Pointed ℓ'}
+  (f g : Susp∙ (typ A) →∙ B)
+  → ·Susp A f g ≡ ·Susp A g f
+·SuspComm' A A' e {B = B} =
+  Equiv∙J (λ A _ → (f g : Susp∙ (typ A) →∙ B)
+        → ·Susp A f g ≡ ·Susp A g f) (·SuspComm A') e
diff --git a/Cubical/Homotopy/Group/Base.agda b/Cubical/Homotopy/Group/Base.agda
index 4713d97de8..08756678e3 100644
--- a/Cubical/Homotopy/Group/Base.agda
+++ b/Cubical/Homotopy/Group/Base.agda
@@ -132,6 +132,16 @@ fst (-Π {A = A} {n = suc (suc n)} f) (merid a j) =
  fst f ((merid a ∙ sym (merid (ptSn _))) (~ j))
 snd (-Π {A = A} {n = suc (suc n)} f) = snd f
 
+-- Action of ∙Π on σ
+∙Πσ : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ} (f g : S₊∙ (suc n) →∙ A) (t : S₊ n)
+  → Square (cong (fst (∙Π f g)) (σS t))
+            (Ω→ f .fst (σS t) ∙ Ω→ g .fst (σS t))
+            (snd (∙Π f g)) (snd (∙Π f g))
+∙Πσ {A = A} {zero} f g false = refl
+∙Πσ {A = A} {zero} f g true =
+    rUnit refl
+  ∙ cong₂ _∙_ (sym (Ω→ f .snd)) (sym (Ω→ g .snd))
+∙Πσ {A = A} {suc n} f g t = ·Suspσ f g t
 
 -- to prove that this gives a group structure on π', we first
 -- prove that Ωⁿ A ≃ (Sⁿ →∙ A).
diff --git a/Cubical/Homotopy/Group/Join.agda b/Cubical/Homotopy/Group/Join.agda
index 0363b836a9..6160f59b15 100644
--- a/Cubical/Homotopy/Group/Join.agda
+++ b/Cubical/Homotopy/Group/Join.agda
@@ -14,9 +14,14 @@ open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
 
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
 open import Cubical.Data.Bool
 
 open import Cubical.HITs.SetTruncation as ST
@@ -24,6 +29,7 @@ open import Cubical.HITs.Sn
 open import Cubical.HITs.Susp renaming (toSusp to σ)
 open import Cubical.HITs.S1
 open import Cubical.HITs.Join
+open import Cubical.HITs.Join.CoHSpace
 open import Cubical.HITs.Sn.Multiplication
 
 open import Cubical.Algebra.Group
@@ -34,32 +40,9 @@ open import Cubical.Algebra.Group.GroupPath
 open Iso
 open GroupStr
 
--- Standard loop in Ω (join A B)
-ℓ* : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
-  → fst A → fst B → Ω (join∙ A B) .fst
-ℓ* A B a b = push (pt A) (pt B)
-           ∙ (push a (pt B) ⁻¹ ∙∙ push a b ∙∙ (push (pt A) b ⁻¹))
-
 ℓS : {n m : ℕ} → S₊ n → S₊ m → Ω (join∙ (S₊∙ n) (S₊∙ m)) .fst
 ℓS {n = n} {m} = ℓ* (S₊∙ n) (S₊∙ m)
 
--- Addition of functions join A B → C
-_+*_ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
-  (f g : join∙ A B →∙ C) → join∙ A B →∙ C
-fst (_+*_ {C = C} f g) (inl x) = pt C
-fst (_+*_ {C = C} f g) (inr x) = pt C
-fst (_+*_ {A = A} {B = B} f g) (push a b i) =
-  (Ω→ f .fst (ℓ* A B a b) ∙ Ω→ g .fst (ℓ* A B a b)) i
-snd (f +* g) = refl
-
--- Inversion
--* : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
-      (f : join∙ A B →∙ C) → join∙ A B →∙ C
-fst (-* {C = C} f) (inl x) = pt C
-fst (-* {C = C} f) (inr x) = pt C
-fst (-* {A = A} {B} f) (push a b i) = Ω→ f .fst (ℓ* A B a b) (~ i)
-snd (-* f) = refl
-
 -- -Π is the same as -*
 -Π≡-* : ∀ {ℓ} {A : Pointed ℓ} {n m : ℕ}
     (f : S₊∙ (suc (n + m)) →∙ A)
@@ -186,6 +169,9 @@ snd (·Π≡+* {A = A} f g i) j = lem i j
 -π* : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} (f : π* n m A) → π* n m A
 -π* = ST.map -*
 
+-π*^ : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} (k : ℕ) (f : π* n m A) → π* n m A
+-π*^ n = iter n -π*
+
 1π* : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} → π* n m A
 1π* = ∣ const∙ _ _ ∣₂
 
@@ -330,3 +316,81 @@ snd (π*∘∙Hom {A = A} {B = B} n m f) =
   → GroupEquiv (π*Gr n m A) (π*Gr n m B)
 fst (π*∘∙Equiv n m f) = isoToEquiv (setTruncIso (pre∘∙equiv f))
 snd (π*∘∙Equiv n m f) = π*∘∙Hom n m (≃∙map f) .snd
+
+-- Swapping indices
+π*SwapIso : ∀ {ℓ} (n m : ℕ) (A : Pointed ℓ)
+  → Iso (π* n m A) (π* m n A)
+π*SwapIso n m A =
+  setTruncIso (post∘∙equiv
+    (isoToEquiv join-comm , push (ptSn m) (ptSn n) ⁻¹))
+
+
+-- This is a group iso whenever n + m > 0
+π*GrSwapIso : ∀ {ℓ} (n m : ℕ) (A : Pointed ℓ)
+  → (n + m > 0)
+  → GroupIso (π*Gr n m A) (π*Gr m n A)
+fst (π*GrSwapIso n m A pos) = π*SwapIso n m A
+snd (π*GrSwapIso n m A pos) =
+  makeIsGroupHom (elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
+    λ f g → cong ∣_∣₂ (ΣPathP ((funExt
+      (λ { (inl x) → refl
+         ; (inr x) → refl
+        ; (push a b i) j → main f g b a j i}))
+          , (sym (rUnit _)
+           ∙ cong (cong (fst (f +* g)))
+             (cong₂ _∙_ refl (∙∙lCancel _) ∙ sym (rUnit _)))
+           ∙ cong sym
+             (cong₂ _∙_
+               (cong (Ω→ f .fst) (ℓ*IdL (S₊∙ n) (S₊∙ m) (ptSn m)) ∙ Ω→ f .snd)
+               ((cong (Ω→ g .fst) (ℓ*IdL (S₊∙ n) (S₊∙ m) (ptSn m)) ∙ Ω→ g .snd))
+               ∙ rCancel _))))
+  where
+  com : (n m : ℕ) → (n + m > 0)
+     → (f g : join∙ (S₊∙ n) (S₊∙ m) →∙ A) (a : _) (b : _)
+    → (Ω→ f .fst (ℓ* (S₊∙ n) (S₊∙ m) a b)
+      ∙ Ω→ g .fst (ℓ* (S₊∙ n) (S₊∙ m) a b))
+    ≡ (Ω→ g .fst (ℓ* (S₊∙ n) (S₊∙ m) a b)
+      ∙ Ω→ f .fst (ℓ* (S₊∙ n) (S₊∙ m) a b))
+  com zero zero p f g a b = ⊥.rec (snotz (+-comm 1 (fst p) ∙ snd p))
+  com zero (suc m) p f g a b i =
+    Susp·→Ωcomm' (S₊∙ (suc m)) (S₊∙ m)
+                  (isoToEquiv (IsoSucSphereSusp _) , IsoSucSphereSusp∙' m)
+      (F f) (F g) i .fst b
+    where
+    F : (f : join∙ (S₊∙ zero) (S₊∙ (suc m)) →∙ A) → Σ _ _
+    F f = (λ b → Ω→ f .fst (ℓ* (S₊∙ zero) (S₊∙ (suc m)) a b))
+      , cong (fst (Ω→ f)) (ℓ*IdR (S₊∙ zero) (S₊∙ (suc m)) a) ∙ Ω→ f .snd
+  com (suc n) m p f g a b i =
+    Susp·→Ωcomm' (S₊∙ (suc n)) (S₊∙ n)
+                  ((isoToEquiv (IsoSucSphereSusp _) , IsoSucSphereSusp∙' n))
+      (F f) (F g) i .fst a
+    where
+    F : (f : join∙ (S₊∙ (suc n)) (S₊∙ m) →∙ A) → Σ _ _
+    F f = (λ a → Ω→ f .fst (ℓ* (S₊∙ (suc n)) (S₊∙ m) a b))
+      , cong (fst (Ω→ f)) (ℓ*IdL (S₊∙ (suc n)) (S₊∙ m) b) ∙ Ω→ f .snd
+
+  main : (f g : join∙ (S₊∙ n) (S₊∙ m) →∙ A) (a : _) (b : _)
+    → (Ω→ f .fst (ℓ* (S₊∙ n) (S₊∙ m) a b)
+     ∙ Ω→ g .fst (ℓ* (S₊∙ n) (S₊∙ m) a b)) ⁻¹
+     ≡ Ω→ (f ∘∙ (join-commFun , _)) .fst (ℓ* (S₊∙ m) (S₊∙ n) b a)
+    ∙  Ω→ (g ∘∙ (join-commFun , _)) .fst (ℓ* (S₊∙ m) (S₊∙ n) b a)
+  main f g a b =
+   cong sym (com n m pos f g a b)
+    ∙ symDistr _ _
+    ∙ sym (cong₂ _∙_ (main-path f) (main-path g))
+    where
+    h : invEquiv∙ ((isoToEquiv join-comm , push (ptSn m) (ptSn n) ⁻¹)) .snd
+      ≡ push (ptSn n) (ptSn m) ⁻¹
+    h = cong₂ _∙_ refl (∙∙lCancel _) ∙ sym (rUnit _)
+
+    main-path : (f : join∙ (S₊∙ n) (S₊∙ m) →∙ A) → _
+    main-path  f =
+       (λ i → fst (Ω→∘∙ f (join-commFun , h i) i) ((ℓ* (S₊∙ m) (S₊∙ n) b a)))
+      ∙ cong (Ω→ f .fst)
+             (sym (PathP→compPathR∙∙
+               (symP (compPathR→PathP∙∙ (join-commFun-ℓ* _ _ _ _)))))
+
+-π*^≡ : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} (k : ℕ)
+  (f : join∙ (S₊∙ n) (S₊∙ m) →∙ A) → -π*^ k ∣ f ∣₂ ≡ ∣ -*^ k f ∣₂
+-π*^≡ zero f = refl
+-π*^≡ (suc k) f = cong -π* (-π*^≡ k f)
diff --git a/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda b/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda
index e075036948..20827deebd 100644
--- a/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda
+++ b/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda
@@ -14,7 +14,8 @@ open import Cubical.Homotopy.HopfInvariant.Base
 open import Cubical.Homotopy.Group.Pi3S2
 open import Cubical.Homotopy.Group.PinSn
 open import Cubical.Homotopy.BlakersMassey
-open import Cubical.Homotopy.Whitehead
+open import Cubical.Homotopy.WhiteheadProducts.Base
+open import Cubical.Homotopy.WhiteheadProducts.Properties
 open import Cubical.Homotopy.Connected
 open import Cubical.Homotopy.Group.LES
 open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2
diff --git a/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda b/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda
index 3ebf02c48f..f2eeaab22a 100644
--- a/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda
+++ b/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda
@@ -62,7 +62,7 @@ open import Cubical.Homotopy.Group.Base
 open import Cubical.Homotopy.Group.Pi3S2
 open import Cubical.Homotopy.Group.PinSn
 open import Cubical.Homotopy.Hopf
-open import Cubical.Homotopy.Whitehead using (joinTo⋁)
+open import Cubical.Homotopy.WhiteheadProducts.Base using (joinTo⋁)
 open import Cubical.Homotopy.Connected
 open import Cubical.Homotopy.HopfInvariant.HopfMap using (hopfMap≡HopfMap')
 -- Only imports a simple equality of two constructions of the Hopf map.
@@ -85,6 +85,7 @@ open import Cubical.HITs.Sn
 open import Cubical.HITs.Sn.Multiplication
 open import Cubical.HITs.Susp renaming (toSusp to σ)
 open import Cubical.HITs.Join hiding (joinS¹S¹→S³)
+open import Cubical.HITs.Join.CoHSpace
 open import Cubical.HITs.Wedge
 open import Cubical.HITs.Pushout
 open import Cubical.HITs.SetTruncation
diff --git a/Cubical/Homotopy/Group/Pi4S3/Summary.agda b/Cubical/Homotopy/Group/Pi4S3/Summary.agda
index ad0238341e..fc11aa3ca3 100644
--- a/Cubical/Homotopy/Group/Pi4S3/Summary.agda
+++ b/Cubical/Homotopy/Group/Pi4S3/Summary.agda
@@ -34,7 +34,8 @@ open import Cubical.Homotopy.HopfInvariant.Base
 open import Cubical.Homotopy.HopfInvariant.Homomorphism
 open import Cubical.Homotopy.HopfInvariant.HopfMap
 open import Cubical.Homotopy.HopfInvariant.Brunerie
-open import Cubical.Homotopy.Whitehead
+open import Cubical.Homotopy.WhiteheadProducts.Base
+open import Cubical.Homotopy.WhiteheadProducts.Properties
 open import Cubical.Homotopy.Group.Base hiding (π)
 open import Cubical.Homotopy.Group.Pi3S2
 open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber
diff --git a/Cubical/Homotopy/HopfInvariant/Brunerie.agda b/Cubical/Homotopy/HopfInvariant/Brunerie.agda
index 2ebb7d472f..01bf08a8de 100644
--- a/Cubical/Homotopy/HopfInvariant/Brunerie.agda
+++ b/Cubical/Homotopy/HopfInvariant/Brunerie.agda
@@ -12,7 +12,7 @@ module Cubical.Homotopy.HopfInvariant.Brunerie where
 open import Cubical.Homotopy.HopfInvariant.Base
 open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber
 open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso
-open import Cubical.Homotopy.Whitehead
+open import Cubical.Homotopy.WhiteheadProducts.Base
 
 open import Cubical.ZCohomology.Base
 open import Cubical.ZCohomology.GroupStructure
diff --git a/Cubical/Homotopy/Loopspace.agda b/Cubical/Homotopy/Loopspace.agda
index 36fef7ea1f..1606fdd5c2 100644
--- a/Cubical/Homotopy/Loopspace.agda
+++ b/Cubical/Homotopy/Loopspace.agda
@@ -460,3 +460,10 @@ EH-π : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (p q : ∥ typ ((Ω^ (2 + n)) A) 
                → π-comp (1 + n) p q ≡ π-comp (1 + n) q p
 EH-π  n = elim2 (λ x y → isOfHLevelPath 2 isSetSetTrunc _ _)
                              λ p q → cong ∣_∣₂ (EH n p q)
+
+-- composition of maps into loop spaces
+·→Ω : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
+  (f g : A →∙ Ω B)
+  → A →∙ Ω B
+fst (·→Ω f g) x = fst f x ∙ fst g x
+snd (·→Ω f g) = cong₂ _∙_ (snd f) (snd g) ∙ sym (rUnit refl)
diff --git a/Cubical/Homotopy/WhiteheadProducts/Base.agda b/Cubical/Homotopy/WhiteheadProducts/Base.agda
new file mode 100644
index 0000000000..1fbac4a11d
--- /dev/null
+++ b/Cubical/Homotopy/WhiteheadProducts/Base.agda
@@ -0,0 +1,130 @@
+{-# OPTIONS --safe --lossy-unification #-}
+module Cubical.Homotopy.WhiteheadProducts.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
+open import Cubical.Foundations.GroupoidLaws
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
+open import Cubical.Data.Bool
+open import Cubical.Data.Int using (ℤ ; pos)
+
+open import Cubical.HITs.Susp renaming (toSusp to σ)
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Sn
+open import Cubical.HITs.Sn.Multiplication
+open import Cubical.HITs.Join
+open import Cubical.HITs.Wedge
+open import Cubical.HITs.SetTruncation
+open import Cubical.HITs.PropositionalTruncation as PT hiding (elim2)
+open import Cubical.HITs.Truncation as TR hiding (elim2)
+open import Cubical.HITs.S1
+
+open import Cubical.Homotopy.Group.Base
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Join
+open import Cubical.Homotopy.Connected
+
+open Iso
+
+-- Whitehead product (main definition)
+[_∣_]-pre : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (S₊∙ (suc n) →∙ X)
+       → (S₊∙ (suc m) →∙ X)
+       → join∙ (S₊∙ n) (S₊∙ m) →∙ X
+[_∣_]-pre {X = X} {n = n} {m = m} f g =
+  joinPinch∙ (S₊∙ n) (S₊∙ m) X
+    (λ a b → (Ω→ g .fst (σS b) ∙ Ω→ f .fst (σS a)))
+
+open import Cubical.Homotopy.WhiteheadProducts.Generalised.Base
+[_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (S₊∙ (suc n) →∙ X)
+       → (S₊∙ (suc m) →∙ X)
+       → S₊∙ (suc (n + m)) →∙ X
+[_∣_] {n = n} {m = m} f g =
+  [ f ∣ g ]-pre ∘∙ (sphere→Join n m , IsoSphereJoin⁻Pres∙ n m)
+
+-- Homotopy group versions
+[_∣_]π' : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → π' (suc n) X → π' (suc m) X
+       → π' (suc (n + m)) X
+[_∣_]π' = elim2 (λ _ _ → squash₂) λ f g → ∣ [ f ∣ g ] ∣₂
+
+-- Join version
+[_∣_]π* : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → π' (suc n) X → π' (suc m) X
+       → π* n m X
+[_∣_]π* = elim2 (λ _ _ → squash₂) λ f g → ∣ [ f ∣ g ]-pre ∣₂
+
+-- The two versions agree
+whπ*≡whπ' : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (f : π' (suc n) X) (g : π' (suc m) X)
+       → [ f ∣ g ]π' ≡ Iso.fun (Iso-π*-π' n m ) [ f ∣ g ]π*
+whπ*≡whπ' {n = n} {m} = elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
+  λ f g → TR.rec (squash₂ _ _)
+          (λ p → cong ∣_∣₂ (ΣPathP (refl , (sym (rUnit _)
+                ∙ cong (cong (fst [ f ∣ g ]-pre)) p
+                ∙ rUnit _))))
+          (help n m)
+  where
+  help : (n m : ℕ)
+    → hLevelTrunc 1 (IsoSphereJoin⁻Pres∙ n m
+                   ≡ snd (≃∙map (invEquiv∙ (joinSphereEquiv∙ n m))))
+  help zero zero = ∣ invEq (congEquiv F) (λ _ → pos 0) ∣ₕ
+    where
+    F : (Path (join (S₊ 0) (S₊ 0)) (inr true) (inl true)) ≃ ℤ
+    F = compEquiv ( (compPathlEquiv (push true true)))
+                (compEquiv ((Ω≃∙ (isoToEquiv (IsoSphereJoin 0 0) , refl) .fst))
+                (isoToEquiv ΩS¹Isoℤ))
+  help zero (suc m) =
+    isConnectedPath 1
+      (isConnectedPath 2
+        (isOfHLevelRetractFromIso 0
+          (mapCompIso (IsoSphereJoin zero (suc m)))
+            (isConnectedSubtr 3 m
+              (subst (λ p → isConnected p (S₊ (2 + m)))
+                (+-comm 3 m)
+                (sphereConnected (2 + m))))) _ _) _ _ .fst
+  help (suc n) m =
+    isConnectedPath 1
+      (isConnectedPath 2
+        (isOfHLevelRetractFromIso 0
+          (mapCompIso (IsoSphereJoin (suc n) m))
+            (isConnectedSubtr 3 (n + m)
+              (subst (λ p → isConnected p (S₊ (2 + (n + m))))
+                (+-comm 3 (n + m)) (sphereConnected (2 + (n + m)))))) _ _) _ _ .fst
+
+whπ'≡whπ* : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (f : π' (suc n) X) (g : π' (suc m) X)
+       → Iso.inv (Iso-π*-π' n m) [ f ∣ g ]π' ≡ [ f ∣ g ]π*
+whπ'≡whπ* {n = n} {m} f g =
+  cong (inv (Iso-π*-π' n m)) (whπ*≡whπ' f g)
+  ∙ Iso.leftInv (Iso-π*-π' n m) _
+
+-- Whitehead product (as a composition)
+joinTo⋁ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
+ → join (typ A) (typ B)
+ → (Susp (typ A) , north) ⋁ (Susp (typ B) , north)
+joinTo⋁ (inl x) = inr north
+joinTo⋁ (inr x) = inl north
+joinTo⋁ {A = A} {B = B} (push a b i) =
+     ((λ i → inr (σ B b i))
+  ∙∙ sym (push tt)
+  ∙∙ λ i → inl (σ A a i)) i
+
+[_∣_]comp : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (S₊∙ (suc n) →∙ X)
+       → (S₊∙ (suc m) →∙ X)
+       → S₊∙ (suc (n + m)) →∙ X
+[_∣_]comp {n = n} {m = m} f g =
+    (((f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
+  ∨→ (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))
+    , cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f)
+  ∘∙ ((joinTo⋁ {A = S₊∙ n} {B = S₊∙ m} , sym (push tt))))
+  ∘∙ (inv (IsoSphereJoin n m) , IsoSphereJoin⁻Pres∙ n m)
diff --git a/Cubical/Homotopy/WhiteheadProducts/Generalised/Base.agda b/Cubical/Homotopy/WhiteheadProducts/Generalised/Base.agda
new file mode 100644
index 0000000000..d7164b71cd
--- /dev/null
+++ b/Cubical/Homotopy/WhiteheadProducts/Generalised/Base.agda
@@ -0,0 +1,202 @@
+{-# OPTIONS --safe --lossy-unification #-}
+module Cubical.Homotopy.WhiteheadProducts.Generalised.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Pointed.Homogeneous
+open import Cubical.Foundations.GroupoidLaws
+
+open import Cubical.Data.Sigma
+
+open import Cubical.HITs.Susp renaming (toSusp to σ)
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Join
+open import Cubical.HITs.Join.CoHSpace
+open import Cubical.HITs.SmashProduct
+
+open import Cubical.Homotopy.Loopspace
+
+open Iso
+open 3x3-span
+
+
+-- Generalised Whitehead products
+module _ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
+         (B : Pointed ℓ') {C : Pointed ℓ''}
+         (f : Susp∙ (typ A) →∙ C) (g : Susp∙ (typ B) →∙ C) where
+
+  ·wh : join∙ A B →∙ C
+  ·wh = joinPinch∙ A B C
+         (λ a b → (Ω→ g .fst (σ B b) ∙ Ω→ f .fst (σ A a)))
+
+  -- alternative version using Suspension and smash
+  private
+    ·whΣ' : Susp∙ (Smash A B) →∙ C
+    fst ·whΣ' north = pt C
+    fst ·whΣ' south = pt C
+    fst ·whΣ' (merid basel i) = pt C
+    fst ·whΣ' (merid baser i) = pt C
+    fst ·whΣ' (merid (proj a b) i) =
+        (Ω→ f .fst (σ A a) ⁻¹
+      ∙ (Ω→ g .fst (σ B b) ∙ Ω→ f .fst (σ A a))
+       ∙ Ω→ g .fst (σ B b) ⁻¹) i
+    fst ·whΣ' (merid (gluel a i₁) i) =
+      (cong (λ p → (Ω→ f .fst (σ A a) ⁻¹ ∙ (p ∙ Ω→ f .fst (σ A a)) ∙ p ⁻¹))
+            (Iso.inv ΩSuspAdjointIso g .snd)
+     ∙ cong₂ _∙_ refl (sym (rUnit _) ∙ sym (lUnit _))
+     ∙ lCancel _) i₁ i
+    fst ·whΣ' (merid (gluer b i₁) i) =
+      (cong (λ p → (p ⁻¹ ∙ (Ω→ g .fst (σ B b) ∙ p) ∙ Ω→ g .fst (σ B b) ⁻¹))
+            (Iso.inv ΩSuspAdjointIso f .snd)
+     ∙ (sym (lUnit _) ∙ cong₂ _∙_ (sym (rUnit _)) refl)
+     ∙ lCancel _) i₁ i
+    snd ·whΣ' = refl
+
+  ·whΣ : Susp∙ (A ⋀ B) →∙ C
+  fst ·whΣ = fst ·whΣ' ∘ suspFun ⋀→Smash
+  snd ·whΣ = refl
+
+  -- The two versions agree modulo the equivalence Σ(A ⋀ B) ≃ A * B
+  ·wh≡·whΣ : ·wh ∘∙ (SuspSmash→Join∙ A B) ≡ ·whΣ
+  ·wh≡·whΣ = ΣPathP (funExt lem , (sym (rUnit _)
+    ∙ cong sym (cong₂ _∙_
+       (Iso.inv ΩSuspAdjointIso g .snd)
+       (Iso.inv ΩSuspAdjointIso f .snd)
+      ∙ sym (rUnit refl))))
+    where
+    lem : (x : _) → ·wh .fst (Iso.fun (SmashJoinIso {A = A} {B = B}) x)
+                  ≡ ·whΣ .fst x
+    lem north = refl
+    lem south = refl
+    lem (merid a i) j = main j a i
+      where
+      main : Path ((A ⋀ B) → Ω C .fst)
+                  (cong (·wh .fst ∘ SuspSmash→Join) ∘ merid)
+                  (cong (fst ·whΣ') ∘ merid ∘ ⋀→Smash)
+      main = ⋀→Homogeneous≡ (isHomogeneousPath _ _)
+        λ x y → cong-∙∙ (·wh .fst) (push x (pt B) ⁻¹) (push x y) (push (pt A) y ⁻¹)
+              ∙ doubleCompPath≡compPath _ _ _
+              ∙ cong₂ _∙_ (cong sym
+                           (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso g .snd) refl
+                          ∙ sym (lUnit _)))
+                      (cong₂ _∙_ refl
+                           (cong sym
+                           (cong₂ _∙_ refl (Iso.inv ΩSuspAdjointIso f .snd)
+                          ∙ sym (rUnit _))))
+
+--- Other elementary properties and lemmas ---
+
+  -- The generalised Whitehead product vanishes under suspension
+  isConst-Susp·w : suspFun∙ (·wh .fst) ≡ const∙ _ _
+  isConst-Susp·w = Susp·w∙
+                 ∙ cong suspFun∙ (cong fst isConst-const*)
+                 ∙ ΣPathP ((suspFunConst (pt C)) , refl)
+    where
+    const* : join∙ A B →∙ C
+    fst const* (inl x) = pt C
+    fst const* (inr x) = pt C
+    fst const* (push a b i) =
+      (Ω→ f .fst (σ A a) ∙ Ω→ g .fst (σ B b)) i
+    snd const* = refl
+
+    isConst-const* : const* ≡ const∙ _ _
+    fst (isConst-const* i) (inl x) = Ω→ f .fst (σ A x) i
+    fst (isConst-const* i) (inr x) = Ω→ g .fst (σ B x) (~ i)
+    fst (isConst-const* i) (push a b j) =
+      compPath-filler'' (Ω→ f .fst (σ A a)) (Ω→ g .fst (σ B b)) (~ i) j
+    snd (isConst-const* i) j =
+      (cong (Ω→ f .fst) (rCancel (merid (pt A))) ∙ Ω→ f .snd) j i
+
+    Susp·w : suspFun (fst ·wh) ≡ suspFun (fst const*)
+    Susp·w i north = north
+    Susp·w i south = south
+    Susp·w i (merid (inl x) j) = merid (pt C) j
+    Susp·w i (merid (inr x) j) = merid (pt C) j
+    Susp·w i (merid (push a b k) j) =
+      hcomp (λ r →
+        λ {(i = i0) → fill₁ k (~ r) j
+         ; (i = i1) → fill₂ k (~ r) j
+         ; (j = i0) → north
+         ; (j = i1) → merid (pt C) r
+         ; (k = i0) → compPath-filler (merid (snd C)) (merid (pt C) ⁻¹) (~ r) j
+         ; (k = i1) → compPath-filler (merid (snd C)) (merid (pt C) ⁻¹) (~ r) j})
+       (hcomp (λ r →
+        λ {(i = i0) → doubleCompPath-filler
+                         (sym (rCancel (merid (pt C))))
+                         (λ k → fill₁ k i1)
+                         (rCancel (merid (pt C))) (~ r) k j
+         ; (i = i1) → doubleCompPath-filler
+                         (sym (rCancel (merid (pt C))))
+                         (λ k → fill₂ k i1)
+                         (rCancel (merid (pt C))) (~ r) k j
+         ; (j = i0) → north
+         ; (j = i1) → north
+         ; (k = i0) → rCancel (merid (pt C)) (~ r) j
+         ; (k = i1) → rCancel (merid (pt C)) (~ r) j})
+           (main i k j))
+      where
+      F : Ω C .fst → (Ω^ 2) (Susp∙ (fst C)) .fst
+      F p = sym (rCancel (merid (pt C)))
+         ∙∙ cong (σ C) p
+         ∙∙ rCancel (merid (pt C))
+
+      F-hom : (p q : _) → F (p ∙ q) ≡ F p ∙ F q
+      F-hom p q =
+          cong (sym (rCancel (merid (pt C)))
+               ∙∙_∙∙ rCancel (merid (pt C)))
+               (cong-∙ (σ C) p q)
+        ∙ doubleCompPath≡compPath (sym (rCancel (merid (pt C)))) _ _
+        ∙ cong (sym (rCancel (merid (pt C))) ∙_)
+               (sym (assoc _ _ _))
+        ∙ assoc _ _ _
+        ∙ (λ i → (sym (rCancel (merid (pt C)))
+                ∙ compPath-filler (cong (σ C) p) (rCancel (merid (pt C))) i)
+                ∙ compPath-filler' (sym (rCancel (merid (pt C))))
+                                   (cong (σ C) q ∙ rCancel (merid (pt C))) i)
+        ∙ cong₂ _∙_ (sym (doubleCompPath≡compPath _ _ _))
+                    (sym (doubleCompPath≡compPath _ _ _))
+
+      main : F ((Ω→ g .fst (σ B b) ∙ Ω→ f .fst (σ A a)))
+           ≡ F ((Ω→ f .fst (σ A a) ∙ Ω→ g .fst (σ B b)))
+      main = F-hom (Ω→ g .fst (σ B b)) (Ω→ f .fst (σ A a))
+           ∙ EH 0 _ _
+           ∙ sym (F-hom (Ω→ f .fst (σ A a)) (Ω→ g .fst (σ B b)))
+
+      fill₁ : (k : I) → _
+      fill₁ k = compPath-filler
+                (merid ((Ω→ g .fst (σ B b)
+                       ∙ Ω→ f .fst (σ A a)) k))
+                (merid (pt C) ⁻¹)
+
+      fill₂ : (k : I) → _
+      fill₂ k = compPath-filler
+                (merid ((Ω→ f .fst (σ A a)
+                       ∙ Ω→ g .fst (σ B b)) k))
+                (merid (pt C) ⁻¹)
+
+    Susp·w∙ : suspFun∙ (·wh .fst) ≡ suspFun∙ (fst const*)
+    Susp·w∙ = ΣPathP (Susp·w , refl)
+
+-- Action on the standard loop in Ω (join A B)
+cong·wh-ℓ* : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+     (f : Susp∙ (typ A) →∙ C) (g : Susp∙ (typ B) →∙ C)
+     (a : _) (b : _)
+  → (cong (fst (·wh A B f g)) (ℓ* A B a b))
+  ≡ ((Ω→ f .fst (σ A a) ⁻¹)
+  ∙∙ (Ω→ g .fst (σ B b) ∙ Ω→ f .fst (σ A a))
+  ∙∙ (Ω→ g .fst (σ B b) ⁻¹))
+cong·wh-ℓ* {A = A} {B = B} f g a b =
+    cong-∙ (fst (·wh A B f g)) _ _
+  ∙ cong₂ _∙_ (cong₂ _∙_ gp fp
+            ∙ sym (rUnit _))
+            (cong-∙∙ (fst (·wh A B f g)) _ _ _
+          ∙ cong₃ _∙∙_∙∙_
+              (cong _⁻¹ (cong₂ _∙_ gp refl ∙ sym (lUnit _)))
+              refl
+              (cong _⁻¹ (cong₂ _∙_ refl fp ∙ sym (rUnit _))))
+  ∙ sym (lUnit _)
+  where
+  fp = cong (Ω→ f .fst) (rCancel _) ∙ Ω→ f .snd
+  gp = cong (Ω→ g .fst) (rCancel _) ∙ Ω→ g .snd
diff --git a/Cubical/Homotopy/WhiteheadProducts/Generalised/Properties.agda b/Cubical/Homotopy/WhiteheadProducts/Generalised/Properties.agda
new file mode 100644
index 0000000000..a482205a85
--- /dev/null
+++ b/Cubical/Homotopy/WhiteheadProducts/Generalised/Properties.agda
@@ -0,0 +1,1014 @@
+{-# OPTIONS --safe --lossy-unification #-}
+module Cubical.Homotopy.WhiteheadProducts.Generalised.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Pointed.Homogeneous
+open import Cubical.Foundations.GroupoidLaws
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma
+
+open import Cubical.HITs.Susp renaming (toSusp to σ)
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Sn
+open import Cubical.HITs.Sn.Multiplication
+open import Cubical.HITs.Join
+open import Cubical.HITs.Join.CoHSpace
+open import Cubical.HITs.Wedge
+open import Cubical.HITs.SmashProduct
+
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.WhiteheadProducts.Generalised.Base
+
+open Iso
+open 3x3-span
+
+-- Left bilinearity of generalised whitehead product
+module _ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
+  (B : Pointed ℓ') {C : Pointed ℓ''}
+  (f g : Susp∙ (Susp (typ A)) →∙ C)
+  (h : Susp∙ (typ B) →∙ C) where
+  private
+    σΣA = σ (Susp∙ (typ A))
+    Ω→f∙ = cong (Ω→ f .fst) (rCancel (merid north)) ∙ Ω→ f .snd
+    Ω→g∙ = cong (Ω→ g .fst) (rCancel (merid north)) ∙ Ω→ g .snd
+
+  WhiteheadProdBilinₗ : ·wh (Susp∙ (typ A)) B (·Susp (Susp∙ (typ A)) f g) h
+                     ≡ (·wh (Susp∙ (typ A)) B f h)
+                    +* (·wh (Susp∙ (typ A)) B g h)
+  fst (WhiteheadProdBilinₗ i) (inl x) =
+    (Ω→ g .fst (σΣA x) ∙ Ω→ f .fst (σΣA x)) i
+  fst (WhiteheadProdBilinₗ i) (inr x) = Ω→ h .fst (σ B x) (~ i)
+  fst (WhiteheadProdBilinₗ i) (push a b j) = main i j
+    where
+    x = Ω→ f .fst (σΣA a)
+    y = Ω→ g .fst (σΣA a)
+    z = Ω→ h .fst (σ B b)
+
+    fun1 fun2 fun3 : Susp∙ (typ A) →∙ Ω C
+    fst fun1 a = z ⁻¹ ∙ (Ω→ g .fst (σΣA a)) ⁻¹ ∙ z
+    snd fun1 = cong (z ⁻¹ ∙_) (cong (_∙ z) (cong sym Ω→g∙)
+                            ∙ sym (lUnit z))
+             ∙ lCancel z
+    fst fun2 a = ((z ∙ Ω→ f .fst (σΣA a)) ∙ Ω→ g .fst (σΣA a)) ∙ z ⁻¹
+    snd fun2 = cong (_∙ z ⁻¹)
+                   (cong₂ _∙_ (cong (z ∙_)
+                               Ω→f∙ ∙ sym (rUnit _))
+                               Ω→g∙
+                 ∙ sym (rUnit _))
+            ∙ rCancel z
+    fun3 = Ω→ g ∘∙ toSuspPointed (Susp∙ (typ A))
+
+    lem : y ⁻¹ ∙ ((z ∙ x) ∙ y) ∙ z ⁻¹
+       ≡ (z ∙ x ∙ z ⁻¹) ∙ ((y ⁻¹ ∙ z) ∙ y) ∙ z ⁻¹
+    lem = (sym (funExt⁻ (cong fst
+                  (Susp·→Ωcomm A fun2 ((sym , refl) ∘∙ fun3))) a)
+        ∙ sym (assoc _ _ _)
+        ∙ sym (assoc _ _ _))
+        ∙ (λ j → (z ∙ x) ∙ y ∙ z ⁻¹ ∙ (rUnit (y ⁻¹) j))
+        ∙ rUnit _
+        ∙ (λ i → ((z ∙ x) ∙ y ∙ z ⁻¹ ∙ y ⁻¹
+                 ∙ λ j → z (j ∧ i)) ∙ λ j → z (~ j ∧ i))
+        ∙ cong (_∙ z ⁻¹)
+        (cong ((z ∙ x) ∙_)
+            (sym (funExt⁻ (cong fst (Susp·→Ωcomm A fun1 fun3)) a)
+           ∙ sym (assoc _ _ _))
+        ∙ assoc _ _ _
+        ∙ cong₂ _∙_ (sym (assoc z x (z ⁻¹)))
+                    refl)
+        ∙ sym (assoc _ _ _)
+
+    main : Square (cong (·wh (Susp∙ (typ A)) B
+                          (·Susp (Susp∙ (typ A)) f g) h .fst) (push a b))
+                  (cong (((·wh (Susp∙ (typ A)) B f h)
+                       +* (·wh (Susp∙ (typ A)) B g h)) .fst) (push a b))
+                  (y ∙ x) (z ⁻¹)
+    main = cong₂ _∙_ refl (sym (rUnit _) ∙ ·Suspσ f g a)
+        ∙ assoc z x y
+       ◁ doubleCompPath-filler (sym (y ∙ x)) ((z ∙ x) ∙ y) (z ⁻¹)
+       ▷ (doubleCompPath≡compPath _ _ _
+        ∙ cong₂ _∙_ (symDistr y x) refl
+        ∙ sym (assoc (x ⁻¹) (y ⁻¹) _)
+        ∙ cong (x ⁻¹ ∙_) lem
+        ∙ assoc (x ⁻¹) (z ∙ x ∙ z ⁻¹) (((y ⁻¹ ∙ z) ∙ y) ∙ z ⁻¹)
+         ∙ cong₂ _∙_ (cong (x ⁻¹ ∙_) (assoc z x (z ⁻¹)))
+                     (cong (_∙ z ⁻¹) (sym (assoc (y ⁻¹) z y))
+                     ∙ sym (assoc (y ⁻¹) (z ∙ y) _))
+         ∙ sym (cong₂ _∙_ (sym (rUnit _) ∙ cong·wh-ℓ* f h a b
+                          ∙ doubleCompPath≡compPath _ _ _)
+                          (sym (rUnit _) ∙ cong·wh-ℓ* g h a b
+                          ∙ doubleCompPath≡compPath _ _ _)))
+
+  snd (WhiteheadProdBilinₗ i) j = lem j i
+    where
+    lem : Ω→ g .fst (σΣA north) ∙ Ω→ f .fst (σΣA north)
+       ≡ refl
+    lem = cong₂ _∙_ Ω→g∙ Ω→f∙
+        ∙ sym (rUnit refl)
+
+-- Right bilinearity of generalised whitehead product
+module _ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
+  (B : Pointed ℓ') {C : Pointed ℓ''}
+  (f : Susp∙ (typ A) →∙ C)
+  (g h : Susp∙ (Susp (typ B)) →∙ C) where
+  private
+    σΣB = σ (Susp∙ (typ B))
+    Ω→f∙ = cong (Ω→ f .fst) (rCancel (merid (pt A))) ∙ Ω→ f .snd
+    Ω→g∙ = cong (Ω→ g .fst) (rCancel (merid north)) ∙ Ω→ g .snd
+    Ω→h∙ = cong (Ω→ h .fst) (rCancel (merid north)) ∙ Ω→ h .snd
+
+  WhiteheadProdBilinᵣ : ·wh A (Susp∙ (typ B)) f (·Susp (Susp∙ (typ B)) g h)
+                     ≡ ·wh A (Susp∙ (typ B)) f g +* ·wh A (Susp∙ (typ B)) f h
+  fst (WhiteheadProdBilinᵣ i) (inl x) = Ω→ f .fst (σ A x) i
+  fst (WhiteheadProdBilinᵣ i) (inr x) =
+    (Ω→ h .fst (σΣB x) ∙ Ω→ g .fst (σΣB x)) (~ i)
+  fst (WhiteheadProdBilinᵣ i) (push a b j) = main i j
+    where
+    x = Ω→ f .fst (σ A a)
+    y = Ω→ g .fst (σΣB b)
+    z = Ω→ h .fst (σΣB b)
+
+    fun1 fun2 : Susp∙ (typ B) →∙ Ω C
+    fst fun1 b = x ∙ Ω→ g .fst (σΣB b) ⁻¹ ∙ x ⁻¹
+    snd fun1 = cong₂ _∙_ refl (cong₂ _∙_ (cong sym Ω→g∙) refl
+                             ∙ sym (lUnit _))
+             ∙ rCancel _
+    fun2 = Ω→ h ∘∙ (σΣB , rCancel (merid north))
+
+    main : Square (cong (·wh A (Susp∙ (typ B)) f
+                        (·Susp (Susp∙ (typ B)) g h) .fst) (push a b))
+                  (cong ((·wh A (Susp∙ (typ B)) f g
+                       +* ·wh A (Susp∙ (typ B)) f h) .fst) (push a b))
+                  x ((z ∙ y) ⁻¹)
+    main = cong₂ _∙_ (·Suspσ' g h b) refl
+         ∙ sym (assoc y z x)
+         ∙ (λ _ → y ∙ (z ∙ x))
+         ◁ doubleCompPath-filler (x ⁻¹) (y ∙ (z ∙ x)) ((z ∙ y) ⁻¹)
+        ▷ (doubleCompPath≡compPath _ _ _
+         ∙ cong (x ⁻¹ ∙_) (sym (assoc _ _ _)
+           ∙ cong₂ _∙_ refl (cong₂ _∙_ refl (symDistr z y)
+                          ∙ assoc _ _ _ ∙ cong₂ _∙_ (sym (assoc z x _)) refl))
+         ∙ assoc _ _ _
+         ∙ cong₂ _∙_ refl
+            ((cong₂ _∙_ refl (lUnit _
+                           ∙ cong (_∙ z ⁻¹) (sym (lCancel x))
+                           ∙ sym (assoc _ _ _))
+           ∙ (assoc _ _ _))
+           ∙ cong₂ _∙_ ((sym (assoc _ _ _) ∙ cong₂ _∙_ refl (sym (assoc _ _ _)))
+                      ∙ sym (funExt⁻ (cong fst (Susp·→Ωcomm B fun1 fun2)) b))
+                       refl
+           ∙ sym (assoc _ _ _))
+         ∙ assoc _ _ _
+         ∙ cong₂ _∙_ (cong ((x ⁻¹ ∙ y) ∙_) (assoc _ _ _)
+                   ∙ assoc _ _ _) refl
+         ∙ sym (assoc _ _ _)
+         ∙ sym (cong₂ _∙_
+                 (sym (rUnit _)
+                 ∙ cong·wh-ℓ* f g a b
+                 ∙ doubleCompPath≡compPath _ _ _
+                 ∙  (assoc _ _ _)
+                  ∙ cong (_∙ y ⁻¹) (assoc _ _ _)
+                  ∙ sym (assoc _ _ _))
+                 (sym (rUnit _)
+                 ∙ cong·wh-ℓ* f h a b
+                 ∙ doubleCompPath≡compPath _ _ _
+                 ∙ cong (x ⁻¹ ∙_) (sym (assoc _ _ _)
+                 ∙ refl))))
+  snd (WhiteheadProdBilinᵣ i) j = Ω→f∙ j i
+
+WhiteheadProdIdL : ∀ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
+         (B : Pointed ℓ') {C : Pointed ℓ''}
+         (f : Susp∙ (typ B) →∙ C)
+      → ·wh A B (const∙ _ _) f ≡ const∙ _ _
+fst (WhiteheadProdIdL A B {C = C} f i) (inl x) = pt C
+fst (WhiteheadProdIdL A B f i) (inr x) = Ω→ f .fst (σ B x) (~ i)
+fst (WhiteheadProdIdL A B f i) (push a b j) = lem i j
+  where
+  lem : Square (Ω→ f .fst (σ B b) ∙ refl ∙ refl) refl
+                refl (sym (Ω→ f .fst (σ B b)))
+  lem = (cong₂ _∙_  refl (sym (rUnit refl)) ∙ sym (rUnit _))
+         ◁ λ i j → (Ω→ f .fst (σ B b) (~ i ∧ j))
+snd (WhiteheadProdIdL A B f i) = refl
+
+WhiteheadProdIdR : ∀ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
+         (B : Pointed ℓ') {C : Pointed ℓ''}
+         (f : Susp∙ (typ A) →∙ C)
+      → ·wh A B f (const∙ _ _) ≡ const∙ _ _
+fst (WhiteheadProdIdR A B f i) (inl x) = Ω→ f .fst (σ A x) i
+fst (WhiteheadProdIdR A B {C = C} f i) (inr x) = pt C
+fst (WhiteheadProdIdR A B f i) (push a b j) = lem i j
+  where
+  lem : Square ((refl ∙ refl) ∙ Ω→ f .fst (σ A a)) refl
+               (Ω→ f .fst (σ A a)) refl
+  lem = (cong₂ _∙_ (sym (rUnit refl)) refl ∙ sym (lUnit _))
+         ◁ λ i j → (Ω→ f .fst (σ A a) (i ∨ j))
+snd (WhiteheadProdIdR A B f i) j =
+  (cong (Ω→ f .fst) (rCancel (merid (pt A))) ∙ Ω→ f .snd) j i
+
+-- inversion distributes over the generalised Whitehead product
+-*DistrWhitehead : ∀ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
+           (B : Pointed ℓ') {C : Pointed ℓ''}
+           (f : Susp∙ (Susp (typ A)) →∙ C)
+           (g : Susp∙ (typ B) →∙ C)
+      → -* (·wh (Susp∙ (typ A)) B f g)
+      ≡ ·wh (Susp∙ (typ A)) B (-Susp (_ , north) f) g
+-*DistrWhitehead A B f g = sym (+*IdL _)
+  ∙∙ cong (_+* (-* lhs)) (sym -*DistrWhiteheadLem)
+  ∙∙ (sym (+*Assoc _ _ _)
+  ∙ cong (rhs +*_) (+*InvR lhs)
+  ∙ +*IdR rhs)
+  where
+  lhs = ·wh (Susp∙ (typ A)) B f g
+  rhs = ·wh (Susp∙ (typ A)) B (-Susp (_ , north) f) g
+
+  -*DistrWhiteheadLem : rhs +* lhs ≡ const∙ _ _
+  -*DistrWhiteheadLem =
+      sym (WhiteheadProdBilinₗ A B _ f g)
+    ∙ cong₂ (·wh (Susp∙ (typ A)) B) (·SuspInvL (_ , north) f) refl --
+    ∙ WhiteheadProdIdL _ _ g --
+
+-- Inversion is compatible with the equivalence A * B ≃ B * A
+-*Swap : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'}
+      {C : Pointed ℓ''} (f : join∙ A B →∙ C)
+   → -* (f ∘∙ join-commFun∙) ≡ ((-* f) ∘∙ join-commFun∙)
+fst (-*Swap {C = C} f i) (inl x) = pt C
+fst (-*Swap {C = C} f i) (inr x) = pt C
+fst (-*Swap {A = A} {B = B} f i) (push b a j) = main i j
+  where
+  main : (Ω→ (f ∘∙ join-commFun∙) .fst (ℓ* B A b a)) ⁻¹
+       ≡ (Ω→ f .fst (ℓ* A B a b))
+  main = cong sym (Ω→∘ f join-commFun∙ (ℓ* B A b a)
+           ∙ cong (Ω→ f .fst)
+                  (cong₃ _∙∙_∙∙_ refl
+                         (cong-∙ (fst join-commFun∙) _ _
+                       ∙ cong₂ _∙_ refl
+                           (cong-∙∙ (fst join-commFun∙) _ _ _))
+                         refl
+                ∙ doubleCompPath≡compPath _ _ _
+                ∙ assoc _ _ _
+                ∙ cong (_∙ push (pt (fst A , snd A)) (pt (fst B , snd B)) ⁻¹)
+                       (assoc _ _ _
+                     ∙ cong₂ _∙_ (rCancel _) refl
+                     ∙ sym (lUnit _))))
+      ∙ cong (Ω→ f .fst) (symDistr _ _)
+snd (-*Swap {A = A} {B = B} f i) =
+   (sym (rUnit _)
+  ∙ cong (Ω→ f .fst) (ℓ*IdL A B (pt B)) ∙ Ω→ f .snd) (~ i)
+
+{-
+`Anti-commutativity' of generalised whitehead products:
+                       [f ∶ g]
+(Susp A) * (Susp B) ------------------> C
+         |                              |
+         |                              |
+         |                              |
+    flip |                              | id
+         |                              |
+         v                              v
+(Susp B) * (Susp A) ------------------> C
+                       [g ∶ f]
+-}
+module _ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
+         (B : Pointed ℓ') {C : Pointed ℓ''}
+         (f : Susp∙ (Susp (typ A)) →∙ C)
+         (g : Susp∙ (Susp (typ B)) →∙ C)
+  where
+  private
+    σΣA = σ (Susp∙ (typ A))
+    σΣB = σ (Susp∙ (typ B))
+
+    Ω→f∙ = cong (Ω→ f .fst) (rCancel (merid north)) ∙ Ω→ f .snd
+    Ω→g∙ = cong (Ω→ g .fst) (rCancel (merid north)) ∙ Ω→ g .snd
+    Ω→-g∙ =
+        cong (Ω→ (-Susp (Susp∙ (typ B)) g) .fst) (rCancel (merid north))
+      ∙ Ω→ (-Susp (Susp∙ (typ B)) g) .snd
+
+    wh' : join∙ (Susp∙ (typ A)) (Susp∙ (typ B)) →∙ C
+    wh' = ·wh (Susp∙ (typ B)) (Susp∙ (typ A)) (-Susp _ g) f
+                           ∘∙ (Iso.fun join-comm , push north north ⁻¹)
+
+    -- equivalent statement (easier to prove)
+    anticomm : -* (·wh (Susp∙ (typ A)) (Susp∙ (typ B)) f g)
+             ≡  (·wh (Susp∙ (typ B)) (Susp∙ (typ A))
+                     (-Susp (Susp∙ (typ B)) g) f
+              ∘∙ join-commFun∙)
+    fst (anticomm i) (inl x) = Ω→ f .fst (σΣA x) i
+    fst (anticomm i) (inr x) = Ω→ g .fst (σΣB x) i
+    fst (anticomm i) (push a b i₁) = l i i₁
+      where
+      x = Ω→ f .fst (σΣA a)
+      y = Ω→ g .fst (σΣB b)
+
+      fun1 fun2 : Susp∙ (typ A) →∙ Ω C
+      fst fun1 a = y ∙ (Ω→ f .fst (σΣA a) ⁻¹) ∙ y ⁻¹
+      snd fun1 =
+        cong (y ∙_)
+          (cong (_∙ y ⁻¹)
+            (cong sym ((Ω→ f ∘∙ toSuspPointed _) .snd))
+                      ∙ sym (lUnit _) )
+        ∙ rCancel y
+      fun2 = Ω→ f ∘∙ toSuspPointed _
+
+      l : Square (cong (fst (-* ((·wh (Susp∙ (typ A))
+                                      (Susp∙ (typ B)) f g))))
+                                      (push a b))
+                 (cong (fst wh') (push a b))
+                 x y
+      l = sym (rUnit _)
+        ∙ cong sym (cong·wh-ℓ* f g a b)
+        ∙ cong₃ _∙∙_∙∙_ refl (symDistr _ _) refl
+        ∙ doubleCompPath≡compPath _ _ _
+        ∙ assoc _ _ _
+        ∙ (λ i → fst (Susp·→Ωcomm _ fun1 fun2 i) a)
+        ∙ cong (x ∙_) (assoc _ _ _)
+        ∙ sym (doubleCompPath≡compPath _ _ _)
+        ◁ symP (doubleCompPath-filler x (y ∙ x ⁻¹) (y ⁻¹))
+        ▷ cong (_∙ x ⁻¹) (cong sym (sym
+                 (cong-∙ (fst (-Susp (Susp (typ B) , north) g))
+                   (merid b)
+                   (sym (merid north))
+              ∙ cong₂ _∙_ refl Ω→g∙ ∙ sym (rUnit _)) ∙ rUnit _))
+        ∙ compPath≡compPath' _ _
+    snd (anticomm i) j = lem i j
+      where
+      lem : Square refl (snd wh') (Ω→ f .fst (σΣA north)) refl
+      lem = flipSquare Ω→f∙
+          ▷ (cong sym (rUnit refl ∙ cong₂ _∙_ (sym Ω→f∙) (sym (Ω→-g∙)))
+           ∙ rUnit _)
+
+  WhiteheadProdComm : ·wh (Susp∙ (typ A)) (Susp∙ (typ B)) f g
+                   ≡ (·wh (Susp∙ (typ B)) (Susp∙ (typ A)) g f ∘∙ join-commFun∙)
+  WhiteheadProdComm =
+       preWhiteheadProdComm
+     ∙ cong₂ _∘∙_ (-*DistrWhitehead _ _ (-Susp (Susp∙ (typ B)) g) f
+                  ∙ cong₂ (·wh (Susp∙ (typ B)) (Susp∙ (typ A)))
+                          (-Susp² (Susp∙ (typ B)) g)
+                          refl)
+                  refl
+    where
+    preWhiteheadProdComm : ·wh (Susp∙ (typ A)) (Susp∙ (typ B)) f g
+                       ≡ (-* (·wh (Susp∙ (typ B)) (Susp∙ (typ A))
+                                  (-Susp (Susp∙ (typ B)) g) f)
+                        ∘∙ join-commFun∙)
+    preWhiteheadProdComm = sym (-*² _) ∙ cong -* anticomm ∙ -*Swap _
+
+WhiteheadProdComm' : ∀ {ℓ ℓ' ℓ''} {C : Pointed ℓ''}
+   (A A' : Pointed ℓ) (eA : A ≃∙ Susp∙ (typ A')) (B B' : Pointed ℓ')
+
+                   (eB : B ≃∙ Susp∙ (typ B'))
+                   (f : _ →∙ C) (g : _ →∙ C)
+  → ·wh A B f g ≡ (·wh B A g f ∘∙ join-commFun∙)
+WhiteheadProdComm' {C = C} A A' =
+  Equiv∙J (λ A _ →  (B B' : Pointed _)
+
+                   (eB : B ≃∙ Susp∙ (typ B'))
+                   (f : _ →∙ C) (g : _ →∙ C)
+                   → ·wh A B f g ≡ (·wh B A g f ∘∙ join-commFun∙))
+    λ B B' → Equiv∙J (λ B _ → (f : _ →∙ C) (g : _ →∙ C)
+                   → ·wh (Susp∙ (typ A')) B f g
+                   ≡ (·wh B (Susp∙ (typ A')) g f ∘∙ join-commFun∙))
+     (WhiteheadProdComm _ _)
+
+  -- (right derivator) version of the Jacobi identity. This
+  -- corresponds to the statement [f,[g,h]] = [[f,g],h] + [g,[f,h]]
+
+-- We need some 'correction functoins' to make the theorem well-typed
+module _ {ℓ ℓ' ℓ'' : Level} (A : Pointed ℓ) (B : Pointed ℓ') (C : Pointed ℓ'') where
+  Jcorrection₁ : join∙ A (B ⋀∙ C) →∙ join∙ (A ⋀∙ B) C
+  fst Jcorrection₁ =
+    ≃∙map (invEquiv∙ (permute⋀Join≃∙ A B C)) .fst
+  snd Jcorrection₁ = sym (push (inl tt) (pt C))
+
+  Jcorrection₁⁻ : join∙ (A ⋀∙ B) C →∙ join∙ A (B ⋀∙ C)
+  Jcorrection₁⁻ = ≃∙map (permute⋀Join≃∙ A B C)
+
+Jcorrection₂ : ∀ {ℓ ℓ' ℓ'' : Level} (A : Pointed ℓ) (B : Pointed ℓ') (C : Pointed ℓ'')
+  → join∙ A (B ⋀∙ C) →∙ join∙ B (A ⋀∙ C)
+Jcorrection₂ A B C = Jcorrection₁⁻ B A C
+           ∘∙ ((join→ ⋀comm→ (idfun _) , refl)
+           ∘∙ Jcorrection₁ A B C)
+
+module _ {ℓ ℓ' ℓ'' ℓ'''} (A : Pointed ℓ)
+         (B : Pointed ℓ') (C : Pointed ℓ'') {D : Pointed ℓ'''}
+         (f : Susp∙ (Susp (typ A)) →∙ D)
+         (g : Susp∙ (Susp (typ B)) →∙ D)
+         (h : Susp∙ (Susp (typ C)) →∙ D)
+  where
+  -- To state the theorem, we make some abbreviations
+  private
+    σΣA = σ (Susp∙ (typ A))
+    σΣB = σ (Susp∙ (typ B))
+    σΣC = σ (Susp∙ (typ C))
+
+    whAB  = ·wh (Susp∙ (typ A)) (Susp∙ (typ B)) {D}
+
+    whAC  = ·wh (Susp∙ (typ A)) (Susp∙ (typ C)) {D}
+    whBC  = ·wh (Susp∙ (typ B)) (Susp∙ (typ C)) {D}
+
+    whA-BC = ·wh (Susp∙ (typ A)) ((Susp∙ (typ B)) ⋀∙ (Susp∙ (typ C))) {D}
+    whAB-C = ·wh ((Susp∙ (typ A)) ⋀∙ (Susp∙ (typ B))) (Susp∙ (typ C)) {D}
+
+    whB-AC = ·wh (Susp∙ (typ B)) ((Susp∙ (typ A)) ⋀∙ (Susp∙ (typ C))) {D}
+
+
+    whB-CA = ·wh (Susp∙ (typ B)) ((Susp∙ (typ C)) ⋀∙ (Susp∙ (typ A))) {D}
+
+    ΣB*ΣC→Σ[B⋀C] = Join→SuspSmash∙ (Susp∙ (typ B)) (Susp∙ (typ C))
+    Σ[B⋀C]→ΣB*ΣC = SuspSmash→Join∙ (Susp∙ (typ B)) (Susp∙ (typ C))
+
+    Σ[A⋀B]→ΣA*ΣB = SuspSmash→Join∙ (Susp∙ (typ A)) (Susp∙ (typ B))
+    Σ[A⋀C]→ΣA*ΣC = SuspSmash→Join∙ (Susp∙ (typ A)) (Susp∙ (typ C))
+
+    whB∧C = ·wh (Susp∙ (typ B)) (Susp∙ (typ C)) {D}
+
+    Ω→f∙ = cong (Ω→ f .fst) (rCancel (merid north)) ∙ Ω→ f .snd
+    Ω→g∙ = cong (Ω→ g .fst) (rCancel (merid north)) ∙ Ω→ g .snd
+    Ω→h∙ = cong (Ω→ h .fst) (rCancel (merid north)) ∙ Ω→ h .snd
+
+  -- We need some 'correction functoins' to make the theorem well-typed
+  correction₁ = Jcorrection₁ (Susp∙ (typ A)) (Susp∙ (typ B)) (Susp∙ (typ C))
+
+  correction₁⁻ = Jcorrection₁⁻ (Susp∙ (typ A)) (Susp∙ (typ B)) (Susp∙ (typ C))
+
+  correction₂ = Jcorrection₂ (Susp∙ (typ A)) (Susp∙ (typ B)) (Susp∙ (typ C))
+
+  -- Main result
+  JacobiR : whA-BC f (whBC g h ∘∙ Σ[B⋀C]→ΣB*ΣC)
+        ≡ ((whAB-C (whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) h ∘∙ correction₁)
+        +* (whB-AC g (whAC f h ∘∙ Σ[A⋀C]→ΣA*ΣC) ∘∙ correction₂))
+  JacobiR =
+
+    ΣPathP ((funExt (λ { (inl x) → lp x
+                       ; (inr x) → rp x
+                       ; (push a b i) j → main a b j i
+                       }))
+          , flipSquare (Iso.inv ΩSuspAdjointIso f .snd))
+    where
+    L = whA-BC f (whBC g h ∘∙ Σ[B⋀C]→ΣB*ΣC)
+    R = ((whAB-C (whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) h ∘∙ correction₁)
+        +* (whB-AC g (whAC f h ∘∙ Σ[A⋀C]→ΣA*ΣC) ∘∙ correction₂))
+
+    -- The identites on point constructors.
+    lp : Susp (typ A) → Ω D .fst
+    lp = Iso.inv ΩSuspAdjointIso f .fst
+
+    rp : (Susp∙ (typ B) ⋀ Susp∙ (typ C)) → Ω D .fst
+    rp = rp' ∘ ⋀→Smash
+      where
+      rpl : ∀ {ℓ} {A : Type ℓ} {x : A} (p q : x ≡ x)
+        → refl ≡ q
+        → (p ∙ q ⁻¹) ∙ p ⁻¹ ∙ q ≡ refl
+      rpl p = J> cong₂ _∙_ (sym (rUnit p)) (sym (rUnit _)) ∙ rCancel p
+
+      rpr : ∀ {ℓ} {A : Type ℓ} {x : A} (q : x ≡ x) (p : x ≡ x)
+        → refl ≡ p
+        → (p ∙ q ⁻¹) ∙ p ⁻¹ ∙ q ≡ refl
+      rpr q = J> cong₂ _∙_ (sym (lUnit _)) (sym (lUnit _)) ∙ lCancel q
+
+      rp' : Smash (Susp∙ (typ B)) (Susp∙ (typ C)) → Ω D .fst
+      rp' basel = refl
+      rp' baser = refl
+      rp' (proj b c) = ((Ω→ g .fst (σΣB b) ∙ (Ω→ h .fst (σΣC c)) ⁻¹)
+                     ∙ ((Ω→ g .fst (σΣB b)) ⁻¹ ∙ Ω→ h .fst (σΣC c))) ⁻¹
+      rp' (gluel b i) =
+        sym (rpl (Ω→ g .fst (σΣB b)) (Ω→ h .fst (σΣC north))
+                 (sym (Iso.inv ΩSuspAdjointIso h .snd)) i)
+      rp' (gluer c i) =
+        sym (rpr (Ω→ h .fst (σΣC c)) (Ω→ g .fst (σΣB north))
+                 (sym (Iso.inv ΩSuspAdjointIso g .snd)) i)
+
+    apL apR : (a : Susp (typ A))
+            → Susp∙ (typ B) ⋀ Susp∙ (typ C) → Ω D .fst
+    apL a x = lp a ⁻¹ ∙∙ cong (fst L) (push a x) ∙∙ rp x
+    apR a x = cong (fst R) (push a x)
+
+    -- Some lemmas simplying the pointed functions involved
+    lem1 : whBC g h ∘∙ Σ[B⋀C]→ΣB*ΣC ≡ (fst (whBC g h ∘∙ Σ[B⋀C]→ΣB*ΣC) , refl)
+    lem1 = ΣPathP (refl , sym (rUnit _)
+                  ∙ cong₃ _∙∙_∙∙_
+                          (cong sym (Iso.inv ΩSuspAdjointIso g .snd))
+                          (cong sym (Iso.inv ΩSuspAdjointIso h .snd))
+                          refl
+                        ∙ sym (rUnit refl))
+
+    lem2 : whAB-C (whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) h ∘∙ correction₁
+      ≡ ((whAB-C (whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) h ∘∙ correction₁) .fst , refl)
+    lem2 = ΣPathP (refl
+      , sym (rUnit _)
+      ∙ cong₃ _∙∙_∙∙_ refl
+              (cong sym (Iso.inv ΩSuspAdjointIso h .snd))
+              refl
+     ∙ sym (compPath≡compPath' _ _)
+     ∙ cong sym (sym (rUnit _))
+     ∙ cong₃ _∙∙_∙∙_ refl
+                     (cong (cong (fst (whAB f g) ∘ fst Σ[A⋀B]→ΣA*ΣB))
+                           (cong sym (rCancel (merid (inl tt)))))
+                     refl
+     ∙ ∙∙lCancel _)
+
+    lem3 : whB-AC g (whAC f h ∘∙ Σ[A⋀C]→ΣA*ΣC) ∘∙ correction₂
+        ≡ ((whB-AC g (whAC f h ∘∙ Σ[A⋀C]→ΣA*ΣC) ∘∙ correction₂) .fst , refl)
+    lem3 = ΣPathP (refl
+      , cong₂ _∙_ (cong (cong (fst (whB-AC g (whAC f h ∘∙ Σ[A⋀C]→ΣA*ΣC)))) lem)
+                  refl
+                 ∙ sym (rUnit refl))
+      where
+      lem : snd correction₂ ≡ refl
+      lem = cong₂ _∙_ (cong (cong (fst (Jcorrection₁⁻ (Susp∙ (typ B)) (Susp∙ (typ A)) (Susp∙ (typ C)))))
+                      (sym (rUnit _))) refl
+          ∙ rCancel _
+
+
+    -- some more abbreviations
+    l : Susp (typ A) → Ω D .fst
+    m : Susp (typ B) → Ω D .fst
+    r : Susp (typ C) → Ω D .fst
+    l a = Ω→ f .fst (σΣA a)
+    m b = Ω→ g .fst (σΣB b)
+    r c = Ω→ h .fst (σΣC c)
+
+    -- Goal: relate 'cong (fst L) (push a (inr (b , c))))' to 'cong
+    -- (fst R) (push a (inr (b , c))))' Unfolding definitions this
+    -- gives rise to a word problem.  We could hope to automate some
+    -- parts of the proof in the future...
+    module _ (a : Susp (typ A)) (b : Susp (typ B)) (c : Susp (typ C)) where
+      leftId : (cong (fst L) (push a (inr (b , c))))
+             ≡ ((m b ⁻¹) ∙∙ r c ∙ m b ∙∙ (r c ⁻¹)) ∙ l a
+      leftId =
+        cong₂ _∙_ ((λ j i → Ω→ (lem1 j) .fst
+                                  (σ (Susp∙ (typ B) ⋀∙ Susp∙ (typ C))
+                                     (inr (b , c))) i)
+        ∙ sym (rUnit _)
+        ∙ cong (cong (fst (whBC g h)))
+               (cong-∙ (fst Σ[B⋀C]→ΣB*ΣC)
+                       (merid (inr (b , c))) (sym (merid (inl tt))))
+        ∙ cong-∙ (fst (whBC g h)) _ _
+        ∙ cong₂ _∙_ (cong-∙∙ (fst (whBC g h)) _ _ _
+                ∙ cong₃ _∙∙_∙∙_
+                     (cong sym (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso h .snd) refl
+                     ∙ sym (lUnit _)))
+                     (λ i → Ω→ h .fst (σΣC c) ∙ Ω→ g .fst (σΣB b))
+                     (cong sym (cong₂ _∙_ refl (Iso.inv ΩSuspAdjointIso g .snd)
+                             ∙ sym (rUnit _)))
+                ∙ refl)
+             (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso h .snd)
+                        (Iso.inv ΩSuspAdjointIso g .snd) ∙ sym (rUnit refl))
+        ∙ sym (rUnit ((m b ⁻¹) ∙∙ r c ∙ m b ∙∙ (r c ⁻¹))))
+        refl
+
+      -- more abbreviations
+      ℓA-BC =  ℓ* (Susp∙ (typ A)) ((Susp∙ (typ B)) ⋀∙ (Susp∙ (typ C)))
+      ℓAB-C =  ℓ* ((Susp∙ (typ A)) ⋀∙ (Susp∙ (typ B))) (Susp∙ (typ C))
+      ℓB-AC =  ℓ* (Susp∙ (typ B)) ((Susp∙ (typ A)) ⋀∙ (Susp∙ (typ C)))
+
+      correction₁-ℓ : cong (fst (correction₁)) (ℓA-BC a (inr (b , c)))
+                    ≡ (push (inl tt) north) ⁻¹
+                    ∙∙ ℓAB-C (inr (a , b)) c
+                    ∙∙ push (inl tt) north
+      correction₁-ℓ = cong-∙ (fst (correction₁)) _ _
+                   ∙ cong (sym (push (inl tt) north) ∙_)
+                          (cong-∙∙ (fst (correction₁)) _ _ _
+                          ∙ doubleCompPath≡compPath _ _ _ ∙ refl)
+                   ∙ assoc _ _ _
+                   ∙ cong₂ _∙_ (rCancel _) refl
+                   ∙ sym (lUnit _)
+                   ∙ cong₂ _∙_ (lUnit _
+                             ∙ (λ i → (λ j → push (inl tt) north (~ j ∨ ~ i))
+                                     ∙ compPath-filler' (push (inl tt) north)
+                                             (push (inr (a , b)) north ⁻¹
+                                             ∙∙ push (inr (a , b)) c
+                                             ∙∙ push (inl tt) c ⁻¹) i))
+                             ((λ i → push (inl tt) c
+                                   ∙∙ push (push (inr b) (~ i)) c ⁻¹
+                                   ∙∙ push (push (inr b) (~ i)) north)
+                             ∙ doubleCompPath≡compPath _ _ _
+                             ∙ assoc _ _ _
+                             ∙ cong₂ _∙_ (rCancel _) refl
+                             ∙ sym (lUnit _))
+                   ∙ sym (assoc _ _ _)
+                   ∙ sym (doubleCompPath≡compPath _ _ _)
+
+
+      correction₂-ℓ : cong (fst correction₂) (ℓA-BC a (inr (b , c)))
+                    ≡ ℓB-AC b (inr (a , c))
+      correction₂-ℓ =
+          cong-∙ (fst correction₂) _ _
+        ∙ cong₂ _∙_ refl
+                    (cong-∙∙ (fst correction₂) _ _ _
+                  ∙ (cong₃ _∙∙_∙∙_ (λ _ → push north (inl tt) ⁻¹)
+                  (help a b c)
+                  (cong sym (help north b c
+                            ∙ cong₂ _∙_ (cong (ℓB-AC b) (sym (push (inr c)))
+                                      ∙ ℓ*IdR _ _ b) refl
+                            ∙ sym (lUnit _)))
+                ∙ doubleCompPath≡compPath _ _ _
+                ∙ cong (push north (inl tt) ⁻¹ ∙_)
+                       (sym (assoc _ _ _)
+                       ∙ (cong (ℓB-AC b (inr (a , c)) ∙_) (rCancel _)
+                       ∙ sym (rUnit _)))
+                ∙ assoc _ _ _
+                ∙ cong₂ _∙_ (rCancel _) refl
+                ∙ sym (lUnit _)))
+
+        where
+        help : (a : _) (b : _) (c : _)
+             → cong (fst correction₂) (push a (inr (b , c)))
+              ≡ ℓB-AC b (inr (a , c)) ∙ push north (inl tt)
+        help a b c =
+          cong-∙∙ ((Jcorrection₁⁻
+                    (Susp∙ (typ B)) (Susp∙ (typ A)) (Susp∙ (typ C))) .fst
+                  ∘ join→ ⋀comm→ (idfun (Susp (typ C)))) _ _ _
+          ∙ cong₃ _∙∙_∙∙_ ((λ i → push north (push (inl a) (~ i))
+                                ∙∙ push b (push (inl a) (~ i)) ⁻¹
+                                ∙∙ push b (inl tt))
+                        ∙ doubleCompPath≡compPath _ _ _
+                        ∙ cong₂ _∙_ refl (lCancel (push b (inl tt)))
+                        ∙ sym (rUnit _))
+                        refl (λ _ → push north (inl tt))
+          ∙ doubleCompPath≡compPath _ _ _ ∙ assoc _ _ _
+
+      -- more abbreviations...
+      x = l a
+      -x = x ⁻¹
+      y = m b
+      -y = y ⁻¹
+      z = r c
+      -z = z ⁻¹
+
+      t₁ = (y ∙ -x ∙ -y ∙ x) ∙ z ∙ -x ∙ y ∙ x ∙ -y
+      t₂ = -y ∙ -x ∙ z ∙ x ∙ -z ∙ y
+      t₃ = z ∙ -x ∙ -z ∙ x
+
+      t₃' = -x ∙ -z ∙ x
+      t₄ = z ∙ x ∙ -z
+
+      fA : Susp∙ (typ A) →∙ Ω D
+      fst fA a = ((-y ∙ z) ∙ Ω→ f .fst (σΣA a)
+               ∙ -z ∙ sym (Ω→ f .fst (σΣA a))) ∙ y
+      snd fA = cong (λ x → ((-y ∙ z) ∙ x ∙ -z ∙ x ⁻¹) ∙ y)
+                    (Iso.inv ΩSuspAdjointIso f .snd)
+             ∙ cong₂ _∙_ (cong₂ _∙_ refl (sym (lUnit _) ∙ sym (rUnit _))
+                       ∙ sym (assoc -y z -z)
+                       ∙ cong (-y ∙_) (rCancel z) ∙ sym (rUnit -y))
+                       refl
+             ∙ lCancel y
+
+      f-xyx f-xyx' f-zyz : Susp∙ (typ B) →∙ Ω D
+      fst f-xyx b = -x ∙ Ω→ g .fst (σΣB b) ⁻¹ ∙ x
+      snd f-xyx = cong₂ _∙_ refl
+        (cong (_∙ x) (cong sym (Iso.inv ΩSuspAdjointIso g .snd))
+          ∙ sym (lUnit x)) ∙ lCancel x
+      fst f-xyx' b = -x ∙ Ω→ g .fst (σΣB b) ∙ x
+      snd f-xyx' =
+        cong₂ _∙_ refl
+        (cong (_∙ x) (Iso.inv ΩSuspAdjointIso g .snd)
+          ∙ sym (lUnit x)) ∙ lCancel x
+      fst f-zyz b = -z ∙ Ω→ g .fst (σΣB b) ⁻¹ ∙ z
+      snd f-zyz = cong₂ _∙_ refl
+        (cong (_∙ z) (cong sym (Iso.inv ΩSuspAdjointIso g .snd))
+          ∙ sym (lUnit z))
+          ∙ lCancel z
+
+      f₁ f₂ fz f₃ f-yazay : Susp∙ (typ C) →∙ Ω D
+      fst f₁ z = (y ∙ -x ∙ -y ∙ x) ∙ Ω→ h .fst (σΣC z) ∙ -x ∙ y ∙ x ∙ -y
+      snd f₁ =
+        cong₂ _∙_
+          (assoc _ _ _ ∙ assoc _ _ _)
+          ((cong₂ _∙_ (Iso.inv ΩSuspAdjointIso h .snd) refl
+                     ∙ sym (lUnit _))
+          ∙ sym (symDistr _ _
+          ∙ cong₂ _∙_ refl
+             (symDistr _ _ ∙ cong₂ _∙_ refl (symDistr _ _))))
+          ∙ rCancel (((y ∙ -x) ∙ -y) ∙ x)
+      fst f₂ z = -y ∙ -x ∙ Ω→ h .fst (σΣC z) ∙ x ∙ Ω→ h .fst (σΣC z) ⁻¹ ∙ y
+      snd f₂ =
+        cong₂ _∙_ refl
+          (cong₂ _∙_ refl
+            (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso h .snd)
+                       (cong₂ _∙_ refl
+                         (cong₂ _∙_ (cong sym (Iso.inv ΩSuspAdjointIso h .snd))
+                                    refl
+                       ∙ sym (lUnit _)))
+                     ∙ sym (lUnit (x ∙ y))))
+        ∙ cong₂ _∙_ refl (assoc -x x y
+                       ∙ cong₂ _∙_ (lCancel x) refl
+                       ∙ sym (lUnit y))
+                     ∙ lCancel y
+      fz = (sym , refl) ∘∙ Iso.inv ΩSuspAdjointIso h
+      fst f₃ c = -x ∙ sym (Ω→ h .fst (σΣC c)) ∙ x
+      snd f₃ =
+          cong (-x ∙_)
+           (cong (_∙ x) (cong sym (Iso.inv ΩSuspAdjointIso h .snd))
+            ∙ sym (lUnit x))
+        ∙ lCancel x
+      fst f-yazay c = (-y ∙ x) ∙ Ω→ h .fst (σΣC c) ∙ -x ∙ y
+      snd f-yazay =
+        cong₂ _∙_ (sym (symDistr -x y))
+                  (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso h .snd) refl
+                           ∙ sym (lUnit (-x ∙ y)))
+                ∙ lCancel (-x ∙ y)
+
+
+      f₄ fa : Susp∙ (typ A) →∙ Ω D
+      fst f₄ a = z ∙ Ω→ f .fst (σΣA a) ∙ -z
+      snd f₄ = cong (z ∙_) (cong (_∙ -z) (Iso.inv ΩSuspAdjointIso f .snd)
+                          ∙ sym (lUnit _)) ∙ rCancel z
+      fa = (sym , refl) ∘∙ Iso.inv ΩSuspAdjointIso f
+
+      rightId₁ : cong (fst R) (push a (inr (b , c)))
+             ≡ (t₂ ∙ t₁) ∙ -z ∙ t₃
+      rightId₁ =
+        cong₂ _∙_ (λ i → Ω→ (lem2 i) .fst (ℓA-BC a (inr (b , c))))
+                   (λ i → Ω→ (lem3 i) .fst (ℓA-BC a (inr (b , c))))
+        ∙ cong₂ _∙_
+          (sym (rUnit _)
+           ∙ cong (cong (fst (whAB-C (whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) h)))
+                  correction₁-ℓ
+            ∙ cong-∙∙ (fst (whAB-C (whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) h)) _ _ _
+            ∙ cong (λ x → x ⁻¹
+                        ∙∙ cong (fst (whAB-C (whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) h))
+                                (ℓAB-C (inr (a , b)) c)
+                        ∙∙ x) (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso h .snd)
+                                         (Iso.inv ΩSuspAdjointIso
+                                           (whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) .snd)
+                           ∙ sym (rUnit refl))
+                ∙ sym (rUnit _) )
+            (sym (rUnit _)
+           ∙ cong (cong (fst (whB-AC g (whAC f h ∘∙ Σ[A⋀C]→ΣA*ΣC))))
+                             (correction₂-ℓ))
+        ∙ cong₂ _∙_ ((λ i → cong·wh-ℓ* {A = _ , inl tt} {B = _ , north}
+                             (lem4 i) h (inr (a , b)) c i)
+                    ∙ cong₃ _∙∙_∙∙_ (sym (rUnit _)
+                                    ∙ cong sym (fgid' A B f g a b)
+                                    ∙ cong₃ _∙∙_∙∙_ refl
+                                       (symDistr (m b) (l a)) refl)
+                                    (cong₂ _∙_ (λ _ → r c)
+                                      (sym (rUnit _) ∙ (fgid' A B f g a b)))
+                                    (λ _ → r c ⁻¹))
+                    ((λ i → cong·wh-ℓ* {A = _ , north} {B = _ , inl tt}
+                              g (lem5 i) b (inr (a , c)) i)
+                    ∙ cong₃ _∙∙_∙∙_ (λ _ → m b ⁻¹)
+                       (cong₂ _∙_ (sym (rUnit _) ∙ fgid' A C f h a c)
+                                  (λ _ → m b))
+                       (sym (rUnit _)
+                       ∙ cong sym (fgid' A C f h a c)
+                       ∙ cong₃ _∙∙_∙∙_ refl (symDistr (r c) (l a)) refl))
+        ∙ cong₂ _∙_ (cong₃ _∙∙_∙∙_ (doubleCompPath≡compPath _ _ _
+                                    ∙ cong₂ _∙_ refl (sym (assoc _ _ _)))
+                                   (cong (r c ∙_) (doubleCompPath≡compPath _ _ _
+                                    ∙ cong₂ _∙_ refl (sym (assoc _ _ _))))
+                                   refl
+                  ∙ doubleCompPath≡compPath _ _ _
+                ∙ assoc _ _ _ ∙ cong (_∙ -z) λ _ → t₁)
+                  (doubleCompPath≡compPath _ _ _
+                  ∙ cong₂ _∙_ refl
+                    (cong₂ _∙_ (cong (_∙ y)
+                      (doubleCompPath≡compPath _ _ _)
+                        ∙ sym (assoc _ _ y)
+                        ∙ cong (-x ∙_) (sym (assoc _ _ y) ∙ sym (assoc _ _ _)))
+                      ((doubleCompPath≡compPath _ _ _)
+                        ∙ (cong (z ∙_) (sym (assoc -x -z x)))))
+                    ∙ assoc -y _ t₃ ∙ λ _ → t₂ ∙ t₃)
+        ∙ sym (assoc t₁ -z (t₂ ∙ t₃))
+        ∙ cong (t₁ ∙_) (assoc -z t₂ t₃
+                     ∙ cong (_∙ t₃) (funExt⁻ (cong fst (Susp·→Ωcomm C fz f₂)) c)
+                     ∙ sym (assoc t₂ -z t₃))
+        ∙ assoc t₁ t₂ _
+        ∙ cong₂ _∙_ (funExt⁻ (cong fst (Susp·→Ωcomm C f₁ f₂)) c) refl
+        where
+        fgid' : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
+                          (f : Susp∙ (Susp (typ A)) →∙ D)
+                          (g : Susp∙ (Susp (typ B)) →∙ D)
+                          (a : Susp (typ A)) (b : Susp (typ B))
+             → cong (fst (·wh (Susp∙ (typ A)) (Susp∙ (typ B)) f g))
+                   (cong (fst (SuspSmash→Join∙ (Susp∙ (typ A)) (Susp∙ (typ B))))
+                      (σ (_ , inl tt) (inr (a , b))))
+             ≡ (Ω→ f .fst (σ (Susp∙ (typ A)) a) ⁻¹
+             ∙∙ Ω→ g .fst (σ (Susp∙ (typ B)) b)
+              ∙ Ω→ f .fst (σ (Susp∙ (typ A)) a)
+             ∙∙ (Ω→ g .fst (σ (Susp∙ (typ B)) b) ⁻¹))
+        fgid' A B f g a b =
+          cong-∙ (fst (·wh (Susp∙ (typ A)) (Susp∙ (typ B)) f g)
+                 ∘ (fst (SuspSmash→Join∙ (Susp∙ (typ A)) (Susp∙ (typ B)))))
+                   (merid (inr (a , b))) _
+                 ∙ cong₂ _∙_ refl
+                             (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso g .snd)
+                                        (Iso.inv ΩSuspAdjointIso f .snd)
+                            ∙ sym (rUnit refl))
+                           ∙ sym (rUnit _)
+             ∙ cong-∙∙ (fst (·wh (Susp∙ (typ A)) (Susp∙ (typ B)) f g)) _ _ _
+             ∙ cong₃ _∙∙_∙∙_
+                 (cong sym (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso g .snd) refl
+                                      ∙ sym (lUnit _)))
+                 refl
+                 (cong sym (cong₂ _∙_ refl (Iso.inv ΩSuspAdjointIso f .snd)
+                          ∙ sym (rUnit _)))
+
+        lem4 : whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB
+            ≡ ((whAB f g ∘∙ Σ[A⋀B]→ΣA*ΣB) .fst , refl)
+        lem4 =
+          ΣPathP (refl , sym (rUnit _)
+                       ∙ cong sym (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso g .snd)
+                                             (Iso.inv ΩSuspAdjointIso f .snd))
+                      ∙ sym (rUnit _))
+        lem5 : whAC f h ∘∙ Σ[A⋀C]→ΣA*ΣC
+            ≡ ((whAC f h ∘∙ Σ[A⋀C]→ΣA*ΣC) .fst , refl)
+        lem5 =
+          ΣPathP (refl ,  sym (rUnit _)
+                        ∙ cong sym (cong₂ _∙_ (Iso.inv ΩSuspAdjointIso h .snd)
+                                              (Iso.inv ΩSuspAdjointIso f .snd))
+                       ∙ sym (rUnit _))
+
+      rightId₂ : (t₂ ∙ t₁) ∙ -z ∙ t₃
+               ≡ -y ∙ (-x ∙ t₄) ∙ y ∙ t₁ ∙ t₃'
+      rightId₂ = cong₂ _∙_ (cong₂ _∙_ (cong (-y ∙_)
+                                        (cong (-x ∙_)
+                                          (assoc _ _ _ ∙ assoc _ _ _
+                                        ∙ cong₂ _∙_ (sym (assoc z x -z)) refl)))
+                                      refl)
+                       (assoc -z z _
+                      ∙ cong₂ _∙_ (lCancel z) refl ∙ sym (lUnit _))
+               ∙ sym (assoc _ _ _)
+               ∙ cong₂ _∙_ (cong (-y ∙_) (assoc _ _ _)
+                           ∙ assoc _ _ _)
+                           refl
+               ∙ sym (assoc _ _ _)
+               ∙ sym (assoc _ _ _)
+
+      rightId₃ : -y ∙ (-x ∙ t₄) ∙ y ∙ t₁ ∙ t₃'
+               ≡ (-y ∙ z) ∙ (x ∙ -z ∙ -x) ∙ y ∙ t₃' ∙ t₁
+      rightId₃ =
+        cong (-y ∙_)
+          (cong₂ _∙_ (funExt⁻ (cong fst (Susp·→Ωcomm A fa f₄)) a)
+                     (cong (y ∙_) (funExt⁻ (cong fst (Susp·→Ωcomm C f₁ f₃)) c)))
+        ∙ (assoc _ _ _
+         ∙ cong₂ _∙_ (cong (-y ∙_) (sym (assoc _ _ _)
+         ∙ cong (z ∙_) (sym (assoc _ _ _)))
+         ∙ assoc _ _ _) refl)
+        ∙ sym (assoc _ _ _)
+
+      rightId₄ : ((-y ∙ z) ∙ (x ∙ -z ∙ -x) ∙ y ∙ t₃' ∙ t₁)
+                 ∙ (y ∙ -z) ∙ (-y ∙ z)
+               ≡ (((-y ∙ z) ∙ x ∙ -z ∙ -x) ∙ y)
+                 ∙ (-x ∙ (-y ∙ x) ∙ z ∙ -x ∙ y) ∙ -z ∙ x
+      rightId₄ =
+        cong₂ _∙_ (cong (λ t → (-y ∙ z) ∙ (x ∙ -z ∙ -x) ∙ y ∙ t₃' ∙ t) t₁≡)
+                  (sym (assoc y -z _))
+        ∙ sym (assoc _ _ _)
+        ∙ cong₂ _∙_ refl (sym (assoc _ _ _)
+                       ∙ cong₂ _∙_ refl (sym (assoc _ _ _)
+                       ∙ cong₂ _∙_ refl (sym (assoc _ _ _)
+                       ∙ cong₂ _∙_ refl (assoc _ _ _
+                       ∙ cong₂ _∙_ (sym (assoc _ _ _)
+                       ∙ cong₂ _∙_ refl (sym (assoc _ _ _)
+                       ∙ cong (y ∙_) (sym (assoc _ _ _)
+                       ∙ cong (z ∙_) (sym (assoc _ _ _)
+                       ∙ cong₂ _∙_ refl (lCancel y)
+                       ∙ sym (rUnit _))))) refl))))
+        ∙ assoc _ _ _
+        ∙ assoc _ y _
+        ∙ cong₂ _∙_ refl id2
+        where
+        t₁≡ : t₁ ≡ (-x ∙ -y ∙ x) ∙ y ∙ z ∙ (-x ∙ y ∙ x) ∙ -y
+        t₁≡ = cong₂ _∙_
+          (funExt⁻ (cong fst (Susp·→Ωcomm B
+                          (Iso.inv ΩSuspAdjointIso g) f-xyx)) b)
+          (cong (z ∙_) (cong (-x ∙_)
+                         (assoc _ _ _) ∙ assoc _ _ _))
+                     ∙ sym (assoc _ _ _)
+
+        id2 : t₃' ∙ ((-x ∙ -y ∙ x) ∙ y ∙ z ∙ (-x ∙ y ∙ x)) ∙ (-z ∙ -y ∙ z)
+            ≡ (-x ∙ (-y ∙ x) ∙ z ∙ -x ∙ y) ∙ (-z ∙ x)
+        id2 = cong (t₃' ∙_)
+          (cong₂ _∙_ (assoc _ _ _ ∙ assoc _ _ _) refl
+          ∙ sym (assoc _ _ _)
+          ∙ cong₂ _∙_ (sym (assoc _ _ _) ∙ sym (assoc _ _ _))
+                      (funExt⁻ (cong fst (Susp·→Ωcomm B f-xyx' f-zyz)) b)
+          ∙ cong₂ _∙_ (assoc _ _ _) refl
+          ∙ assoc _ _ _
+          ∙ cong₂ _∙_ (cong₂ _∙_ refl
+                  (assoc _ _ _
+                 ∙ cong (_∙ z) (sym (symDistr y z)))
+                 ∙ assoc _ _ _
+                 ∙ cong (_∙ z) (sym (assoc _ _ _)
+                              ∙ cong₂ _∙_ refl (rCancel (y ∙ z))
+                              ∙ sym (rUnit _)))
+                 refl)
+          ∙ assoc _ _ _
+          ∙ cong₂ _∙_ (assoc _ _ _
+                      ∙ cong (_∙ z) (assoc _ -x _
+                        ∙ cong₂ _∙_ (sym (assoc _ _ _)
+                          ∙ cong (-x ∙_) (sym (assoc -z x -x)
+                            ∙ cong (-z ∙_) (rCancel x)
+                              ∙ sym (rUnit -z))) refl)) refl
+          ∙ assoc _ _ _
+          ∙ assoc _ _ _
+          ∙ cong (_∙ x) (sym (assoc _ _ _)
+                       ∙ sym (assoc _ _ _)
+                       ∙ sym (assoc _ _ _)
+                       ∙ sym (assoc -x -z _))
+          ∙ sym (assoc _ _ _)
+          ∙ cong (-x ∙_) (cong (_∙ x)
+                 (funExt⁻ (cong fst (Susp·→Ωcomm C fz f-yazay)) c)
+                 ∙ sym (assoc _ _ _))
+          ∙ assoc -x _ _
+          ∙ cong (_∙ (-z ∙ x)) refl
+
+      rightId₅ : ((((-y ∙ z) ∙ x ∙ -z ∙ -x) ∙ y) ∙ x)
+                  ∙ (-x ∙ (-y ∙ x) ∙ z ∙ -x ∙ y) ∙ -z ∙ x
+               ≡ (-y ∙∙ z ∙ y ∙∙ -z) ∙ x
+      rightId₅ = assoc _ _ _
+               ∙ assoc _ _ _
+               ∙ cong (_∙ x)
+               (cong (_∙ -z) (sym (assoc _ x _)
+               ∙ cong₂ _∙_ refl (assoc x -x _
+                                ∙ cong₂ _∙_ (rCancel x) refl
+                                ∙ sym (lUnit _)
+                                ∙ sym (assoc _ _ _))
+               ∙ sym (assoc _ y _)
+               ∙ cong₂ _∙_ refl (assoc y -y _ ∙ cong₂ _∙_ (rCancel y) refl
+                              ∙ sym (lUnit _))
+               ∙ sym (assoc _ _ _)
+               ∙ cong₂ _∙_ refl (cong₂ _∙_ refl (assoc _ _ _ ∙ assoc _ _ _)
+                              ∙ assoc _ _ _
+                              ∙ cong (_∙ y)
+                                (cong₂ _∙_ refl (sym (symDistr x (-z ∙ -x)
+                                              ∙ cong (_∙ -x) (symDistr -z -x)))
+                                ∙ rCancel (x ∙ -z ∙ -x))
+                                ∙ sym (lUnit y))
+                                ∙ sym (assoc _ _ _))
+               ∙ sym (assoc _ _ _)
+               ∙ sym (doubleCompPath≡compPath _ _ _))
+
+      rightId : x ∙∙ cong (fst R) (push a (inr (b , c)))
+                  ∙∙ ((y ∙ -z) ∙ (-y ∙ z))
+              ≡ (-y ∙∙ z ∙ y ∙∙ -z) ∙ x
+      rightId = cong (x ∙∙_∙∙ (y ∙ -z) ∙ (-y ∙ z))
+                     (rightId₁ ∙ rightId₂
+                    ∙ rightId₃)
+              ∙ doubleCompPath≡compPath _ _ _
+              ∙ cong (x ∙_) (rightId₄ ∙ refl)
+              ∙ assoc _ _ _
+              ∙ cong₂ _∙_ (funExt⁻ (cong fst (Susp·→Ωcomm A
+                                     (Iso.inv ΩSuspAdjointIso f) fA)) a)
+                          refl
+              ∙ rightId₅
+
+      mainId :
+        Square (cong (fst L) (push a (inr (b , c))))
+               (cong (fst R) (push a (inr (b , c))))
+               (lp a) (rp (inr (b , c)))
+      mainId = (leftId ∙ sym rightId)
+            ◁ symP (doubleCompPath-filler
+                     x
+                     (cong (fst R) (push a (inr (b , c))))
+                     ((y ∙ -z) ∙ (-y ∙ z)))
+
+    main : (a : Susp (typ A))
+          (x : Susp∙ (typ B) ⋀ Susp∙ (typ C))
+        → Square (cong (fst L) (push a x))
+                  (cong (fst R) (push a x))
+                  (lp a) (rp x)
+    main a x =
+        doubleCompPath-filler (lp a ⁻¹) (cong (fst L) (push a x)) (rp x)
+      ▷ asFuns a x
+      where
+      asFuns : (a : Susp (typ A))
+             → (x : Susp∙ (typ B) ⋀ Susp∙ (typ C))
+             → apL a x ≡ apR a x
+      asFuns a = funExt⁻ (⋀→Homogeneous≡ (isHomogeneousPath _ _)
+         λ b c → sym (transport (PathP≡doubleCompPathʳ _ _ _ _)
+                      (symP (mainId a b c))))
+
+JacobiR' :
+  ∀ {ℓ ℓ' ℓ'' ℓ'''} {D : Pointed ℓ'''}
+     (A A' : Pointed ℓ) (eA : A ≃∙ Susp∙ (typ A'))
+     (B B' : Pointed ℓ') (eB : B ≃∙ Susp∙ (typ B'))
+     (C C' : Pointed ℓ'') (eC : C ≃∙ Susp∙ (typ C'))
+     (f : Susp∙ (typ A) →∙ D)
+     (g : Susp∙ (typ B) →∙ D)
+     (h : Susp∙ (typ C) →∙ D)
+     → ·wh A (B ⋀∙ C) f (·wh B C g h ∘∙ SuspSmash→Join∙ B C)
+      ≡ (·wh (A ⋀∙ B) C (·wh A B f g ∘∙ SuspSmash→Join∙ A B) h ∘∙ Jcorrection₁ A B C)
+      +* (·wh B (A ⋀∙ C) g (·wh A C f h ∘∙ SuspSmash→Join∙ A C) ∘∙ Jcorrection₂ A B C)
+JacobiR' {D = D} A A' eA B B' eB C C' eC =
+  transport (λ i → (f : Susp∙ (typ (pA i)) →∙ D)
+     (g : Susp∙ (typ (pB i)) →∙ D)
+     (h : Susp∙ (typ (pC i)) →∙ D)
+     → ·wh (pA i) ((pB i) ⋀∙ (pC i)) f (·wh (pB i) (pC i) g h
+                                        ∘∙ SuspSmash→Join∙ (pB i) (pC i))
+      ≡ (·wh ((pA i) ⋀∙ (pB i)) (pC i) (·wh (pA i) (pB i) f g
+                                        ∘∙ SuspSmash→Join∙ (pA i) (pB i)) h
+        ∘∙ Jcorrection₁ (pA i) (pB i) (pC i))
+      +* (·wh (pB i) ((pA i) ⋀∙ (pC i)) g (·wh (pA i) (pC i) f h
+                                           ∘∙ SuspSmash→Join∙ (pA i) (pC i))
+       ∘∙ Jcorrection₂ (pA i) (pB i) (pC i)))
+      (JacobiR A' B' C')
+  where
+  pA = ua∙ (fst eA) (snd eA) ⁻¹
+  pB = ua∙ (fst eB) (snd eB) ⁻¹
+  pC = ua∙ (fst eC) (snd eC) ⁻¹
diff --git a/Cubical/Homotopy/Whitehead.agda b/Cubical/Homotopy/WhiteheadProducts/Properties.agda
similarity index 72%
rename from Cubical/Homotopy/Whitehead.agda
rename to Cubical/Homotopy/WhiteheadProducts/Properties.agda
index fbdffd6ed4..46418044b6 100644
--- a/Cubical/Homotopy/Whitehead.agda
+++ b/Cubical/Homotopy/WhiteheadProducts/Properties.agda
@@ -1,8 +1,9 @@
 {-# OPTIONS --safe --lossy-unification #-}
-module Cubical.Homotopy.Whitehead where
+module Cubical.Homotopy.WhiteheadProducts.Properties where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Path
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Pointed
@@ -18,54 +19,17 @@ open import Cubical.HITs.Sn
 open import Cubical.HITs.Sn.Multiplication
 open import Cubical.HITs.Join
 open import Cubical.HITs.Wedge
-open import Cubical.HITs.SetTruncation
 
 open import Cubical.Homotopy.Group.Base
-open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Join
+
+open import Cubical.Homotopy.WhiteheadProducts.Base
+open import Cubical.Homotopy.WhiteheadProducts.Generalised.Base
+open import Cubical.Homotopy.WhiteheadProducts.Generalised.Properties
 
 open Iso
 open 3x3-span
 
--- Whitehead product (main definition)
-[_∣_]-pre : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (S₊∙ (suc n) →∙ X)
-       → (S₊∙ (suc m) →∙ X)
-       → join∙ (S₊∙ n) (S₊∙ m) →∙ X
-fst ([_∣_]-pre {X = X} {n = n} {m = m} f g) (inl x) = pt X
-fst ([_∣_]-pre {X = X} {n = n} {m = m} f g) (inr x) = pt X
-fst ([_∣_]-pre {n = n} {m = m} f g) (push a b i) =
-  (Ω→ g .fst (σS b) ∙ Ω→ f .fst (σS a)) i
-snd ([_∣_]-pre {n = n} {m = m} f g) = refl
-
-[_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (S₊∙ (suc n) →∙ X)
-       → (S₊∙ (suc m) →∙ X)
-       → S₊∙ (suc (n + m)) →∙ X
-[_∣_] {n = n} {m = m} f g =
-  [ f ∣ g ]-pre ∘∙ (sphere→Join n m , IsoSphereJoin⁻Pres∙ n m)
-
--- Whitehead product (as a composition)
-joinTo⋁ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
- → join (typ A) (typ B)
- → (Susp (typ A) , north) ⋁ (Susp (typ B) , north)
-joinTo⋁ (inl x) = inr north
-joinTo⋁ (inr x) = inl north
-joinTo⋁ {A = A} {B = B} (push a b i) =
-     ((λ i → inr (σ B b i))
-  ∙∙ sym (push tt)
-  ∙∙ λ i → inl (σ A a i)) i
-
-[_∣_]comp : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (S₊∙ (suc n) →∙ X)
-       → (S₊∙ (suc m) →∙ X)
-       → S₊∙ (suc (n + m)) →∙ X
-[_∣_]comp {n = n} {m = m} f g =
-    (((f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
-  ∨→ (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))
-    , cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f)
-  ∘∙ ((joinTo⋁ {A = S₊∙ n} {B = S₊∙ m} , sym (push tt))))
-  ∘∙ (inv (IsoSphereJoin n m) , IsoSphereJoin⁻Pres∙ n m)
-
 []comp≡[] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
        → (f : (S₊∙ (suc n) →∙ X))
        → (g : (S₊∙ (suc m) →∙ X))
@@ -80,7 +44,6 @@ joinTo⋁ {A = A} {B = B} (push a b i) =
        (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))
        , cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f)
 
-    open import Cubical.Foundations.Path
     main : (n m : ℕ) (f : (S₊∙ (suc n) →∙ X)) (g : (S₊∙ (suc m) →∙ X))
       → (∨fun f g ∘∙ (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m} , sym (push tt)))
       ≡ [ f ∣ g ]-pre
@@ -150,11 +113,7 @@ joinTo⋁ {A = A} {B = B} (push a b i) =
                 ∙ (sym (snd f) ∙∙ cong (fst f) (σS a) ∙∙ λ j → snd f (j ∧ i))
                ∙∙ sym (compPath-filler (cong (fst f) (IsoSucSphereSusp∙ n)) (snd f) i))
 
--- Homotopy group version
-[_∣_]π' : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → π' (suc n) X → π' (suc m) X
-       → π' (suc (n + m)) X
-[_∣_]π' = elim2 (λ _ _ → squash₂) λ f g → ∣ [ f ∣ g ] ∣₂
+
 
 -- We prove that the function joinTo⋁ used in the definition of the whitehead
 -- product gives an equivalence between (Susp A × Susp B) and the
@@ -467,104 +426,138 @@ module _ (A B : Type) (a₀ : A) (b₀ : B) where
        ∙ (λ i j → north , cong-∙ invSusp (merid a) (sym (merid b₀)) i (~ j) )
         ◁ λ i j → north , compPath-filler (sym (merid a)) (merid b₀) (~ i) (~ j)
 
--- Generalised Whitehead products
-module _ {ℓ ℓ' ℓ''} {A : Pointed ℓ}
-         {B : Pointed ℓ'} {C : Pointed ℓ''}
-         (f : Susp∙ (typ A) →∙ C) (g : Susp∙ (typ B) →∙ C) where
-
-  _·w_ : join∙ A B →∙ C
-  fst _·w_ (inl x) = pt C
-  fst _·w_ (inr x) = pt C
-  fst _·w_ (push a b i) = (Ω→ g .fst (σ B b) ∙ Ω→ f .fst (σ A a)) i
-  snd _·w_ = refl
-
-  -- The generalised Whitehead product vanishes under suspension
-  isConst-Susp·w : suspFun∙ (_·w_ .fst) ≡ const∙ _ _
-  isConst-Susp·w = Susp·w∙
-                 ∙ cong suspFun∙ (cong fst isConst-const*)
-                 ∙ ΣPathP ((suspFunConst (pt C)) , refl)
+
+open import Cubical.Data.Nat.Order
+
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Homotopy.WhiteheadProducts.Generalised.Properties
+open import Cubical.Homotopy.Group.Join
+open import Cubical.HITs.SetTruncation
+
+-π^ : ∀ {ℓ} {k : ℕ} {A : Pointed ℓ} (n : ℕ) → π' (suc k) A → π' (suc k) A
+-π^ {k = k} n = iter n (-π' k)
+
+[_∣_]π*-comm : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       (f : π' (suc (suc n)) X) (g : π' (suc (suc m)) X)
+       → [ f ∣ g ]π* ≡ fun (π*SwapIso (suc m) (suc n) X) [ g ∣ f ]π*
+[_∣_]π*-comm {n = n} {m = m} = elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
+  λ f g → cong ∣_∣₂
+    (WhiteheadProdComm'
+        (S₊∙ (suc n)) (S₊∙ n) (isoToEquiv (IsoSucSphereSusp n) , IsoSucSphereSusp∙' n)
+        (S₊∙ (suc m)) (S₊∙ m) (isoToEquiv (IsoSucSphereSusp m) , IsoSucSphereSusp∙' m) f g
+    ∙ cong (·wh (S₊∙ (suc m)) (S₊∙ (suc n)) g f ∘∙_)
+       (ΣPathP (refl , sym (cong₂ _∙_ refl (∙∙lCancel _) ∙ sym (rUnit _)))))
+
+[_∣_]π'-comm : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       (f : π' (suc (suc n)) X) (g : π' (suc (suc m)) X)
+    → [ f ∣ g ]π'
+      ≡ subst (λ k → π' (suc k) X) (+-comm (suc m) (suc n))
+              (-π^ (n · m) [ g ∣ f ]π')
+[_∣_]π'-comm {X = X} {n} {m} f g = {!!}
+  where
+  open import Cubical.HITs.SetTruncation as ST
+  open import Cubical.Foundations.Transport
+  open import Cubical.HITs.S1 hiding (_·_)
+  
+  com-main : (n m : ℕ) (t : π' (suc (n + m)) X)
+    → (fun (π*SwapIso n m X) (inv (Iso-π*-π' n m) t))
+      ≡ -π*^ (n · m) (inv (Iso-π*-π' m n)
+           (subst (λ k → π' (suc k) X) (+-comm n m) t))
+  com-main n m = ST.elim {!!}
+    λ t → cong ∣_∣₂ (ΣPathP ({!!} , {!!}) ∙ {!!})
+         ∙ sym (-π*^≡ (n · m) _)
     where
-    const* : join∙ A B →∙ C
-    fst const* (inl x) = pt C
-    fst const* (inr x) = pt C
-    fst const* (push a b i) =
-      (Ω→ f .fst (σ A a) ∙ Ω→ g .fst (σ B b)) i
-    snd const* = refl
-
-    isConst-const* : const* ≡ const∙ _ _
-    fst (isConst-const* i) (inl x) = Ω→ f .fst (σ A x) i
-    fst (isConst-const* i) (inr x) = Ω→ g .fst (σ B x) (~ i)
-    fst (isConst-const* i) (push a b j) =
-      compPath-filler'' (Ω→ f .fst (σ A a)) (Ω→ g .fst (σ B b)) (~ i) j
-    snd (isConst-const* i) j =
-      (cong (Ω→ f .fst) (rCancel (merid (pt A))) ∙ Ω→ f .snd) j i
-
-    Susp·w : suspFun (fst _·w_) ≡ suspFun (fst const*)
-    Susp·w i north = north
-    Susp·w i south = south
-    Susp·w i (merid (inl x) j) = merid (pt C) j
-    Susp·w i (merid (inr x) j) = merid (pt C) j
-    Susp·w i (merid (push a b k) j) =
-      hcomp (λ r →
-        λ {(i = i0) → fill₁ k (~ r) j
-         ; (i = i1) → fill₂ k (~ r) j
-         ; (j = i0) → north
-         ; (j = i1) → merid (pt C) r
-         ; (k = i0) → compPath-filler (merid (snd C)) (merid (pt C) ⁻¹) (~ r) j
-         ; (k = i1) → compPath-filler (merid (snd C)) (merid (pt C) ⁻¹) (~ r) j})
-       (hcomp (λ r →
-        λ {(i = i0) → doubleCompPath-filler
-                         (sym (rCancel (merid (pt C))))
-                         (λ k → fill₁ k i1)
-                         (rCancel (merid (pt C))) (~ r) k j
-         ; (i = i1) → doubleCompPath-filler
-                         (sym (rCancel (merid (pt C))))
-                         (λ k → fill₂ k i1)
-                         (rCancel (merid (pt C))) (~ r) k j
-         ; (j = i0) → north
-         ; (j = i1) → north
-         ; (k = i0) → rCancel (merid (pt C)) (~ r) j
-         ; (k = i1) → rCancel (merid (pt C)) (~ r) j})
-           (main i k j))
+    invSphere∙ : (n : ℕ) → invSphere (ptSn (suc n)) ≡ ptSn (suc n)
+    invSphere∙ zero = refl
+    invSphere∙ (suc n) = merid (ptSn (suc n)) ⁻¹
+
+    -- iter-const : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (a : A) → iter n (λ _ → 
+    -- iter-const = ?
+
+    -S^∙ : {k : ℕ} (n : ℕ) → -S^ {k = (suc k)} n (ptSn (suc k)) ≡ ptSn (suc k)
+    -S^∙ zero = refl
+    -S^∙ (suc n) = cong invSphere (-S^∙ n) ∙ invSphere∙ _
+
+    open import Cubical.Data.Bool
+    cong-S^ : {k : ℕ} (n : ℕ) (x : S₊ k)
+      → PathP (λ i → -S^∙ {k = k} n i ≡ -S^∙ n i) (cong (-S^ n) (σS x)) (sym^ n (σS x))
+    cong-S^ {k} zero x = refl
+    cong-S^ {zero} (suc n) false = {!iterswap n invLooper!} ◁ {!!} ▷ {!!}
+    cong-S^ {zero} (suc n) true =
+      (λ i _ → -S^∙ {k = zero} (suc n) i) ▷ sym (sym^-refl (suc n))
+
+    cong-S^ {suc k} (suc n) x i j = 
+      hcomp (λ k → λ {(i = i0) → invSphere (iter n invSphere (σS x j))
+                     ; (i = i1) → help k j})
+            (invSphere (cong-S^ n x i j))
+      where
+      help : Square (cong invSusp (sym^ n (σS x))) (sym^ (suc n) (σS x))
+                    (merid (ptSn _) ⁻¹) (merid (ptSn _) ⁻¹)
+      help = (sym (cong (cong invSusp) (σS-S^ n x))
+             ∙ cong-∙ invSusp (merid (-S^ n x)) (merid (ptSn (suc k)) ⁻¹))
+            ◁ (λ i → compPath-filler (compPath-filler' (merid (ptSn _))
+                        (sym (merid (-S^ n x))) i) (merid (ptSn _)) (~ i))
+                   ▷ sym (symDistr _ _)
+            ▷ (cong sym (σS-S^ n x))
+
+{-
+Goal: S₊ (suc k)
+———— Boundary (wanted) —————————————————————————————————————
+j = i0 ⊢ hcomp
+         (doubleComp-faces (λ _ → invSphere (-S^ n (ptSn (suc k))))
+          (invSphere∙ (suc k)) i)
+         (invSphere (-S^∙ n i))
+j = i1 ⊢ hcomp
+         (doubleComp-faces (λ _ → invSphere (-S^ n (ptSn (suc k))))
+          (invSphere∙ (suc k)) i)
+         (invSphere (-S^∙ n i))
+i = i0 ⊢ invSphere (iter n invSphere (σS x j))
+i = i1 ⊢ iter n (λ p i₁ → p (~ i₁)) (σS x) (~ j)
+-}
+
+
+    open import Cubical.Homotopy.Loopspace
+    p : (j : I) → _
+    p j = doubleWhiskFiller refl (λ i → ptSn (suc (+-comm n m i))) (sym (-S^∙ (suc (n · m)))) j -- (λ i → ptSn (suc (+-comm n m i))) ▷ sym (-S^∙ (suc (n · m)))
+
+    help : (x : _) → PathP (λ i → S₊ (suc (+-comm n m i)))
+                            (join→Sphere n m (join-commFun x))
+                            (-S^ (suc (n · m)) ((join→Sphere m n x)))
+    help (inl x) = p i1
+    help (inr x) = p i1
+    help (push a b i) j = help' j i
       where
-      F : Ω C .fst → (Ω^ 2) (Susp∙ (fst C)) .fst
-      F p = sym (rCancel (merid (pt C)))
-         ∙∙ cong (σ C) p
-         ∙∙ rCancel (merid (pt C))
-
-      F-hom : (p q : _) → F (p ∙ q) ≡ F p ∙ F q
-      F-hom p q =
-          cong (sym (rCancel (merid (pt C)))
-               ∙∙_∙∙ rCancel (merid (pt C)))
-               (cong-∙ (σ C) p q)
-        ∙ doubleCompPath≡compPath (sym (rCancel (merid (pt C)))) _ _
-        ∙ cong (sym (rCancel (merid (pt C))) ∙_)
-               (sym (assoc _ _ _))
-        ∙ assoc _ _ _
-        ∙ (λ i → (sym (rCancel (merid (pt C)))
-                ∙ compPath-filler (cong (σ C) p) (rCancel (merid (pt C))) i)
-                ∙ compPath-filler' (sym (rCancel (merid (pt C))))
-                                   (cong (σ C) q ∙ rCancel (merid (pt C))) i)
-        ∙ cong₂ _∙_ (sym (doubleCompPath≡compPath _ _ _))
-                    (sym (doubleCompPath≡compPath _ _ _))
-
-      main : F ((Ω→ g .fst (σ B b) ∙ Ω→ f .fst (σ A a)))
-           ≡ F ((Ω→ f .fst (σ A a) ∙ Ω→ g .fst (σ B b)))
-      main = F-hom (Ω→ g .fst (σ B b)) (Ω→ f .fst (σ A a))
-           ∙ EH 0 _ _
-           ∙ sym (F-hom (Ω→ f .fst (σ A a)) (Ω→ g .fst (σ B b)))
-
-      fill₁ : (k : I) → _
-      fill₁ k = compPath-filler
-                (merid ((Ω→ g .fst (σ B b)
-                       ∙ Ω→ f .fst (σ A a)) k))
-                (merid (pt C) ⁻¹)
-
-      fill₂ : (k : I) → _
-      fill₂ k = compPath-filler
-                (merid ((Ω→ f .fst (σ A a)
-                       ∙ Ω→ g .fst (σ B b)) k))
-                (merid (pt C) ⁻¹)
-
-    Susp·w∙ : suspFun∙ (_·w_ .fst) ≡ suspFun∙ (fst const*)
-    Susp·w∙ = ΣPathP (Susp·w , refl)
+      help' : SquareP (λ i j → S₊ (suc (+-comm n m i)))
+                (sym (σSn (n + m) (b ⌣S a)))
+                (cong (-S^ (suc (n · m))) (σS (a ⌣S b)))
+                (p i1) (p i1)
+      help' = cong sym (cong (σSn (n + m)) (comm⌣S b a))
+            ◁ (cong sym (sym (substCommSlice S₊
+                              (λ x → Ω (S₊∙ (suc x)) .fst)
+                              (λ _ → σS) (+-comm m n)
+                              _))
+             ◁ transport (λ j → PathP (λ i → p j i ≡ p j i)
+                         (sym (subst (λ x → Ω (S₊∙ (suc x)) .fst)
+                                  (isSetℕ _ _ (+-comm m n) (sym (+-comm n m)) (~ j))
+                              (σSn (m + n) (-S^ (m · n) (a ⌣S b)))))
+                         (doubleCompPath-filler (sym (-S^∙ (suc (n · m))))
+                                                (cong (-S^ (suc (n · m))) (σS (a ⌣S b)))
+                                                ((-S^∙ (suc (n · m)))) (~ j)))
+               (toPathP (transport⁻Transport (λ i₁ → p i0 (~ i₁) ≡ p i0 (~ i₁)) _
+                      ∙ transport (PathP≡doubleCompPathʳ _ _ _ _) {!!})))
+  com : (n m : ℕ) (t : π' (suc (n + m)) X)
+    →  (fun (π*SwapIso n m X) (inv (Iso-π*-π' n m) t))
+     ≡ inv (Iso-π*-π' m n) (subst (λ k → π' (suc k) X) (+-comm n m)
+        (-π^ (n · m) t))
+  com n m = ST.elim {!!}
+    λ t → cong ∣_∣₂ (ΣPathP ((funExt (λ x → cong (fst t) {!!})) , {!!})) ∙ {!!}
+
+  main : Iso.inv (π*Gr≅π'Gr (suc n) (suc m) X .fst) ([ f ∣ g ]π')
+       ≡ Iso.inv (π*Gr≅π'Gr (suc n) (suc m) X .fst)
+                 (subst (λ k → π' (suc k) X) (+-comm (suc m) (suc n))
+                   (-π^ (n · m) [ g ∣ f ]π' ))
+  main = whπ'≡whπ* f g
+       ∙ [ f ∣ g ]π*-comm
+       ∙ {!!}
+  
diff --git a/Cubical/Papers/Pi4S3-JournalVersion.agda b/Cubical/Papers/Pi4S3-JournalVersion.agda
index fc4281db18..abae5c0e3e 100644
--- a/Cubical/Papers/Pi4S3-JournalVersion.agda
+++ b/Cubical/Papers/Pi4S3-JournalVersion.agda
@@ -28,60 +28,63 @@ open import Cubical.Data.Bool as Boolean
 open import Cubical.Data.Unit as UnitType
 
 open import Cubical.HITs.S1 as Circle
-open import Cubical.Foundations.Prelude                      as Prelude
-open import Cubical.HITs.Susp                                as Suspensions
-open import Cubical.HITs.Sn                                  as Spheres
+open import Cubical.Foundations.Prelude                         as Prelude
+open import Cubical.HITs.Susp                                   as Suspensions
+open import Cubical.HITs.Sn                                     as Spheres
   hiding (S) renaming (S₊ to S)
-open import Cubical.HITs.Pushout                             as Pushouts
-open import Cubical.HITs.Wedge                               as Wedges
-open import Cubical.HITs.Join                                as Joins
-open import Cubical.HITs.Susp                                as Suspension
-open import Cubical.HITs.PropositionalTruncation             as PT
-open import Cubical.HITs.Truncation                          as Trunc
-open import Cubical.Foundations.Univalence                   as Univ
-open import Cubical.Homotopy.Loopspace                       as Loopy
-
-open import Cubical.Homotopy.HSpace                          as H-Spaces
-open import Cubical.Homotopy.Group.Base                      as HomotopyGroups
-open import Cubical.Homotopy.Group.LES                       as LES
-open import Cubical.Homotopy.HopfInvariant.HopfMap           as HopfMap
-open import Cubical.Homotopy.Hopf                            as HopfFibration
-open import Cubical.Homotopy.Connected                       as Connectedness
+open import Cubical.HITs.Pushout                                as Pushouts
+open import Cubical.HITs.Wedge                                  as Wedges
+open import Cubical.HITs.Join                                   as Joins
+open import Cubical.HITs.Susp                                   as Suspension
+open import Cubical.HITs.PropositionalTruncation                as PT
+open import Cubical.HITs.Truncation                             as Trunc
+open import Cubical.Foundations.Univalence                      as Univ
+open import Cubical.Homotopy.Loopspace                          as Loopy
+
+open import Cubical.Homotopy.HSpace                             as H-Spaces
+open import Cubical.Homotopy.Group.Base                         as HomotopyGroups
+open import Cubical.Homotopy.Group.LES                          as LES
+open import Cubical.Homotopy.HopfInvariant.HopfMap              as HopfMap
+open import Cubical.Homotopy.Hopf                               as HopfFibration
+open import Cubical.Homotopy.Connected                          as Connectedness
 open S¹Hopf
-open import Cubical.Homotopy.Freudenthal                     as Freudenthal
-open import Cubical.Homotopy.Group.PinSn                     as Stable
-open import Cubical.Homotopy.Group.Pi3S2                     as π₃S²
+open import Cubical.Homotopy.Freudenthal                        as Freudenthal
+open import Cubical.Homotopy.Group.PinSn                        as Stable
+open import Cubical.Homotopy.Group.Pi3S2                        as π₃S²
 
 -- 3
-open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso        as James₁
-open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2       as James₂
-open import Cubical.HITs.S2                                  as Sphere
-open import Cubical.Homotopy.Whitehead                       as Whitehead
+open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso           as James₁
+open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2          as James₂
+open import Cubical.HITs.S2                                     as Sphere
+open import Cubical.Homotopy.WhiteheadProducts.Base             as Whitehead
+open import Cubical.Homotopy.WhiteheadProducts.Properties       as WhiteheadProps
+open import Cubical.Homotopy.WhiteheadProducts.Generalised.Base as WhiteheadGen
 open import Cubical.Homotopy.BlakersMassey
 module BM = BlakersMassey□
 open BM
-open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber      as BNumber
+open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber         as BNumber
   hiding (W)
 
 -- 5
-open import Cubical.ZCohomology.Base                         as cohom
-open import Cubical.ZCohomology.GroupStructure               as cohomGr
-open import Cubical.ZCohomology.Properties                   as cohomProps
-open import Cubical.ZCohomology.RingStructure.CupProduct     as cup
-open import Cubical.ZCohomology.MayerVietorisUnreduced       as MayerVietoris
-open import Cubical.Homotopy.HopfInvariant.Base              as HI
-open import Cubical.Homotopy.HopfInvariant.Homomorphism      as HI-hom
-open import Cubical.Homotopy.HopfInvariant.Brunerie          as HI-β
-open import Cubical.ZCohomology.Gysin                        as GysinSeq
-open import Cubical.Homotopy.Group.Pi4S3.Summary             as π₄S³
+open import Cubical.ZCohomology.Base                            as cohom
+open import Cubical.ZCohomology.GroupStructure                  as cohomGr
+open import Cubical.ZCohomology.Properties                      as cohomProps
+open import Cubical.ZCohomology.RingStructure.CupProduct        as cup
+open import Cubical.ZCohomology.MayerVietorisUnreduced          as MayerVietoris
+open import Cubical.Homotopy.HopfInvariant.Base                 as HI
+open import Cubical.Homotopy.HopfInvariant.Homomorphism         as HI-hom
+open import Cubical.Homotopy.HopfInvariant.Brunerie             as HI-β
+open import Cubical.ZCohomology.Gysin                           as GysinSeq
+open import Cubical.Homotopy.Group.Pi4S3.Summary                as π₄S³
   hiding (π)
-open import Cubical.ZCohomology.RingStructure.RingLaws       as cupLaws
+open import Cubical.ZCohomology.RingStructure.RingLaws          as cupLaws
 
 -- 6
-open import Cubical.HITs.SmashProduct.Base                   as SmashProd
-open import Cubical.HITs.Sn.Multiplication                   as SMult
-open import Cubical.Homotopy.Group.Join                      as JoinGroup
-open import Cubical.Homotopy.Group.Pi4S3.DirectProof         as Direct
+open import Cubical.HITs.SmashProduct.Base                      as SmashProd
+open import Cubical.HITs.Sn.Multiplication                      as SMult
+open import Cubical.Homotopy.Group.Join                         as JoinGroup
+open import Cubical.HITs.Join.CoHSpace                          as JoinCoH
+open import Cubical.Homotopy.Group.Pi4S3.DirectProof            as Direct
 
 
 ------ 2. HOMOTOPY TYPE THEORY IN Cubical Agda ------
@@ -361,7 +364,7 @@ open SMult using (comm⌣S ; assoc⌣S)
 open JoinGroup using (π*)
 
 -- Addition +*
-open JoinGroup using (_+*_)
+open JoinCoH using (_+*_)
 
 -- Proposition 6.8
 open JoinGroup using (·Π≡+*)
@@ -387,10 +390,10 @@ open Direct using (η₃' ; computerIsoη₃)
 -- Not formalised explicitly
 
 -- Definition of generalised Whitehead products ·w
-open Whitehead using (_·w_)
+open WhiteheadGen using (·wh)
 
 -- Proposition 6.22 (including Lemmas 19 and 20 and Proposition 6.21)
-open Whitehead using (isConst-Susp·w)
+open WhiteheadGen using (isConst-Susp·w)
 
 -- Theorem 6.23
 -- Follows directly from above but not formalised explicitly (awaiting
diff --git a/Cubical/Papers/Pi4S3.agda b/Cubical/Papers/Pi4S3.agda
index fa312717f5..d032bd8ec7 100644
--- a/Cubical/Papers/Pi4S3.agda
+++ b/Cubical/Papers/Pi4S3.agda
@@ -57,7 +57,7 @@ open import Cubical.Homotopy.Group.Pi3S2                    as π₃S²
 open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso       as James₁
 open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2      as James₂
 open import Cubical.HITs.S2                                 as Sphere
-open import Cubical.Homotopy.Whitehead                      as Whitehead
+open import Cubical.Homotopy.WhiteheadProducts.Base         as Whitehead
 open import Cubical.Homotopy.BlakersMassey
 module BM = BlakersMassey□
 open BM