diff --git a/Cubical/Foundations/Path.agda b/Cubical/Foundations/Path.agda
index a738bdf499..4bc87ae60c 100644
--- a/Cubical/Foundations/Path.agda
+++ b/Cubical/Foundations/Path.agda
@@ -410,6 +410,16 @@ compPathR→PathP∙∙ {p = p} {q = q} {r = r} {s = s} P j i =
                    ; (j = i1) → doubleCompPath-filler  p s (sym q) (~ k) i})
           (P j i)
 
+PathP→compPathR∙∙ : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
+  → PathP (λ i → p i ≡ q i) r s
+  → r ≡ p ∙∙ s ∙∙ sym q
+PathP→compPathR∙∙ {p = p} {q = q} {r = r} {s = s} P j i =
+    hcomp (λ k → λ { (i = i0) → p (j ∧ ~ k)
+                   ; (i = i1) → q (j ∧ ~ k)
+                   ; (j = i0) → r i
+                   ; (j = i1) → doubleCompPath-filler  p s (sym q) k i})
+          (P j i)
+
 compPath→Square-faces : {a b c d : A} (p : a ≡ c) (q : b ≡ d) (r : a ≡ b) (s : c ≡ d)
   → (i j k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A
 compPath→Square-faces p q r s i j k = λ where
diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda
index 993a2a6af1..7d2151f194 100644
--- a/Cubical/Foundations/Prelude.agda
+++ b/Cubical/Foundations/Prelude.agda
@@ -87,6 +87,16 @@ cong₂ : {C : (a : A) → (b : B a) → Type ℓ} →
 cong₂ f p q i = f (p i) (q i)
 {-# INLINE cong₂ #-}
 
+cong₃ : {C : (a : A) → (b : B a) → Type ℓ}
+        {D : (a : A) (b : B a) → C a b → Type ℓ'}
+        (f : (a : A) (b : B a) (c : C a b) → D a b c) →
+        {x y : A} (p : x ≡ y)
+        {u : B x} {v : B y} (q : PathP (λ i → B (p i)) u v)
+        {s : C x u} {t : C y v} (r : PathP (λ i → C (p i) (q i)) s t)
+      → PathP (λ i → D (p i) (q i) (r i)) (f x u s) (f y v t)
+cong₃ f p q r i = f (p i) (q i) (r i)
+{-# INLINE cong₃ #-}
+
 congP₂ : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'}
   {C : (i : I) (a : A i) → B i a → Type ℓ''}
   (f : (i : I) → (a : A i) → (b : B i a) → C i a b)
diff --git a/Cubical/HITs/S2/Properties.agda b/Cubical/HITs/S2/Properties.agda
index 3d4b60fe14..89faa21478 100644
--- a/Cubical/HITs/S2/Properties.agda
+++ b/Cubical/HITs/S2/Properties.agda
@@ -7,6 +7,7 @@ open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Path
+open import Cubical.Foundations.Isomorphism
 
 open import Cubical.HITs.S1.Base
 open import Cubical.HITs.S2.Base
@@ -63,11 +64,20 @@ S¹×S¹→S² base y = base
 S¹×S¹→S² (loop i) base = base
 S¹×S¹→S² (loop i) (loop j) = surf i j
 
-
 invS² : S² → S²
 invS² base = base
 invS² (surf i j) = surf j i
 
+invS²∘invS²≡id : (x : _) → invS² (invS² x) ≡ x
+invS²∘invS²≡id base = refl
+invS²∘invS²≡id (surf i i₁) = refl
+
+invS²Iso : Iso S² S²
+Iso.fun invS²Iso = invS²
+Iso.inv invS²Iso = invS²
+Iso.rightInv invS²Iso = invS²∘invS²≡id
+Iso.leftInv invS²Iso = invS²∘invS²≡id
+
 S¹×S¹→S²-anticomm : (x y : S¹) → invS² (S¹×S¹→S² x y) ≡ S¹×S¹→S² y x
 S¹×S¹→S²-anticomm base base = refl
 S¹×S¹→S²-anticomm base (loop i) = refl
diff --git a/Cubical/HITs/Sn/Multiplication.agda b/Cubical/HITs/Sn/Multiplication.agda
index 00ca912c0c..56899e9848 100644
--- a/Cubical/HITs/Sn/Multiplication.agda
+++ b/Cubical/HITs/Sn/Multiplication.agda
@@ -4,7 +4,8 @@
 This file contains:
 1. Definition of the multplication Sⁿ × Sᵐ → Sⁿ⁺ᵐ
 2. The fact that the multiplication induces an equivalence Sⁿ ∧ Sᵐ ≃ Sⁿ⁺ᵐ
-3. The algebraic properties of this map
+3. The fact that the multiplication induces an equivalence Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹
+4. The algebraic properties of this map
 -}
 
 module Cubical.HITs.Sn.Multiplication where
@@ -25,8 +26,9 @@ open import Cubical.Data.Bool hiding (elim)
 open import Cubical.Data.Nat hiding (elim)
 open import Cubical.Data.Sigma
 
-open import Cubical.HITs.S1 hiding (_·_)
-open import Cubical.HITs.Sn hiding (IsoSphereJoin)
+open import Cubical.HITs.S1 renaming (_·_ to _*_)
+open import Cubical.HITs.S2
+open import Cubical.HITs.Sn
 open import Cubical.HITs.Susp renaming (toSusp to σ)
 open import Cubical.HITs.Join
 open import Cubical.HITs.Pushout
@@ -316,6 +318,21 @@ joinSphereIso' n m =
    (compIso (congSuspIso (SphereSmashIso n m))
     (invIso (IsoSucSphereSusp (n + m))))
 
+-- The inverse function is not definitionally pointed. Let's change this
+sphere→Join : (n m : ℕ)
+  → S₊ (suc (n + m)) → join (S₊ n) (S₊ m)
+sphere→Join zero zero = Iso.inv (joinSphereIso' 0 0)
+sphere→Join zero (suc m) north = inl true
+sphere→Join zero (suc m) south = inl true
+sphere→Join zero (suc m) (merid a i) =
+  (push true (ptSn (suc m))
+  ∙ cong (Iso.inv (joinSphereIso' zero (suc m))) (merid a)) i
+sphere→Join (suc n) m north = inl (ptSn (suc n))
+sphere→Join (suc n) m south = inl (ptSn (suc n))
+sphere→Join (suc n) m (merid a i) =
+    (push (ptSn (suc n)) (ptSn m)
+  ∙ cong (Iso.inv (joinSphereIso' (suc n) m)) (merid a)) i
+
 join→Sphere≡ : (n m : ℕ) (x : _)
   → join→Sphere n m x ≡ joinSphereIso' n m .Iso.fun x
 join→Sphere≡ zero zero (inl x) = refl
@@ -338,22 +355,45 @@ join→Sphere≡ (suc n) (suc m) (push a b i) j =
   compPath-filler
     (merid (a ⌣S b)) (sym (merid (ptSn (suc n + suc m)))) (~ j) i
 
+sphere→Join≡ : (n m : ℕ) (x : _)
+  → sphere→Join n m x ≡ joinSphereIso' n m .Iso.inv x
+sphere→Join≡ zero zero x = refl
+sphere→Join≡ zero (suc m) north = push true (pt (S₊∙ (suc m)))
+sphere→Join≡ zero (suc m) south = refl
+sphere→Join≡ zero (suc m) (merid a i) j =
+  compPath-filler' (push true (pt (S₊∙ (suc m))))
+                   (cong (joinSphereIso' zero (suc m) .Iso.inv) (merid a)) (~ j) i
+sphere→Join≡ (suc n) m north = push (ptSn (suc n)) (pt (S₊∙ m))
+sphere→Join≡ (suc n) m south = refl
+sphere→Join≡ (suc n) m (merid a i) j =
+  compPath-filler' (push (ptSn (suc n)) (pt (S₊∙ m)))
+                   (cong (joinSphereIso' (suc n) m .Iso.inv) (merid a)) (~ j) i
+
 -- Todo: integrate with Sn.Properties IsoSphereJoin
 IsoSphereJoin : (n m : ℕ)
   → Iso (join (S₊ n) (S₊ m)) (S₊ (suc (n + m)))
 fun (IsoSphereJoin n m) = join→Sphere n m
-inv (IsoSphereJoin n m) = joinSphereIso' n m .Iso.inv
+inv (IsoSphereJoin n m) = sphere→Join n m
 rightInv (IsoSphereJoin n m) x =
-  join→Sphere≡ n m (joinSphereIso' n m .Iso.inv x)
+  (λ i → join→Sphere≡ n m (sphere→Join≡ n m x i) i)
   ∙ joinSphereIso' n m .Iso.rightInv x
 leftInv (IsoSphereJoin n m) x =
-  cong (joinSphereIso' n m .inv) (join→Sphere≡ n m x)
+  (λ i → sphere→Join≡ n m (join→Sphere≡ n m x i) i)
   ∙ joinSphereIso' n m .Iso.leftInv x
 
 joinSphereEquiv∙ : (n m : ℕ) → join∙ (S₊∙ n) (S₊∙ m) ≃∙ S₊∙ (suc (n + m))
 fst (joinSphereEquiv∙ n m) = isoToEquiv (IsoSphereJoin n m)
 snd (joinSphereEquiv∙ n m) = refl
 
+IsoSphereJoinPres∙ : (n m : ℕ)
+  → Iso.fun (IsoSphereJoin n m) (inl (ptSn n)) ≡ ptSn (suc (n + m))
+IsoSphereJoinPres∙ n m = refl
+
+IsoSphereJoin⁻Pres∙ : (n m : ℕ)
+  → Iso.inv (IsoSphereJoin n m) (ptSn (suc (n + m))) ≡ inl (ptSn n)
+IsoSphereJoin⁻Pres∙ zero zero = push true true ⁻¹
+IsoSphereJoin⁻Pres∙ zero (suc m) = refl
+IsoSphereJoin⁻Pres∙ (suc n) m = refl
 
 -- Associativity ⌣S
 -- Preliminary lemma
@@ -896,3 +936,103 @@ comm⌣S {n = suc (suc n)} {m = suc (suc m)} x y =
       ∙ sym (cong (subst S₊ (sym (+-comm (suc m) (suc n)))
                  ∘ -S^ (suc n · suc m))
          (comm⌣S x y))) x y
+
+-- Additional properties in low dimension:
+diag⌣ : {n : ℕ} (x : S₊ (suc n)) → x ⌣S x ≡ ptSn _
+diag⌣ {n = zero} base = refl
+diag⌣ {n = zero} (loop i) j = help j i
+  where
+  help : cong₂ _⌣S_ loop loop ≡ refl
+  help = cong₂Funct _⌣S_ loop loop
+       ∙ sym (rUnit _)
+       ∙ rCancel (merid base)
+diag⌣ {n = suc n} north = refl
+diag⌣ {n = suc n} south = refl
+diag⌣ {n = suc n} (merid a i) j = help j i
+  where
+  help : cong₂ _⌣S_ (merid a) (merid a) ≡ refl
+  help = cong₂Funct _⌣S_ (merid a) (merid a)
+       ∙ sym (rUnit _)
+       ∙ flipSquare (cong IdL⌣S (merid a))
+
+⌣₁,₁-distr : (a b : S¹) → (b * a) ⌣S b ≡ a ⌣S b
+⌣₁,₁-distr a base = refl
+⌣₁,₁-distr a (loop i) j = lem j i
+  where
+  lem : cong₂ (λ (b1 b2 : S¹) → (b1 * a) ⌣S b2) loop loop
+     ≡ (λ i → a ⌣S loop i)
+  lem = (cong₂Funct (λ (b1 b2 : S¹) → (b1 * a) ⌣S b2) loop loop
+      ∙ cong₂ _∙_ (PathP→compPathR
+                   (flipSquare (cong (IdL⌣S {n = 1} {1} ∘ (_* a)) loop))
+                ∙ cong₂ _∙_ refl (sym (lUnit _))
+                ∙ rCancel _)
+                  refl
+      ∙ sym (lUnit _))
+
+⌣₁,₁-distr' : (a b : S¹) → (a * b) ⌣S b ≡ a ⌣S b
+⌣₁,₁-distr' a b = cong (_⌣S b) (commS¹ a b) ∙ ⌣₁,₁-distr a b
+
+⌣Sinvₗ : {n m : ℕ} (x : S₊ (suc n)) (y : S₊ (suc m))
+  → (invSphere x) ⌣S y ≡ invSphere (x ⌣S y)
+⌣Sinvₗ {n = zero} {m} base y = merid (ptSn (suc m))
+⌣Sinvₗ {n = zero} {m} (loop i) y j = lem j i
+  where
+  lem : Square (σS y ⁻¹)
+               (λ i → invSphere (loop i ⌣S y))
+               (merid (ptSn (suc m))) (merid (ptSn (suc m)))
+  lem = sym (cong-∙ invSphere' (merid y) (sym (merid (ptSn (suc m))))
+      ∙ cong₂ _∙_ refl (rCancel _)
+      ∙ sym (rUnit _))
+      ◁ (λ j i → invSphere'≡ (loop i ⌣S y) j)
+⌣Sinvₗ {n = suc n} {m} north y = merid (ptSn (suc (n + suc m)))
+⌣Sinvₗ {n = suc n} {m} south y = merid (ptSn (suc (n + suc m)))
+⌣Sinvₗ {n = suc n} {m} (merid a i) y j = lem j i
+  where
+  p = ptSn (suc (n + suc m))
+
+  lem : Square (σS (a ⌣S y) ⁻¹)
+               (λ i → invSphere (merid a i ⌣S y))
+               (merid p) (merid p)
+  lem = (sym (cong-∙ invSphere' (merid (a ⌣S y)) (sym (merid p))
+      ∙ cong₂ _∙_ refl (rCancel _)
+      ∙ sym (rUnit _)))
+      ◁ λ j i → invSphere'≡ (merid a i ⌣S y) j
+
+⌣Sinvᵣ : {n m : ℕ} (x : S₊ (suc n)) (y : S₊ (suc m))
+      → x ⌣S (invSphere y) ≡ invSphere (x ⌣S y)
+⌣Sinvᵣ {n = n} {m} x y =
+    comm⌣S x (invSphere y)
+  ∙ cong (subst S₊ (+-comm (suc m) (suc n)))
+         (cong (-S^ (suc m · suc n)) (⌣Sinvₗ y x)
+         ∙ sym (invSphere-S^ (suc m · suc n) (y ⌣S x)))
+       ∙ -S^-transp _ (+-comm (suc m) (suc n)) 1
+                      (-S^ (suc m · suc n) (y ⌣S x))
+       ∙ cong invSphere
+           (cong (subst S₊ (+-comm (suc m) (suc n)))
+             (cong (-S^ (suc m · suc n)) (comm⌣S y x)
+             ∙ sym (-S^-transp _ (+-comm (suc n) (suc m))
+                      (suc m · suc n)
+                      (-S^ (suc n · suc m) (x ⌣S y)))
+             ∙ cong (subst S₊ (+-comm (suc n) (suc m)))
+                    ((cong (-S^ (suc m · suc n))
+                      (λ i → -S^ (·-comm (suc n) (suc m) i) (x ⌣S y)))
+                   ∙ -S^² (suc m · suc n) (x ⌣S y))
+                   ∙ cong (λ p → subst S₊ p (x ⌣S y))
+                        (isSetℕ _ _ (+-comm (suc n) (suc m))
+                                     (+-comm (suc m) (suc n) ⁻¹)))
+             ∙ subst⁻Subst S₊ (+-comm (suc m) (suc n) ⁻¹) (x ⌣S y))
+
+-- Interaction between ⌣S, SuspS¹→S² and SuspS¹→S²
+SuspS¹→S²-S¹×S¹→S² : (a b : S¹)
+  → SuspS¹→S² (a ⌣S b) ≡ S¹×S¹→S² a b
+SuspS¹→S²-S¹×S¹→S² base b = refl
+SuspS¹→S²-S¹×S¹→S² (loop i) b j = main b j i
+  where
+  lem : (b : _) → cong SuspS¹→S² (merid b) ≡ (λ j → S¹×S¹→S² (loop j) b)
+  lem base = refl
+  lem (loop i) = refl
+
+  main : (b : _) → cong SuspS¹→S² (σS b) ≡ (λ j → S¹×S¹→S² (loop j) b)
+  main b = cong-∙ SuspS¹→S² (merid b) (merid base ⁻¹)
+         ∙ sym (rUnit _)
+         ∙ lem b
diff --git a/Cubical/HITs/Sn/Properties.agda b/Cubical/HITs/Sn/Properties.agda
index 7eb740a4c0..91bf1fa440 100644
--- a/Cubical/HITs/Sn/Properties.agda
+++ b/Cubical/HITs/Sn/Properties.agda
@@ -33,8 +33,7 @@ private
 open Iso
 
 σSn : (n : ℕ) → S₊ n → Path (S₊ (suc n)) (ptSn (suc n)) (ptSn (suc n))
-σSn zero false = loop
-σSn zero true = refl
+σSn zero = cong SuspBool→S¹ ∘ merid
 σSn (suc n) x = toSusp (S₊∙ (suc n)) x
 
 σS : {n : ℕ} → S₊ n → Path (S₊ (suc n)) (ptSn _) (ptSn _)
@@ -477,180 +476,6 @@ SuspS¹-inv x = (lUnit _
      ∙ ((λ i → cong ∣_∣ₕ (σSn 1 (rCancelS¹ x (~ i))))
      ∙ cong (cong ∣_∣ₕ) (rCancel (merid base))) ∙ sym (rCancel _)
 
--------------------- join Sⁿ Sᵐ ≃ Sⁿ⁺¹⁺ᵐ -------------------------
-{-
-This section contains a proof that join Sⁿ Sᵐ ≃ Sⁿ⁺ᵐ⁺¹. This is easy using
-various properties proved in HITs.Join. However, we would like the map
-join Sⁿ Sᵐ → Sⁿ⁺ᵐ⁺¹
-to be nice, in particular when n = m = 1. Therefore, we put in some extra work into
-the equivalence.
--}
-
-
-{- We begin with join S¹ S¹ ≃ S³. The iso is induced by: -}
-S¹×S¹→S² : S¹ → S¹ → S₊ 2
-S¹×S¹→S² base y = north
-S¹×S¹→S² (loop i) base = north
-S¹×S¹→S² (loop i) (loop j) =
-  (sym (rCancel (merid base))
-  ∙∙ (λ i → merid (loop i) ∙ sym (merid base))
-  ∙∙ rCancel (merid base)) i j
-
-joinS¹S¹→S³ : join S¹ S¹ → S₊ 3
-joinS¹S¹→S³ (inl x) = north
-joinS¹S¹→S³ (inr x) = south
-joinS¹S¹→S³ (push a b i) = merid (S¹×S¹→S² a b) i
-
-{- Proving that this is an equivalence directly is painful,
-  so we simply prove that it is equal to the old definition of
-  the equivalence join S¹ S¹ ≃ S³ ≃ S₊ 3
-  To this end, we start by rephrasing the map -}
-private
-  3cell : (r i j k : I) → S₊ 3
-  3cell r i j k =
-    hfill (λ r → λ {(i = i0) → merid (merid base j) (k ∧ ~ r)
-                   ; (i = i1) → merid (merid base j) (k ∧ ~ r)
-                   ; (j = i0) → merid north (k ∧ ~ r)
-                   ; (j = i1) → merid south (k ∧ ~ r)
-                   ; (k = i0) → north
-                   ; (k = i1) → merid (merid base j) (~ r)})
-          (inS (merid (merid (loop i) j) k))
-          r
-
-joinS¹S¹→S³' : join S¹ S¹ → S₊ 3
-joinS¹S¹→S³' (inl x) = north
-joinS¹S¹→S³' (inr x) = north
-joinS¹S¹→S³' (push base b i) = north
-joinS¹S¹→S³' (push (loop i₁) base i) = north
-joinS¹S¹→S³' (push (loop i₁) (loop i₂) i) = 3cell i1 i₁ i₂ i
-
-{- These two maps are equal -}
-joinS¹S¹→S³'≡joinS¹S¹→S³' : (x : _) → joinS¹S¹→S³ x ≡ joinS¹S¹→S³' x
-joinS¹S¹→S³'≡joinS¹S¹→S³' (inl base) = refl
-joinS¹S¹→S³'≡joinS¹S¹→S³' (inl (loop i)) = refl
-joinS¹S¹→S³'≡joinS¹S¹→S³' (inr base) = sym (merid north)
-joinS¹S¹→S³'≡joinS¹S¹→S³' (inr (loop i)) = sym (merid north)
-joinS¹S¹→S³'≡joinS¹S¹→S³' (push base base i) k = merid north (~ k ∧ i)
-joinS¹S¹→S³'≡joinS¹S¹→S³' (push base (loop i₁) i) k  = merid north (~ k ∧ i)
-joinS¹S¹→S³'≡joinS¹S¹→S³' (push (loop i₁) base i) k =  (merid north) (~ k ∧ i)
-joinS¹S¹→S³'≡joinS¹S¹→S³' (push (loop i) (loop j) k) l =
-  hcomp (λ r → λ { (i = i0) → merid (sym (rCancel (merid base)) (~ r) j)
-                                      (~ l ∧ k)
-                  ; (i = i1) → merid (sym (rCancel (merid base)) (~ r) j)
-                                      (~ l ∧ k)
-                  ; (j = i0) → merid north (~ l ∧ k)
-                  ; (j = i1) → merid north (~ l ∧ k)
-                  ; (k = i0) → north
-                  ; (k = i1) → merid (sym (rCancel (merid base)) (~ r) j) (~ l)
-                  ; (l = i0) → merid (doubleCompPath-filler
-                                      (sym (rCancel (merid base)))
-                                      (cong (σSn 1) loop)
-                                      (rCancel (merid base)) r i j) k
-                  ; (l = i1) → 3cell i1 i j k})
-    (hcomp (λ r → λ {(i = i0) → merid (cp-fill base r j) (k ∧ ~ l)
-                   ; (i = i1) → merid (cp-fill base r j) (k ∧ ~ l)
-                   ; (j = i0) → merid north (~ l ∧ k)
-                   ; (j = i1) → merid (merid base (~ r)) (~ l ∧ k)
-                   ; (k = i0) → north
-                   ; (k = i1) → merid (cp-fill base r j) (~ l)
-                   ; (l = i0) → merid (cp-fill (loop i) r j) k
-                   ; (l = i1) → 3cell i1 i j k})
-       (hcomp (λ r → λ {(i = i0) → merid (merid base j) (k ∧ (~ r ∨ ~ l))
-                   ; (i = i1) → merid (merid base j) (k ∧ (~ r ∨ ~ l))
-                   ; (j = i0) → merid north (k ∧ (~ l ∨ ~ r))
-                   ; (j = i1) → merid south (k ∧ (~ l ∨ ~ r))
-                   ; (k = i0) → north
-                   ; (k = i1) → merid (merid base j) (~ r ∨ ~ l)
-                   ; (l = i0) → merid (merid (loop i) j) k
-                   ; (l = i1) → 3cell r i j k})
-              (merid (merid (loop i) j) k)))
-  where
-  cp-fill : (a : S¹) → _
-  cp-fill a = compPath-filler (merid a) (sym (merid base))
-
-{- joinS¹S¹→S³' is equal to the original
-  equivalence (modulo a flipping of interval variables) -}
-joinS¹S¹→S³'Id : (x : join S¹ S¹)
-  → joinS¹S¹→S³' x ≡ (Iso.fun IsoS³S3 ∘ flip₀₂S³ ∘ joinS¹S¹→S3) x
-joinS¹S¹→S³'Id (inl x) = refl
-joinS¹S¹→S³'Id (inr x) = refl
-joinS¹S¹→S³'Id (push base base i) = refl
-joinS¹S¹→S³'Id (push base (loop i₁) i) = refl
-joinS¹S¹→S³'Id (push (loop i₁) base i) = refl
-joinS¹S¹→S³'Id (push (loop i) (loop j) k) l =
-  hcomp (λ r → λ {(i = i0) → merid (merid base (j ∧ ~ l)) (~ r ∧ k)
-                 ; (i = i1) → merid (merid base (j ∧ ~ l)) (~ r ∧ k)
-                 ; (j = i0) → merid north (k ∧ ~ r)
-                 ; (j = i1) → merid (merid base (~ l)) (~ r ∧ k)
-                 ; (k = i0) → north
-                 ; (k = i1) → merid (merid base (j ∧ ~ l)) (~ r)
-                 ; (l = i0) → 3cell r i j k
-                 ; (l = i1) → Iso.fun (IsoType→IsoSusp S²IsoSuspS¹)
-                                       (meridian-contraction-2 k j i r)})
-        (merid (S²Cube i j l) k)
-  where
-  S²Cube : Cube {A = S₊ 2} (λ j l → merid base (j ∧ ~ l))
-                             (λ j l → merid base (j ∧ ~ l))
-                             (λ i l → north)
-                             (λ i l → merid base (~ l))
-                             (λ i j → merid (loop i) j)
-                             λ i j → fun S²IsoSuspS¹ (surf j i)
-  S²Cube i j l =
-    hcomp (λ r → λ {(i = i0) → merid base (j ∧ (~ l ∨ ~ r))
-                 ; (i = i1) → merid base (j ∧ (~ l ∨ ~ r))
-                 ; (j = i0) → north
-                 ; (j = i1) → merid base (~ l ∨ ~ r)
-                 ; (l = i0) → merid (loop i) j
-                 ; (l = i1) → meridian-contraction j i r})
-           (merid (loop i) j)
-
-{-So, finally our map joinS¹S¹→S³ is an iso. We state its inverse explicitly. -}
-Iso-joinS¹S¹-S³ : Iso (join S¹ S¹) (S₊ 3)
-fun Iso-joinS¹S¹-S³ = joinS¹S¹→S³
-inv Iso-joinS¹S¹-S³ = S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3
-rightInv Iso-joinS¹S¹-S³ x =
-     joinS¹S¹→S³'≡joinS¹S¹→S³'
-       ((S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3) x)
-  ∙∙ joinS¹S¹→S³'Id ((S³→joinS¹S¹ ∘ flip₀₂S³ ∘ Iso.inv IsoS³S3) x)
-  ∙∙ Iso.leftInv (compIso (invIso IsoS³S3)
-                  (compIso flip₀₂S³Iso (S³IsojoinS¹S¹))) x
-leftInv Iso-joinS¹S¹-S³ x =
-     cong (S³→joinS¹S¹ ∘ flip₀₂S³ ∘ inv IsoS³S3)
-          (joinS¹S¹→S³'≡joinS¹S¹→S³' x ∙ joinS¹S¹→S³'Id x)
-   ∙ Iso.rightInv (compIso (invIso IsoS³S3) (compIso flip₀₂S³Iso (S³IsojoinS¹S¹))) x
-
-{- We now get the full iso Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹ -}
-IsoSphereJoin : (n m : ℕ)
-  → Iso (join (S₊ n) (S₊ m)) (S₊ (suc (n + m)))
-IsoSphereJoin zero zero = compIso (invIso Susp-iso-joinBool) (invIso S¹IsoSuspBool)
-IsoSphereJoin zero (suc m) = compIso join-comm (invIso Susp-iso-joinBool)
-IsoSphereJoin (suc zero) zero = (invIso Susp-iso-joinBool)
-IsoSphereJoin (suc zero) (suc zero) = Iso-joinS¹S¹-S³
-IsoSphereJoin (suc zero) (suc (suc m)) =
-  compIso join-comm
-    (compIso (compIso (Iso-joinSusp-suspJoin {A = S₊∙ (suc m)} {B = S₊∙ (suc zero)})
-      (congSuspIso join-comm))
-      (congSuspIso (IsoSphereJoin (suc zero) (suc m))))
-IsoSphereJoin (suc (suc n)) m =
-  compIso (Iso-joinSusp-suspJoin {A = S₊∙ (suc n)} {B = S₊∙ m}) (congSuspIso (IsoSphereJoin (suc n) m))
-
-{- Pointedness holds by refl.
-  This is due to the explicit definition of Iso-joinSusp-suspJoin  -}
-IsoSphereJoinPres∙ : (n m : ℕ)
-  → Iso.fun (IsoSphereJoin n m) (inl (ptSn n)) ≡ ptSn (suc (n + m))
-IsoSphereJoinPres∙ zero zero = refl
-IsoSphereJoinPres∙ zero (suc m) = refl
-IsoSphereJoinPres∙ (suc zero) zero = refl
-IsoSphereJoinPres∙ (suc zero) (suc zero) = refl
-IsoSphereJoinPres∙ (suc zero) (suc (suc m)) = refl
-IsoSphereJoinPres∙ (suc (suc n)) m = refl
-
-IsoSphereJoin⁻Pres∙ : (n m : ℕ)
-  → Iso.inv (IsoSphereJoin n m) (ptSn (suc (n + m))) ≡ inl (ptSn n)
-IsoSphereJoin⁻Pres∙ n m =
-     cong (Iso.inv (IsoSphereJoin n m)) (sym (IsoSphereJoinPres∙ n m))
-   ∙ Iso.leftInv (IsoSphereJoin n m) (inl (ptSn n))
-
 -- Inversion on spheres
 invSphere : {n : ℕ} → S₊ n → S₊ n
 invSphere {n = zero} = not
@@ -698,120 +523,3 @@ 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
-
-
--- Some facts about the map S¹×S¹→S²
--- Todo: generalise to Sⁿ×Sᵐ→Sⁿ⁺ᵐ
-S¹×S¹→S²rUnit : (a : S¹) → S¹×S¹→S² a base ≡ north
-S¹×S¹→S²rUnit base = refl
-S¹×S¹→S²rUnit (loop i) = refl
-
-S¹×S¹→S²x+x : (x : S¹) → S¹×S¹→S² x x ≡ north
-S¹×S¹→S²x+x base = refl
-S¹×S¹→S²x+x (loop i) k = lem k i
-  where
-  lem : cong₂ S¹×S¹→S² loop loop ≡ refl
-  lem = cong₂Funct S¹×S¹→S² loop loop
-    ∙ (λ i → rUnit (cong (λ x → S¹×S¹→S²rUnit x i) loop) (~ i))
-
-S¹×S¹→S²-antiComm : (a b : S¹) → S¹×S¹→S² a b ≡ S¹×S¹→S² b (invLooper a)
-S¹×S¹→S²-antiComm base base = refl
-S¹×S¹→S²-antiComm base (loop i) = refl
-S¹×S¹→S²-antiComm (loop i) base = refl
-S¹×S¹→S²-antiComm (loop i) (loop j) k =
-  sym≡flipSquare (λ j i → S¹×S¹→S² (loop i) (loop j)) (~ k) i j
-
-private
-  S¹×S¹→S²-Distr-filler : (i : I)
-    → cong₂ (λ b c → S¹×S¹→S² ((loop i) * b) c) loop loop
-    ≡ cong (S¹×S¹→S² (loop i)) loop
-  S¹×S¹→S²-Distr-filler i =
-    cong₂Funct (λ b c → S¹×S¹→S² ((loop i) * b) c) loop loop
-     ∙∙ (λ j → cong (λ x → S¹×S¹→S²rUnit (rotLoop x i) j) loop ∙
-                cong (λ c → S¹×S¹→S² (loop i) c) loop)
-     ∙∙ sym (lUnit _)
-
-S¹×S¹→S²-Distr : (a b : S¹) → S¹×S¹→S² (a * b) b ≡ S¹×S¹→S² a b
-S¹×S¹→S²-Distr a base j = S¹×S¹→S² (rUnitS¹ a j) base
-S¹×S¹→S²-Distr base (loop i) k = S¹×S¹→S²-Distr-filler i0 k i
-S¹×S¹→S²-Distr (loop i₁) (loop i) k = S¹×S¹→S²-Distr-filler i₁ k i
-
-invSusp∘S¹×S¹→S² : (a b : S¹)
-  → S¹×S¹→S² a (invLooper b) ≡ invSusp (S¹×S¹→S² a b)
-invSusp∘S¹×S¹→S² base b = merid base
-invSusp∘S¹×S¹→S² (loop i) base = merid base
-invSusp∘S¹×S¹→S² (loop i) (loop j) k =
-  hcomp (λ r → λ {(i = i0) → i-Boundary₂ r j k
-                 ; (i = i1) → i-Boundary₂ r j k
-                 ; (j = i0) → m-b k
-                 ; (j = i1) → m-b k
-                 ; (k = i0) → doubleCompPath-filler
-                                rCancel-mb⁻¹ (cong σ₁ loop) rCancel-mb r i (~ j)
-                 ; (k = i1)
-                    → invSusp (doubleCompPath-filler
-                                 rCancel-mb⁻¹ (cong σ₁ loop) rCancel-mb r i j)})
-   (hcomp (λ r → λ {(i = i0) → i-Boundary r (~ j) k
-                   ; (i = i1) → i-Boundary r (~ j) k
-                   ; (j = i0) → merid base (~ r ∨ k)
-                   ; (j = i1) → merid base (r ∧ k)
-                   ; (k = i0) → cp-filler (loop i) r (~ j)
-                   ; (k = i1) → invSusp (cp-filler (loop i) r j)})
-           (merid (loop i) (~ j)))
-  where
-  σ₁ = σSn 1
-  m-b = merid base
-  rCancel-mb = rCancel m-b
-  rCancel-mb⁻¹ = sym (rCancel m-b)
-
-  cp-filler : (a : S¹) (i j : I) → S₊ 2
-  cp-filler a i j = compPath-filler (merid a) (sym (merid base)) i j
-
-  i-Boundary : I → I → I → S₊ 2
-  i-Boundary r j k =
-    hfill (λ r → λ{(j = i0) → m-b (k ∧ r)
-                  ; (j = i1) → m-b (~ r ∨ k)
-                  ; (k = i0) → cp-filler base r j
-                  ; (k = i1) → invSusp (cp-filler base r (~ j))})
-          (inS (m-b j))
-          r
-
-  i-Boundary₂ : I → I → I → S₊ 2
-  i-Boundary₂ r j k =
-    hcomp (λ i → λ {(r = i0) → i-Boundary i (~ j) k
-                 ; (r = i1) → m-b k
-                 ; (j = i0) → m-b (k ∨ (~ i ∧ ~ r))
-                 ; (j = i1) → m-b (k ∧ (i ∨ r))
-                 ; (k = i0) → rCancel-filler m-b i r (~ j)
-                 ; (k = i1) → invSusp (rCancel-filler m-b i r j) })
-     (hcomp (λ i → λ {(r = i0) → m-b (~ j ∨ (~ i ∧ k))
-                 ; (r = i1) → m-b (k ∨ (~ i ∧ ~ j))
-                 ; (j = i0) → m-b (k ∨ (~ r ∨ ~ i))
-                 ; (j = i1) → m-b (k ∧ (~ i ∨ r))
-                 ; (k = i0) → m-b (~ j ∧ (~ r ∨ ~ i))
-                 ; (k = i1) → m-b ((~ j ∨ ~ i) ∨ r) })
-            (m-b (~ j ∨ k)))
-
--- Interaction between S¹×S¹→S² and SuspS¹→S²
-SuspS¹→S²-S¹×S¹→S² : (a b : S¹)
-  → (SuspS¹→S² (S¹×S¹→S² a b)) ≡ (S¹×S¹→S²' b a)
-SuspS¹→S²-S¹×S¹→S² base base = refl
-SuspS¹→S²-S¹×S¹→S² base (loop i) = refl
-SuspS¹→S²-S¹×S¹→S² (loop i) base = refl
-SuspS¹→S²-S¹×S¹→S² (loop i) (loop j) k =
-  hcomp (λ r → λ {(i = i0) → rUnit (λ _ → base) (~ r ∧ ~ k) j
-                 ; (i = i1) → rUnit (λ _ → base) (~ r ∧ ~ k) j
-                 ; (j = i0) → base
-                 ; (j = i1) → base
-                 ; (k = i0) → SuspS¹→S² (doubleCompPath-filler (
-                                 sym (rCancel (merid base)))
-                                 ((λ i → merid (loop i) ∙ sym (merid base)))
-                                 (rCancel (merid base)) r i j )
-                 ; (k = i1) → surf j i})
-    (hcomp (λ r → λ {(i = i0) → rUnit (λ _ → base) (r ∧ ~ k) j
-                 ; (i = i1) → rUnit (λ _ → base) (r ∧ ~ k) j
-                 ; (j = i0) → base
-                 ; (j = i1) → base
-                 ; (k = i0) → SuspS¹→S²
-                       (compPath-filler (merid (loop i)) (sym (merid base)) r j)
-                 ; (k = i1) → surf j i})
-           (surf j i))
diff --git a/Cubical/HITs/Susp/Properties.agda b/Cubical/HITs/Susp/Properties.agda
index 6c043cf3b9..98f7c2a2ab 100644
--- a/Cubical/HITs/Susp/Properties.agda
+++ b/Cubical/HITs/Susp/Properties.agda
@@ -378,3 +378,12 @@ toSusp-invSusp A (merid a i) j =
           λ r → flipSquare (sym (rUnit refl)
                 ◁ (flipSquare (sym (sym≡cong-sym r))
                 ▷ 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
+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
diff --git a/Cubical/Homotopy/Group/Base.agda b/Cubical/Homotopy/Group/Base.agda
index ec0c1f8f4a..4713d97de8 100644
--- a/Cubical/Homotopy/Group/Base.agda
+++ b/Cubical/Homotopy/Group/Base.agda
@@ -117,12 +117,7 @@ fst (∙Π {A = A} {n = suc zero} (f , p) (g , q)) base = pt A
 fst (∙Π {A = A} {n = suc zero} (f , p) (g , q)) (loop j) =
   ((sym p ∙∙ cong f loop ∙∙ p) ∙ (sym q ∙∙ cong g loop ∙∙ q)) j
 snd (∙Π {A = A} {n = suc zero} (f , p) (g , q)) = refl
-fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) north = pt A
-fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) south = pt A
-fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) (merid a j) =
-   ((sym p ∙∙ cong f (merid a ∙ sym (merid (ptSn (suc n)))) ∙∙ p)
-  ∙ (sym q ∙∙ cong g (merid a ∙ sym (merid (ptSn (suc n)))) ∙∙ q)) j
-snd (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) = refl
+∙Π {A = A} {n = suc (suc n)} = ·Susp (S₊∙ (suc n))
 
 -Π : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
   → (S₊∙ n →∙ A)
diff --git a/Cubical/Homotopy/Group/Join.agda b/Cubical/Homotopy/Group/Join.agda
index e3015ab4c7..0363b836a9 100644
--- a/Cubical/Homotopy/Group/Join.agda
+++ b/Cubical/Homotopy/Group/Join.agda
@@ -324,3 +324,9 @@ snd (π*∘∙Hom {A = A} {B = B} n m f) =
                          (≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))}
                           (joinSphereEquiv∙ n m) .fst)
                        ∙ ∘∙-idˡ g)))
+
+π*∘∙Equiv : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
+  (n m : ℕ) (f : A ≃∙ B)
+  → 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
diff --git a/Cubical/Homotopy/Group/Pi3S2.agda b/Cubical/Homotopy/Group/Pi3S2.agda
index bfde3950ad..119cae49ba 100644
--- a/Cubical/Homotopy/Group/Pi3S2.agda
+++ b/Cubical/Homotopy/Group/Pi3S2.agda
@@ -25,6 +25,7 @@ open import Cubical.Foundations.Equiv
 
 open import Cubical.HITs.SetTruncation renaming (elim to sElim)
 open import Cubical.HITs.Sn
+open import Cubical.HITs.Sn.Multiplication
 open import Cubical.HITs.Susp
 open import Cubical.HITs.S1
 
diff --git a/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda b/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda
index b25c4a31a1..e075036948 100644
--- a/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda
+++ b/Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda
@@ -37,6 +37,8 @@ open import Cubical.Data.Int
 
 open import Cubical.HITs.S1
 open import Cubical.HITs.Sn
+open import Cubical.HITs.Sn.Multiplication
+open import Cubical.HITs.Join
 open import Cubical.HITs.Susp
 open import Cubical.HITs.Wedge
 open import Cubical.HITs.Pushout
@@ -398,21 +400,22 @@ module _ where
 -- first need the following:
 fold∘W≡Whitehead :
         fst (π'∘∙Hom 2 (fold∘W , refl)) ∣ idfun∙ (S₊∙ 3) ∣₂
-      ≡ ∣ [ idfun∙ (S₊∙ 2) ∣ idfun∙ (S₊∙ 2) ]₂ ∣₂
+      ≡ ∣ [ idfun∙ (S₊∙ 2) ∣ idfun∙ (S₊∙ 2) ] ∣₂
 fold∘W≡Whitehead =
-  pRec (squash₂ _ _)
-    (cong ∣_∣₂)
-    (indΠ₃S₂ _ _
-      (funExt (λ x → funExt⁻ (sym (cong fst (id∨→∙id {A = S₊∙ 2}))) (W x))))
+  cong ∣_∣₂ (ΣPathP (funExt (main ∘ sphere→Join 1 1) , refl))
   where
-  indΠ₃S₂ : ∀ {ℓ} {A : Pointed ℓ}
-    → (f g : A →∙ S₊∙ 2)
-      → fst f ≡ fst g → ∥ f ≡ g ∥₁
-  indΠ₃S₂ {A = A} f g p =
-    trRec squash₁
-     (λ r → ∣ ΣPathP (p , r) ∣₁)
-      (isConnectedPathP 1 {A = (λ i → p i (snd A) ≡ north)}
-        (isConnectedPathSⁿ 1 (fst g (pt A)) north) (snd f) (snd g) .fst )
+  main : (x : _) → fold⋁ (joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1} x)
+                  ≡ fst [ idfun∙ (Susp S¹ , north)
+                         ∣ idfun∙ (Susp S¹ , north) ]-pre x
+  main (inl x) = refl
+  main (inr x) = refl
+  main (push a b i) j = help j i
+    where
+    help : cong (fold⋁ ∘ joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1}) (push a b)
+         ≡ (σS b ∙ refl) ∙ σS a ∙ refl
+    help = cong-∙∙ fold⋁ _ _ _
+         ∙ doubleCompPath≡compPath _ _ _
+         ∙ cong₂ _∙_ (rUnit _) (sym (lUnit (σS a)) ∙ rUnit (σS a))
 
 BrunerieIsoAbstract : GroupEquiv (π'Gr 3 (S₊∙ 3)) (abstractℤGroup/ Brunerie)
 BrunerieIsoAbstract =
@@ -430,12 +433,10 @@ BrunerieIsoAbstract =
     fst (π'∘∙Hom 2 (fold∘W , refl))
          (Iso.inv (fst (πₙ'Sⁿ≅ℤ 2)) 1)
      ≡ [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π'
-  mainPath =
-      cong (fst (π'∘∙Hom 2 (fold∘W , refl)))
+  mainPath = cong (fst (π'∘∙Hom 2 (fold∘W , refl)))
            (cong (Iso.inv (fst (πₙ'Sⁿ≅ℤ 2))) (sym (πₙ'Sⁿ≅ℤ-idfun∙ 2))
            ∙ (Iso.leftInv (fst (πₙ'Sⁿ≅ℤ 2)) ∣ idfun∙ (S₊∙ 3) ∣₂))
-    ∙ fold∘W≡Whitehead
-    ∙ cong ∣_∣₂ (sym ([]≡[]₂ (idfun∙ (S₊∙ 2)) (idfun∙ (S₊∙ 2))))
+           ∙ fold∘W≡Whitehead
 
   main : _ ≡ Brunerie
   main i = abs (HopfInvariant-π' 0 (mainPath i))
diff --git a/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda b/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda
index 41513b68cc..3ebf02c48f 100644
--- a/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda
+++ b/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda
@@ -18,9 +18,8 @@ complicates things. In this file, we try to work around this problem.
 The proof goes as follows.
 
 1. Define π₃*(A) := ∥ S¹ * S¹ →∙ A ∥₀ and define explicitly an
-addition on this type. Prove that the equivalence π₃(A) ≃ π₃*(A) is
-structure preserving, thereby giving a group structure on π₃*(A) and a
-group iso π₃*(A) ≅ π₃(A)
+addition on this type. This is already done in
+Cubical.Homotopy.Group.Join.
 
 2. Under this iso, η gets mapped to η₁ (by construction) defined by
 S¹ * S¹ -ᵂ→ S² ∨ S² -ᶠᵒˡᵈ→ S²
@@ -73,6 +72,7 @@ open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber
 open import Cubical.Homotopy.Group.Pi4S3.BrunerieExperiments
   using (K₂ ; f7' ; S¹∙ ; encodeTruncS²)
 -- For computation (alternative proof)
+open import Cubical.Homotopy.Group.Join
 
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat
@@ -82,6 +82,7 @@ open import Cubical.Data.Int
 open import Cubical.HITs.S1 as S1 renaming (_·_ to _*_)
 open import Cubical.HITs.S2 renaming (S¹×S¹→S² to S¹×S¹→S²')
 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.Wedge
@@ -142,231 +143,29 @@ private
         (IsoSphereJoin 1 1)
         (isConnectedSubtr 3 1 (sphereConnected 3)))
 
+  joinS¹S¹→S³ = join→Sphere 1 1
+  S¹×S¹→S² : S¹ → S¹ → S₊ 2
+  S¹×S¹→S² = _⌣S_
+
 -- Key goal: prove that the following element of π₃(S²) gets mapped to -2
 η : π' 3 (S₊∙ 2)
 η = fst (π'∘∙Hom 2 (fold∘W , refl)) ∣ id∙ (S₊∙ 3) ∣₂
 
-{- Step 1. Define an addition on π₃*(A) := ∥ S¹ * S¹ →∙ A ∥₀ -}
--- On the underlying function spaces.
-_+join_ : (f g : (join S¹ S¹ , inl base) →∙ A)
-       → (join S¹ S¹ , inl base) →∙ A
-fst (f +join g) (inl x) = fst f (inl x)
-fst (f +join g) (inr x) = fst g (inr x)
-fst (f +join g) (push a b i) =
-  (cong (fst f) (push a b ∙ sym (push base b))
-  ∙∙ snd f ∙ sym (snd g)
-  ∙∙ cong (fst g) (push base base ∙∙ sym (push a base) ∙∙ push a b)) i
-snd (f +join g) = snd f
-
--- Homotopy group version
-_π₃*+_ : (f g : ∥ (join S¹ S¹ , inl base) →∙ S₊∙ 2 ∥₂)
-      → ∥ (join S¹ S¹ , inl base) →∙ S₊∙ 2 ∥₂
-_π₃*+_ = sRec2 squash₂ λ x y → ∣ x +join y ∣₂
-
--- transferring between π₃ and π₃*
--- (homotopy groups defined in terms of S¹ * S¹)
-joinify :  S₊∙ 3 →∙ A → (join S¹ S¹ , inl base) →∙ A
-fst (joinify f) x = fst f (joinS¹S¹→S³ x)
-snd (joinify f) = snd f
-
-disjoin : (join S¹ S¹ , inl base) →∙ A → S₊∙ 3 →∙ A
-fst (disjoin f) = λ x → fst f (Iso.inv (IsoSphereJoin 1 1) x)
-snd (disjoin f) = snd f
-
-
--- joinify is structure preserving
-+join≡∙Π : (f g : S₊∙ 3 →∙ A)
-         → joinify (∙Π f g)
-         ≡ (joinify f +join joinify g)
-+join≡∙Π f' g' =
-  ΣPathP ((funExt (λ { (inl x) → sym fp
-                     ; (inr x) → sym gp ∙ cong g (merid north)
-                     ; (push a b i) j → main a b j i}))
-        , λ i j → fp (j ∨ ~ i))
-  where
-  f = fst f'
-  g = fst g'
-
-  fp = snd f'
-  gp = snd g'
-
-  path-lem : ∀ {ℓ} {A : Type ℓ} {x y z w u : A}
-       (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) (s : w ≡ u)
-    → (refl ∙∙ p ∙∙ q) ∙ (r ∙∙ s ∙∙ refl)
-     ≡ (p ∙∙ (q ∙ r) ∙∙ s)
-  path-lem p q r s =
-       cong ((p ∙ q) ∙_) (sym (compPath≡compPath' r s))
-    ∙∙ sym (∙assoc p q (r ∙ s))
-    ∙∙ cong (p ∙_) (∙assoc q r s)
-     ∙ sym (doubleCompPath≡compPath p (q ∙ r) s)
-
-  main-helper : (a b : S¹)
-    → Square ((refl ∙∙ cong f (σ₂ (S¹×S¹→S² a b)) ∙∙ fp)
-             ∙ (sym gp ∙∙ cong g (σ₂ (S¹×S¹→S² a b)) ∙∙ refl))
-             ((cong f (merid (S¹×S¹→S² a b))
-             ∙ sym (cong f (merid north)))
-               ∙∙ (fp ∙ sym gp)
-               ∙∙ cong g (merid (S¹×S¹→S² a b)))
-           (λ _ → f north)
-           (cong g (merid north))
-  main-helper a b =
-    path-lem (cong f (σ₂ (S¹×S¹→S² a b)))  fp (sym gp)
-             (cong g (σ₂ (S¹×S¹→S² a b)))
-          ◁ lem
-    where
-    lem : PathP (λ i → f north ≡ cong g (merid north) i)
-              ((λ i → f (σ₂ (S¹×S¹→S² a b) i))
-                    ∙∙ fp ∙ (sym gp) ∙∙
-               (cong g (σ₂ (S¹×S¹→S² a b))))
-              ((cong f (merid (S¹×S¹→S² a b)) ∙ sym (cong f (merid north)))
-               ∙∙ fp ∙ sym gp
-               ∙∙ cong g (merid (S¹×S¹→S² a b)))
-    lem i j =
-      hcomp (λ k → λ { (i = i0) →
-                          (cong-∙ f (merid (S¹×S¹→S² a b))
-                                    (sym (merid north)) (~ k)
-                       ∙∙ fp ∙ sym gp
-                       ∙∙ (λ i → g (σ-filler (S¹×S¹→S² a b) north k i))) j
-                       ; (i = i1) → ((cong f (merid (S¹×S¹→S² a b))
-                                       ∙ sym (cong f (merid north)))
-                                     ∙∙ (fp ∙ sym gp)
-                                     ∙∙ cong g (merid (S¹×S¹→S² a b))) j
-                       ; (j = i0) → f north
-                       ; (j = i1) → g (merid north (~ k ∨ i))})
-            (((cong f (merid (S¹×S¹→S² a b)) ∙ sym (cong f (merid north)))
-            ∙∙ (fp ∙ sym gp)
-            ∙∙ cong g (merid (S¹×S¹→S² a b))) j)
-
-
-  main-helper₂ : (a b : S¹)
-    → cong (fst (joinify g')) (push base base ∙∙ sym (push a base) ∙∙ push a b)
-    ≡ cong g (merid (S¹×S¹→S² a b))
-  main-helper₂ a b = cong-∙∙ (fst (joinify g'))
-       (push base base) (sym (push a base)) (push a b)
-       ∙ cong (cong g (merid north) ∙∙_∙∙ cong g (merid (S¹×S¹→S² a b)))
-              (cong (cong g) (cong sym (cong merid (S¹×S¹→S²rUnit a))))
-       ∙  ((λ i → (cong g (λ j → merid north (j ∧ ~ i)))
-       ∙∙ (cong g (λ j → merid north (~ j ∧ ~ i)))
-       ∙∙ cong g (merid (S¹×S¹→S² a b)))
-       ∙ sym (lUnit (cong g (merid (S¹×S¹→S² a b)))))
-
-  main : (a b : S¹)
-    → PathP (λ i → fp (~ i) ≡ (sym gp ∙ cong g (merid north)) i)
-            ((sym fp ∙∙ cong f (σ₂ (S¹×S¹→S² a b)) ∙∙ fp)
-           ∙ (sym gp ∙∙ cong g (σ₂ (S¹×S¹→S² a b)) ∙∙ gp))
-            ((cong (fst (joinify f')) (push a b ∙ sym (push base b))
-          ∙∙ fp ∙ sym gp
-          ∙∙ cong (fst (joinify g'))
-              (push base base ∙∙ sym (push a base) ∙∙ push a b)))
-  main a b =
-    ((λ i j → hcomp (λ k → λ {(i = i0) → (((λ j → fp (~ j ∧ k))
-                                          ∙∙ cong f (σ₂ (S¹×S¹→S² a b))
-                                          ∙∙ fp)
-                                          ∙ (sym gp
-                                          ∙∙ cong g (σ₂ (S¹×S¹→S² a b))
-                                          ∙∙ λ j → gp (j ∧ k))) j
-                              ; (i = i1) → ((cong f (merid (S¹×S¹→S² a b))
-                                           ∙ sym (cong f (merid north)))
-                                          ∙∙ fp ∙ sym gp
-                                          ∙∙ cong g (merid (S¹×S¹→S² a b))) j
-                              ; (j = i0) → fp (~ i ∧ k)
-                              ; (j = i1) → compPath-filler'
-                                           (sym gp) (cong g (merid north)) k i})
-                     (main-helper a b i j)))
-    ▷ λ i →
-      cong-∙ (fst (joinify f')) (push a b) (sym (push base b)) (~ i)
-      ∙∙ fp ∙ sym gp
-      ∙∙ main-helper₂ a b (~ i)
-
-
-
--- Group structure on π₃*
--- todo: remove connectivity assumption
-module _ (A : Pointed ℓ) (con : (isConnected 3 (typ A))) where
-  π₃*Iso : Iso (typ (π'Gr 2 A)) ∥ (join S¹ S¹ , inl base) →∙ A ∥₂
-  fun π₃*Iso = sMap joinify
-  inv π₃*Iso = sMap disjoin
-  rightInv π₃*Iso =
-    sElim (λ _ → isSetPathImplicit)
-      λ f → to3ConnectedId
-        con (funExt λ x → cong (fst f) (Iso.leftInv (IsoSphereJoin 1 1) x))
-  leftInv π₃*Iso =
-    sElim (λ _ → isSetPathImplicit)
-      λ f → to3ConnectedId
-        con (funExt (λ x → cong (fst f) (Iso.rightInv (IsoSphereJoin 1 1) x)))
-
-  π₃* : Group ℓ
-  π₃* = InducedGroupFromPres·
-          (π'Gr 2 A)
-          (sRec2 squash₂ (λ x y → ∣ x +join y ∣₂))
-          (isoToEquiv π₃*Iso)
-          (sElim2 (λ _ _ → isSetPathImplicit) (λ f g → cong ∣_∣₂ (+join≡∙Π f g)))
-
-  π₃≅π₃* : GroupEquiv (π'Gr 2 A) π₃*
-  π₃≅π₃* =
-    InducedGroupEquivFromPres· (π'Gr 2 A) (sRec2 squash₂ (λ x y → ∣ x +join y ∣₂))
-      (isoToEquiv π₃*Iso)
-      (sElim2 (λ _ _ → isSetPathImplicit) (λ f g → cong ∣_∣₂ (+join≡∙Π f g)))
-
-
--- Induced homomorphisms (A →∙ B) → (π₃*(A) → π₃*(B))
--- todo: remove connectivity assumptions
-module _ (conA : (isConnected 3 (typ A))) (conB : (isConnected 3 (typ B)))
-         (f : A →∙ B) where
-  postCompπ₃* : GroupHom (π₃* A conA) (π₃* B conB)
-  fst postCompπ₃* = sMap (f ∘∙_)
-  snd postCompπ₃* =
-    makeIsGroupHom
-      (sElim2 (λ _ _ → isSetPathImplicit)
-        λ h g → to3ConnectedId conB
-          (funExt λ { (inl x) → refl
-                    ; (inr x) → refl
-                    ; (push a b i) j →
-           (cong-∙∙ (fst f)
-                    (cong (fst h) ((push a b ∙ (sym (push base b)))))
-                    (snd h ∙ (sym (snd g)))
-                    (cong (fst g) ((push base base
-                               ∙∙ (sym (push a base))
-                               ∙∙ push a b)))
-          ∙ cong (cong (fst f)
-                   (cong (fst h) (push a b ∙ (sym (push base b))))
-                    ∙∙_∙∙
-                   cong (fst f ∘ fst g)
-                     ((push base base ∙∙ (sym (push a base)) ∙∙ push a b)))
-                 (cong-∙ (fst f) (snd h) (sym (snd g))
-                 ∙ λ j → compPath-filler (cong (fst f) (snd h)) (snd f) j
-                        ∙ sym (compPath-filler
-                               (cong (fst f) (snd g)) (snd f) j))) j i}))
-
--- Induced iso (A ≃∙ B) → π₃*(A) ≅ π₃*(B)
--- todo: remove connectivity assumptions
-module _ (conA : (isConnected 3 (typ A))) (conB : (isConnected 3 (typ B)))
-         (f : A ≃∙ B) where
-  postCompπ₃*Equiv : GroupEquiv (π₃* A conA) (π₃* B conB)
-  fst postCompπ₃*Equiv = isoToEquiv h
-    where
-    h : Iso (π₃* A conA .fst) (π₃* B conB .fst)
-    fun h = fst (postCompπ₃* conA conB (≃∙map f))
-    inv h = fst (postCompπ₃* conB conA (≃∙map (invEquiv∙ f)))
-    rightInv h =
-      sElim (λ _ → isSetPathImplicit)
-        λ g → to3ConnectedId conB (funExt λ x → secEq (fst f) (fst g x))
-    leftInv h =
-      sElim (λ _ → isSetPathImplicit)
-        λ g → to3ConnectedId conA (funExt λ x → retEq (fst f) (fst g x))
-  snd postCompπ₃*Equiv = snd (postCompπ₃* conA conB (≃∙map f))
 
 -- The relevant groups (in order of the iso π₃(S²) ≅ ℤ)
 π₃S² = π'Gr 2 (S₊∙ 2)
 
-π₃*S² = π₃* (S₊∙ 2) (sphereConnected 2)
+π₃*S² = π*Gr 1 1 (S₊∙ 2)
 
-π₃*joinS¹S¹ = π₃* (join S¹ S¹ , inl base) con-joinS¹S¹
+π₃*joinS¹S¹ = π*Gr 1 1 (join∙ (S₊∙ 1) (S₊∙ 1))
 
-π₃*S³ = π₃* (S₊∙ 3) connS³
+π₃*S³ = π*Gr 1 1 (S₊∙ 3)
 
 π₃S³ = π'Gr 2 (S₊∙ 3)
 
+π₃≅π₃* : {A : Pointed₀} → GroupEquiv (π'Gr 2 A) (π*Gr 1 1 A)
+π₃≅π₃* {A = A} = invGroupEquiv (GroupIso→GroupEquiv (π*Gr≅π'Gr 1 1 A))
+
 {- Goal now:  Show that
    (η : π₃(S²))
 ↦ (η₁ : π₃*(S²))
@@ -383,13 +182,13 @@ Hence, there is an is an iso π₃(S²) ≅ ℤ taking η to
 -}
 
 -- Underlying functions of (some of) the ηs
-η₁-raw : (join S¹ S¹ , inl base) →∙ S₊∙ 2
+η₁-raw : join∙ S¹∙ S¹∙ →∙ S₊∙ 2
 fst η₁-raw (inl x) = north
 fst η₁-raw (inr x) = north
 fst η₁-raw (push a b i) = (σ₁ b ∙ σ₁ a) i
 snd η₁-raw = refl
 
-η₂-raw : (join S¹ S¹ , inl base) →∙ (join S¹ S¹ , inl base)
+η₂-raw : join∙ S¹∙ S¹∙ →∙ join∙ S¹∙ S¹∙
 fst η₂-raw (inl x) = inr (invLooper x)
 fst η₂-raw (inr x) = inr x
 fst η₂-raw (push a b i) =
@@ -397,7 +196,7 @@ fst η₂-raw (push a b i) =
   ∙ push (b * invLooper a) b) i
 snd η₂-raw = sym (push base base)
 
-η₃-raw : (join S¹ S¹ , inl base) →∙ S₊∙ 3
+η₃-raw : join∙ S¹∙ S¹∙ →∙ S₊∙ 3
 fst η₃-raw (inl x) = north
 fst η₃-raw (inr x) = north
 fst η₃-raw (push a b i) =
@@ -420,7 +219,7 @@ snd η₃-raw = refl
 
 -- π₃S²≅π₃*S²
 π₃S²→π₃*S² : GroupEquiv π₃S² π₃*S²
-π₃S²→π₃*S² = π₃≅π₃* (S₊∙ 2) (sphereConnected 2)
+π₃S²→π₃*S² = GroupIso→GroupEquiv (invGroupIso (π*Gr≅π'Gr 1 1 (S₊∙ 2)))
 
 -- Time for π₃*(S¹ * S¹) ≅ π₃*S².
 -- We have this iso already, but slightly differently stated,
@@ -433,9 +232,7 @@ Hopfσ (inr x) = north
 Hopfσ (push a b i) = σ₁ (invLooper a * b) i
 
 π₃*joinS¹S¹→π₃*S² : GroupHom π₃*joinS¹S¹ π₃*S²
-π₃*joinS¹S¹→π₃*S² =
-  postCompπ₃* con-joinS¹S¹ (sphereConnected 2)
-    (Hopfσ , refl)
+π₃*joinS¹S¹→π₃*S² = π*∘∙Hom 1 1 (Hopfσ , refl)
 
 π₃*joinS¹S¹≅π₃*S² : GroupEquiv π₃*joinS¹S¹ π₃*S²
 fst (fst π₃*joinS¹S¹≅π₃*S²) = fst π₃*joinS¹S¹→π₃*S²
@@ -444,8 +241,7 @@ snd (fst π₃*joinS¹S¹≅π₃*S²) =
   where
   π₃*joinS¹S¹→π₃*S²' : GroupHom π₃*joinS¹S¹ π₃*S²
   π₃*joinS¹S¹→π₃*S²' =
-    postCompπ₃* con-joinS¹S¹ (sphereConnected 2)
-      (fst ∘ JoinS¹S¹→TotalHopf , refl)
+    π*∘∙Hom 1 1 (fst ∘ JoinS¹S¹→TotalHopf , refl)
 
   isEquivπ₃*joinS¹S¹→π₃*S²' : isEquiv (fst π₃*joinS¹S¹→π₃*S²')
   isEquivπ₃*joinS¹S¹→π₃*S²' =
@@ -458,10 +254,10 @@ snd (fst π₃*joinS¹S¹≅π₃*S²) =
         (λ i → GroupHom
                 (GroupPath π₃*joinS¹S¹ π₃S³ .fst
                   (compGroupEquiv
-                   (invGroupEquiv (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹))
+                   (invGroupEquiv π₃≅π₃*)
                    (π'Iso 2 (isoToEquiv (IsoSphereJoin 1 1) , refl))) i)
                 (GroupPath π₃*S² π₃S² .fst
-                  (invGroupEquiv (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) i))
+                  (invGroupEquiv π₃≅π₃*) i))
          π₃*joinS¹S¹→π₃*S²'
          (fst (fst GrEq) , snd GrEq)
     help =
@@ -469,20 +265,21 @@ snd (fst π₃*joinS¹S¹≅π₃*S²) =
         (funExt
           λ f → (λ i
            → transportRefl
-              ((invGroupEquiv (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) .fst .fst
+              ((invGroupEquiv (π₃≅π₃*)) .fst .fst
                 (fst π₃*joinS¹S¹→π₃*S²' (
-                  ((fst (fst (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹)))
+                  ((fst (fst π₃≅π₃*))
                   (invEq (fst (π'Iso 2 (isoToEquiv (IsoSphereJoin 1 1) , refl)))
                      (transportRefl f i)))))) i)
-              ∙ main f))
+              ∙ main f
+              ))
 
       where
-      main : (f : _) → invEquiv (fst (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) .fst
-        (fst π₃*joinS¹S¹→π₃*S²'
-         (invEq
-          (invEquiv (fst (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹)))
-          (invEq (fst (π'Iso 2 (isoToEquiv Iso-joinS¹S¹-S³ , (λ _ → north))))
-           f)))
+      main : (f : _) → invEquiv (fst π₃≅π₃*) .fst
+                          (fst π₃*joinS¹S¹→π₃*S²'
+                           (fst (fst π₃≅π₃*)
+                            (invEq
+                             (fst (π'Iso 2 (isoToEquiv (IsoSphereJoin 1 1) , (λ _ → north))))
+                             f)))
         ≡ fst GrEq .fst f
       main = sElim (λ _ → isSetPathImplicit)
         λ f → to3ConnectedId (sphereConnected 2)
@@ -509,13 +306,11 @@ snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S²
 -- π₃*(S³) ≅ π₃*(S¹ * S¹)
 π₃*S³≅π₃*joinS¹S¹ : GroupEquiv π₃*S³ π₃*joinS¹S¹
 π₃*S³≅π₃*joinS¹S¹ =
-  postCompπ₃*Equiv
-    connS³ con-joinS¹S¹
-      (isoToEquiv (invIso (IsoSphereJoin 1 1)) , refl)
+  π*∘∙Equiv 1 1 (isoToEquiv (invIso (IsoSphereJoin 1 1)) , refl)
 
 -- π₃(S³)≅π₃*(S³)
 π₃S³≅π₃*S³ : GroupEquiv π₃S³ π₃*S³
-π₃S³≅π₃*S³ = π₃≅π₃* (S₊∙ 3) connS³
+π₃S³≅π₃*S³ = π₃≅π₃*
 
 η↦η₁ :  fst (fst π₃S²→π₃*S²) η ≡ η₁
 η↦η₁ = to3ConnectedId (sphereConnected 2)
@@ -576,42 +371,27 @@ snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S²
 η₂↦η₃ : invEq (fst π₃*S³≅π₃*joinS¹S¹) η₂ ≡ η₃
 η₂↦η₃ =
   to3ConnectedId connS³
-   (funExt λ x → sym (joinS¹S¹→S³σ≡ (fst η₂-raw x))
-                ∙ lem x)
+   (funExt λ x → lem x)
   where
-  joinS¹S¹→S³σ : join S¹ S¹ → S₊ 3
-  joinS¹S¹→S³σ (inl x) = north
-  joinS¹S¹→S³σ (inr x) = north
-  joinS¹S¹→S³σ (push a b i) = σ₂ (S¹×S¹→S² a b) i
-
-  joinS¹S¹→S³σ≡ : (x : _) → joinS¹S¹→S³σ x ≡ joinS¹S¹→S³ x
-  joinS¹S¹→S³σ≡ (inl x) = refl
-  joinS¹S¹→S³σ≡ (inr x) = merid north
-  joinS¹S¹→S³σ≡ (push a b i) j =
-    compPath-filler (merid (S¹×S¹→S² a b)) (sym (merid north)) (~ j) i
-
-  lem : (x : _) → joinS¹S¹→S³σ (fst η₂-raw x) ≡ fst η₃-raw x
+  lem : (x : _) → joinS¹S¹→S³ (fst η₂-raw x) ≡ fst η₃-raw x
   lem (inl x) = refl
   lem (inr x) = refl
   lem (push a b i) j = main j i
     where
     left-lem : σ₂ (S¹×S¹→S² (b * invLooper a) (invLooper a))
              ≡ σ₂ (S¹×S¹→S² a b)
-    left-lem = cong σ₂ (S¹×S¹→S²-Distr b (invLooper a)
-             ∙ sym (S¹×S¹→S²-antiComm a b))
+    left-lem = cong σ₂ (⌣₁,₁-distr' b (invLooper a)
+                      ∙ ⌣Sinvᵣ b a
+                      ∙ sym (transportRefl _)
+                      ∙ sym (comm⌣S a b))
 
     right-lem : σ₂ (S¹×S¹→S² (b * invLooper a) b) ≡ sym (σ₂ (S¹×S¹→S² a b))
-    right-lem =
-         cong σ₂ ((cong (λ x → S¹×S¹→S² x b) (commS¹ b (invLooper a))
-                 ∙ S¹×S¹→S²-Distr (invLooper a) b)
-                 ∙∙ S¹×S¹→S²-antiComm (invLooper a) b
-                 ∙∙ invSusp∘S¹×S¹→S² b (invLooper a))
-      ∙∙ σ-invSphere 1 (S¹×S¹→S² b (invLooper a))
-      ∙∙ cong (sym ∘ σ₂) (sym (S¹×S¹→S²-antiComm a b))
-
-    main : cong (joinS¹S¹→S³σ ∘ fst η₂-raw) (push a b)
+    right-lem = cong σ₂ (⌣₁,₁-distr (invLooper a) b ∙ ⌣Sinvₗ a b)
+              ∙ σ-invSphere 1 (a ⌣S b)
+
+    main : cong (joinS¹S¹→S³ ∘ fst η₂-raw) (push a b)
         ≡ sym (σ₂ (S¹×S¹→S² a b)) ∙ sym (σ₂ (S¹×S¹→S² a b))
-    main = cong-∙ joinS¹S¹→S³σ
+    main = cong-∙ joinS¹S¹→S³
             (sym (push (b * invLooper a) (invLooper a)))
             (push (b * invLooper a) b)
          ∙ cong₂ _∙_ (cong sym left-lem) right-lem
@@ -640,7 +420,15 @@ snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S²
     to3ConnectedId connS³
       (funExt λ { (inl x) → refl
                 ; (inr x) → refl
-                ; (push a b i) → refl})
+                ; (push a b i) j → help a b j i
+                })
+    where
+    help : (a b : S¹)
+      → cong (fst (inv (Iso-JoinMap-SphereMap 1 1) (-Π (idfun∙ (S₊∙ 3))))) (push a b)
+       ≡ σS (a ⌣S b) ⁻¹
+    help a b = cong-∙ (fst (-Π (idfun∙ (S₊∙ 3)))) (merid (a ⌣S b)) (merid north ⁻¹)
+             ∙ cong₂ _∙_ refl (rCancel (merid north))
+             ∙ sym (rUnit (σS (a ⌣S b) ⁻¹))
 
   η₃/2+η₃/2≡η₃ : η₃/2 +π₃* η₃/2 ≡ η₃
   η₃/2+η₃/2≡η₃ =
@@ -649,23 +437,21 @@ snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S²
                 ; (inr x) → refl
                 ; (push a b i) → λ j → lem a b j i})
     where
-    lem : (a b : S¹) → cong (fst (η₃-raw/2 +join η₃-raw/2)) (push a b)
+    pre : (a b : S¹) → cong (fst η₃-raw/2) (ℓS a b) ≡ σS (a ⌣S b) ⁻¹
+    pre a b = cong-∙ (fst η₃-raw/2) _ _
+            ∙ cong₂ _∙_
+                (cong sym (rCancel (merid north)))
+                (cong-∙∙ (fst η₃-raw/2) _ _ _
+                ∙ (λ i →
+                        (cong σ₂ (IdL⌣S {n = 1} {1} a) ∙ (rCancel (merid north))) i
+                      ∙∙ σS (a ⌣S b) ⁻¹
+                      ∙∙ rCancel (merid north) i)
+                ∙ sym (rUnit _))
+            ∙ sym (lUnit _)
+
+    lem : (a b : S¹) → cong (fst (η₃-raw/2 +* η₃-raw/2)) (push a b)
                       ≡ cong (fst η₃-raw) (push a b)
-    lem a b = (λ i → cong-∙ (fst η₃-raw/2) (push a b) (sym (push base b)) i
-                   ∙∙ rUnit refl (~ i)
-                   ∙∙ cong-∙∙ (fst η₃-raw/2)
-                        (push base base) (sym (push a base)) (push a b) i)
-           ∙∙ (λ i → (sym (σ₂ (S¹×S¹→S² a b)) ∙ rCancel (merid north) i)
-                   ∙∙ refl
-                   ∙∙ (sym (rCancel (merid north) i)
-                   ∙∙ (cong σ₂ (S¹×S¹→S²rUnit a) ∙ rCancel (merid north)) i
-                   ∙∙ sym (σ₂ (S¹×S¹→S² a b))))
-           ∙∙ ((λ i → rUnit (sym (σ₂ (S¹×S¹→S² a b))) (~ i)
-                    ∙∙ refl
-                    ∙∙ lUnit (sym (σ₂ (S¹×S¹→S² a b))) (~ i))
-             ∙ λ i → (λ j → σ₂ (S¹×S¹→S² a b) (i ∨ ~ j))
-                   ∙∙ (λ j → σ₂ (S¹×S¹→S² a b) (i ∧ ~ j))
-                   ∙∙ sym (σ₂ (S¹×S¹→S² a b)))
+    lem a b = cong₂ _∙_ (sym (rUnit _) ∙ pre a b) (sym (rUnit _) ∙ pre a b)
 
 -- Agda is very keen on expanding things, so we make an abstract
 -- summary of the main lemmas above
@@ -789,7 +575,7 @@ snd connSuspS² =
            λ i j → ∣ merid base (i ∧ j) ∣ₕ
 
 π₃*S³' : Group₀
-π₃*S³' = π₃* (Susp∙ S²) (isConnectedSubtr 3 1 connSuspS²)
+π₃*S³' = π*Gr 1 1 (Susp∙ S²)
 
 -- The version of η₃ we have been able to compute lies in π₃*S³'
 η₃'-raw : (join S¹ S¹ , inl base) →∙ (Susp S² , north)
@@ -802,10 +588,13 @@ snd η₃'-raw = refl
 η₃' : π₃*S³' .fst
 η₃' = ∣ η₃'-raw ∣₂
 
+altS²IsoSuspS¹ : Iso S² SuspS¹
+altS²IsoSuspS¹ = compIso invS²Iso S²IsoSuspS¹
+
 -- We first have to show (manually) that the following iso sends η₃ to η₃'
 π₃*S³≅π₃*S³' : GroupEquiv π₃*S³ π₃*S³'
-π₃*S³≅π₃*S³' = postCompπ₃*Equiv _ _
-        (isoToEquiv (congSuspIso (invIso S²IsoSuspS¹))
+π₃*S³≅π₃*S³' = π*∘∙Equiv 1 1 -- _ _ -- postCompπ₃*Equiv _ _
+        (isoToEquiv (congSuspIso (invIso altS²IsoSuspS¹))
        , refl)
 
 π₃*S³≅π₃*S³'-pres-η₃ : fst (fst π₃*S³≅π₃*S³') η₃ ≡ η₃'
@@ -813,21 +602,24 @@ snd η₃'-raw = refl
   cong ∣_∣₂
     (ΣPathP ((funExt (λ { (inl x) → refl
                         ; (inr x) → refl
-                        ; (push a b i) j → lem a b j i}))
+                        ; (push a b i) j → lem a b j i
+                        }))
                         , sym (rUnit refl)))
   where
   lem : (a b : S¹)
-    → cong (suspFun SuspS¹→S²)
+    → cong (suspFun (invS² ∘ SuspS¹→S²))
             (sym (σ₂ (S¹×S¹→S² a b)) ∙ sym (σ₂ (S¹×S¹→S² a b)))
-    ≡ (σ (S² , base) (S¹×S¹→S²' a b) ∙ σ (S² , base) (S¹×S¹→S²' a b))
+    ≡ (σ (S² , base) (S¹×S¹→S²' a b) ∙ (σ (S² , base) (S¹×S¹→S²' a b)))
   lem a b =
-      cong-∙ (suspFun SuspS¹→S²)
+      cong-∙ (suspFun (invS² ∘ SuspS¹→S²))
              (sym (σ₂ (S¹×S¹→S² a b))) (sym (σ₂ (S¹×S¹→S² a b)))
     ∙ cong (λ x → x ∙ x)
            (cong sym (cong-∙
-             (suspFun SuspS¹→S²) (merid (S¹×S¹→S² a b)) (sym (merid north)))
-          ∙ cong sym (cong (σ S²∙) (SuspS¹→S²-S¹×S¹→S² a b))
-          ∙ sym (S¹×S¹→S²-sym a b))
+             (suspFun (invS² ∘ SuspS¹→S²)) (merid (S¹×S¹→S² a b)) (sym (merid north)))
+         ∙ cong sym (cong (σ S²∙)
+                    (cong invS² (SuspS¹→S²-S¹×S¹→S² a b)
+                    ∙ S¹×S¹→S²-anticomm a b))
+         ∙ sym (S¹×S¹→S²-sym a b))
 
 -- After this, we want to establish an iso π₃*S³'≅ℤ which is nice enough to compute.
 -- This requires a bit of work and some hacking.
@@ -942,26 +734,28 @@ snd π₁S¹→∙ΩS³'≅π₃*S³' =
             λ f g → cong ∣_∣₂
               (ΣPathP ((funExt (λ { (inl x) → refl
                                   ; (inr x) → refl
-                                  ; (push a b i) j → main f g a b j i}))
+                                  ; (push a b i) j → main f g a b j i
+                                  }))
                       , refl)))
+
   where
+  lem1 : (f : S₊∙ 1 →∙ (S₊∙ 1 →∙ Ω (Susp∙ S²) ∙)) (a b : S¹)
+      → congS (fst (map← f)) (ℓ* S¹∙ S¹∙ a b) ≡ fst f a .fst b
+  lem1 f a b = cong-∙ (fst (map← f)) _ _
+            ∙ cong₂ _∙_ (fst f base .snd)
+                    ((cong-∙∙ (fst (map← f)) _ _ _)
+                  ∙ (λ j → sym (fst f a .snd j)
+                         ∙∙ fst f a .fst b
+                         ∙∙ sym (snd f j .fst b))
+                  ∙ sym (rUnit _))
+            ∙ sym (lUnit _)
+
   main : (f g : S₊∙ 1 →∙ (S₊∙ 1 →∙ Ω (Susp∙ S²) ∙)) (a b : S¹)
     → cong (fst (map← (∙Π f g))) (push a b)
-    ≡ cong (fst (map← f +join map← g)) (push a b)
-  main f g a b = (main-lem a b
-            ∙ (λ i → (λ j → fst f a .fst b (j ∧ i))
-                   ∙∙ ((λ j → fst f a .fst b (j ∨ i)))
-                   ∙∙ fst g a .fst b))
-            ∙ λ i → (rUnit (fst f a .fst b) ∙ cong (fst f a .fst b ∙_)
-                       (cong sym (sym (funExt⁻ (cong fst (snd f)) b)))
-                      ∙ sym (cong-∙ (map← f .fst) (push a b) (sym (push base b)))) i
-                  ∙∙ rUnit refl i
-                  ∙∙ ((lUnit (fst g a .fst b)
-            ∙ (λ i → fst g base .snd (~ i)
-                   ∙∙ sym (fst g a .snd (~ i))
-                   ∙∙ cong (map← g .fst) (push a b)))
-                    ∙ (sym (cong-∙∙ (map← g .fst)
-                            (push base base) (sym (push a base)) (push a b)))) i
+    ≡ cong (fst (_+*_ {A = S¹∙} {B = S¹∙} (map← f) (map← g))) (push a b)
+  main f g a b = main-lem a b
+               ∙ cong₂ _∙_ (sym (lem1 f a b) ∙ rUnit _)
+                           (sym (lem1 g a b) ∙ rUnit _)
     where
     JLem : ∀ {ℓ} {A : Type ℓ} (* : A)
               (fab : * ≡ *) (fabrefl : refl ≡ fab)
diff --git a/Cubical/Homotopy/Hopf.agda b/Cubical/Homotopy/Hopf.agda
index acb0dbb140..061b4d9fb6 100644
--- a/Cubical/Homotopy/Hopf.agda
+++ b/Cubical/Homotopy/Hopf.agda
@@ -19,7 +19,7 @@ open import Cubical.Data.Int hiding (_·_)
 
 open import Cubical.HITs.Pushout.Flattening
 open import Cubical.HITs.Pushout
-open import Cubical.HITs.Sn hiding (joinS¹S¹→S³)
+open import Cubical.HITs.Sn
 open import Cubical.HITs.Susp
 open import Cubical.HITs.S1
 open import Cubical.HITs.S2
diff --git a/Cubical/Homotopy/HopfInvariant/Brunerie.agda b/Cubical/Homotopy/HopfInvariant/Brunerie.agda
index 7d7a13d504..2ebb7d472f 100644
--- a/Cubical/Homotopy/HopfInvariant/Brunerie.agda
+++ b/Cubical/Homotopy/HopfInvariant/Brunerie.agda
@@ -391,8 +391,7 @@ Brunerie'≡2 = BrunerieNumLem.main (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1) Hⁿ
 -- number in Brunerie (2016)
 Brunerie'≡Brunerie : [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π' ≡ ∣ fold∘W , refl ∣₂
 Brunerie'≡Brunerie =
-    cong ∣_∣₂ ([]≡[]₂ (idfun∙ (S₊∙ 2)) (idfun∙ (S₊∙ 2)) )
-  ∙ sym fold∘W≡Whitehead
+    sym fold∘W≡Whitehead
   ∙ cong ∣_∣₂ (∘∙-idˡ (fold∘W , refl))
 
 -- And we get the main result
diff --git a/Cubical/Homotopy/HopfInvariant/HopfMap.agda b/Cubical/Homotopy/HopfInvariant/HopfMap.agda
index d6dd589af1..4f01dc2f75 100644
--- a/Cubical/Homotopy/HopfInvariant/HopfMap.agda
+++ b/Cubical/Homotopy/HopfInvariant/HopfMap.agda
@@ -48,6 +48,7 @@ open import Cubical.HITs.Pushout as Pushout
 open import Cubical.HITs.Join
 open import Cubical.HITs.S1 renaming (_·_ to _*_)
 open import Cubical.HITs.Sn
+open import Cubical.HITs.Sn.Multiplication
 open import Cubical.HITs.Susp
 open import Cubical.HITs.Truncation
   renaming (rec to trRec ; elim to trElim)
diff --git a/Cubical/Homotopy/Whitehead.agda b/Cubical/Homotopy/Whitehead.agda
index 2daec9e530..fbdffd6ed4 100644
--- a/Cubical/Homotopy/Whitehead.agda
+++ b/Cubical/Homotopy/Whitehead.agda
@@ -15,6 +15,7 @@ open import Cubical.Data.Unit
 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
@@ -25,6 +26,25 @@ open import Cubical.Homotopy.Loopspace
 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)
@@ -35,63 +55,100 @@ joinTo⋁ {A = A} {B = B} (push a b i) =
   ∙∙ sym (push tt)
   ∙∙ λ i → inl (σ A a i)) i
 
--- Whitehead product (main definition)
-[_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+[_∣_]comp : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
        → (S₊∙ (suc n) →∙ X)
        → (S₊∙ (suc m) →∙ X)
        → S₊∙ (suc (n + m)) →∙ X
-fst ([_∣_] {X = X} {n = n} {m = m} f g) x =
-  _∨→_ (f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
-        (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))
-        (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}
-          (inv (IsoSphereJoin n m) x))
-snd ([_∣_] {n = n} {m = m} f g) =
-  cong (_∨→_ (f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
-       (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m)))
-       (cong (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}) (IsoSphereJoin⁻Pres∙ n m))
-    ∙ cong (fst g) (IsoSucSphereSusp∙ m)
-    ∙ snd g
-
--- For Sⁿ, Sᵐ with n, m ≥ 2, we can avoid some bureaucracy. We make
--- a separate definition and prove it equivalent.
-[_∣_]-pre : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (S₊∙ (suc (suc n)) →∙ X)
-       → (S₊∙ (suc (suc m)) →∙ X)
-       → join (typ (S₊∙ (suc n))) (typ (S₊∙ (suc m))) → fst X
-[_∣_]-pre {n = n} {m = m} f g x =
-  _∨→_ f g
-        (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
-        x)
-
-[_∣_]₂ : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (S₊∙ (suc (suc n)) →∙ X)
-       → (S₊∙ (suc (suc m)) →∙ X)
-       → S₊∙ (suc ((suc n) + (suc m))) →∙ X
-fst ([_∣_]₂ {n = n} {m = m} f g) x =
-  [ f ∣ g ]-pre (inv (IsoSphereJoin (suc n) (suc m)) x)
-snd ([_∣_]₂ {n = n} {m = m} f g) =
-    cong ([ f ∣ g ]-pre) (IsoSphereJoin⁻Pres∙ (suc n) (suc m))
-  ∙ snd g
-
-[]≡[]₂ : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (f : (S₊∙ (suc (suc n)) →∙ X))
-       → (g : (S₊∙ (suc (suc m)) →∙ X))
-       → [ f ∣ g ] ≡ [ f ∣ g ]₂
-[]≡[]₂ {n = n} {m = m} f g =
-  ΣPathP (
-    (λ i x → _∨→_ (∘∙-idˡ f i)
-                    (∘∙-idˡ g i)
-                (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
-                 (inv (IsoSphereJoin (suc n) (suc m)) x)))
-  , (cong (cong (_∨→_ (f ∘∙ idfun∙ _)
-                       (g ∘∙ idfun∙ _))
-       (cong (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)})
-             (IsoSphereJoin⁻Pres∙ (suc n) (suc m))) ∙_)
-                (sym (lUnit (snd g)))
-  ◁ λ j → (λ i → _∨→_ (∘∙-idˡ f j)
-                        (∘∙-idˡ g j)
-           ( joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
-          ((IsoSphereJoin⁻Pres∙ (suc n) (suc m)) i))) ∙ snd g))
+[_∣_]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))
+       → [ f ∣ g ]comp ≡ [ f ∣ g ]
+[]comp≡[] {X = X} {n = n} {m} f g =
+  cong (_∘∙ (sphere→Join n m , IsoSphereJoin⁻Pres∙ n m)) (main n m f g)
+    where
+    ∨fun : {n m : ℕ} (f : (S₊∙ (suc n) →∙ X)) (g : (S₊∙ (suc m) →∙ X))
+      → ((_ , inl north) →∙ X)
+    ∨fun {n = n} {m} f g =
+       ((f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n)) ∨→
+       (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
+    main n m f g =
+      ΣPathP ((funExt (λ { (inl x) → rp
+                         ; (inr x) → lp
+                         ; (push a b i) j → pushcase a b j i}))
+          , ((cong₂ _∙_ (symDistr _ _) refl
+          ∙ sym (assoc _ _ _)
+          ∙ cong (rp ∙_) (rCancel _)
+          ∙ sym (rUnit rp))
+          ◁ λ i j → rp (i ∨ j)))
+      where
+      lp = cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f
+      rp = cong (fst g) (IsoSucSphereSusp∙ m) ∙ snd g
+
+      help : (n : ℕ) (a : _)
+        → Square (cong (inv (IsoSucSphereSusp n)) (σ (S₊∙ n) a)) (σS a)
+                  (IsoSucSphereSusp∙ n) (IsoSucSphereSusp∙ n)
+      help zero a = cong-∙ SuspBool→S¹ (merid a) (sym (merid (pt (S₊∙ zero))))
+                  ∙ sym (rUnit _)
+      help (suc n) a = refl
+
+      ∙∙Distr∙ : ∀ {ℓ} {A : Type ℓ} {x y z w u : A}
+                 {p : x ≡ y} {q : y ≡ z} {r : z ≡ w} {s : w ≡ u}
+               → p ∙∙ q ∙ r ∙∙ s ≡ ((p ∙ q) ∙ r ∙ s)
+      ∙∙Distr∙ = doubleCompPath≡compPath _ _ _
+               ∙ assoc _ _ _
+               ∙ cong₂ _∙_ (assoc _ _ _) refl
+               ∙ sym (assoc _ _ _)
+
+
+      pushcase : (a : S₊ n) (b : S₊ m)
+        → Square (cong (∨fun f g .fst ∘ joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}) (push a b))
+                  (cong (fst [ f ∣ g ]-pre) (push a b))
+                  rp lp
+      pushcase a b =
+        (cong-∙∙ (∨fun f g .fst) _ _ _
+        ∙ (λ i → cong (fst g) (PathP→compPathR∙∙ (help _ b) i)
+              ∙∙ symDistr lp (sym rp) i
+              ∙∙ cong (fst f) (PathP→compPathR∙∙ (help _ a) i))
+        ∙ (λ i → cong (fst g)
+                      (IsoSucSphereSusp∙ m
+                     ∙∙ σS b
+                     ∙∙ (λ j → IsoSucSphereSusp∙ m (~ j ∨ i)))
+              ∙∙ compPath-filler' (cong (fst g) (IsoSucSphereSusp∙ m)) (snd g) (~ i)
+               ∙ sym (compPath-filler' (cong (fst f) (IsoSucSphereSusp∙ n)) (snd f) (~ i))
+              ∙∙ cong (fst f)
+                      ((λ j → IsoSucSphereSusp∙ n (i ∨ j))
+                      ∙∙ σS a
+                      ∙∙ sym (IsoSucSphereSusp∙ n))))
+       ◁ compPathR→PathP∙∙
+           ( ∙∙Distr∙
+          ∙ cong₂ _∙_ (cong₂ _∙_ (cong (cong (fst g)) (sym (compPath≡compPath' _ _)))
+                                 refl)
+                      refl
+          ∙ cong₂ _∙_ (cong (_∙ snd g) (cong-∙ (fst g) (IsoSucSphereSusp∙ m) (σS b))
+                                     ∙ sym (assoc _ _ _))
+                      (cong (sym (snd f) ∙_)
+                        (cong-∙ (fst f) (σS a)
+                          (sym (IsoSucSphereSusp∙ n)))
+                         ∙ assoc _ _ _)
+          ∙ sym ∙∙Distr∙
+          ∙ cong₃ _∙∙_∙∙_ refl (cong₂ _∙_ refl (compPath≡compPath' _ _)) refl
+         ∙ λ i → compPath-filler (cong (fst g) (IsoSucSphereSusp∙ m)) (snd g) i
+               ∙∙ ((λ j → snd g (~ j ∧ i)) ∙∙ cong (fst g) (σS b) ∙∙ snd g)
+                ∙ (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 : ℕ}
diff --git a/Cubical/Papers/Pi4S3-JournalVersion.agda b/Cubical/Papers/Pi4S3-JournalVersion.agda
index 212a444a0d..fc4281db18 100644
--- a/Cubical/Papers/Pi4S3-JournalVersion.agda
+++ b/Cubical/Papers/Pi4S3-JournalVersion.agda
@@ -165,7 +165,7 @@ module ExactSeq = πLES
 open Suspensions renaming (toSusp to σ)
 
 -- Proposition 3.4: Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹
-open Spheres using (IsoSphereJoin)
+open SMult using (IsoSphereJoin)
 
 -- Definition 3.5 and Proposition 3.6 (Hopf map),
 -- Phrased somewhat differently in the paper.
@@ -243,7 +243,7 @@ open James₁ using (IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅)
 
 -- Definition 4.8: W + whitehead product
 W = joinTo⋁
-open Whitehead using ([_∣_]₂)
+open Whitehead using ([_∣_])
 
 -- Theorem 4.9 is omitted as it is used implicitly in the proof of the main result
 
diff --git a/Cubical/Papers/Pi4S3.agda b/Cubical/Papers/Pi4S3.agda
index 6bcc7e8642..fa312717f5 100644
--- a/Cubical/Papers/Pi4S3.agda
+++ b/Cubical/Papers/Pi4S3.agda
@@ -35,6 +35,7 @@ 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.Sn.Multiplication                  as SMult
 open import Cubical.HITs.Pushout                            as Pushouts
 open import Cubical.HITs.Wedge                           as Wedges
 open import Cubical.HITs.Join                               as Joins
@@ -212,11 +213,11 @@ open James₁ using (IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅)
 
 ---- C. Formalization of the James construction ----
 -- Proposition 8: Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹
-open Spheres using (IsoSphereJoin)
+open SMult using (IsoSphereJoin)
 
 -- Definition 6: W + whitehead product
 W = joinTo⋁
-open Whitehead using ([_∣_]₂)
+open Whitehead using ([_∣_])
 
 -- Theorem 3 is omitted as it is used implicitly in the proof of the main result