diff --git a/Cubical/HITs/Join/Base.agda b/Cubical/HITs/Join/Base.agda
index d94f9551a6..330bf198db 100644
--- a/Cubical/HITs/Join/Base.agda
+++ b/Cubical/HITs/Join/Base.agda
@@ -4,6 +4,7 @@ module Cubical.HITs.Join.Base where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed.Base
 
 open import Cubical.HITs.S1
 open import Cubical.HITs.S3
@@ -15,6 +16,11 @@ data join {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ-max ℓ ℓ') wh
   inr : B → join A B
   push : ∀ a b → inl a ≡ inr b
 
+join∙ : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
+  → Pointed _
+fst (join∙ A B) = join (fst A) (fst B)
+snd (join∙ A B) = inl (pt A)
+
 facek01 : I → I → I → join S¹ S¹
 facek01 i j k = hfill (λ l → λ { (j = i0) → push base base (~ l ∧ ~ k)
                                ; (j = i1) → push base base (~ l ∧ ~ k)
diff --git a/Cubical/HITs/SmashProduct/Base.agda b/Cubical/HITs/SmashProduct/Base.agda
index 6ce442c4f7..2c591a2797 100644
--- a/Cubical/HITs/SmashProduct/Base.agda
+++ b/Cubical/HITs/SmashProduct/Base.agda
@@ -9,6 +9,7 @@ open import Cubical.Foundations.Pointed.Homogeneous
 open import Cubical.Foundations.Path
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Transport
+open import Cubical.Foundations.Equiv
 
 open import Cubical.Data.Unit
 open import Cubical.Data.Sigma
@@ -17,6 +18,10 @@ open import Cubical.Data.Fin
 
 open import Cubical.HITs.Pushout.Base
 open import Cubical.HITs.Wedge
+open import Cubical.HITs.Susp renaming (toSusp to σ)
+open import Cubical.HITs.Join
+
+open import Cubical.Homotopy.Loopspace
 
 data Smash {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') : Type (ℓ-max ℓ ℓ') where
   basel : Smash A B
@@ -279,6 +284,34 @@ _⋀∙→refl_ : ∀ {ℓ ℓ'} {C : Type ℓ} {D : Type ℓ'}
 fst (f ⋀∙→refl g) = f ⋀→refl g
 snd (f ⋀∙→refl g) = refl
 
+
+⋀≃ : ∀ {ℓ ℓ'} {A B : Pointed ℓ} {C D : Pointed ℓ'}
+  → (f : A ≃∙ B) (g : C ≃∙ D)
+  → (A ⋀ C) ≃ (B ⋀ D)
+⋀≃ {ℓ = ℓ} {ℓ'} {B = B} {D = D} f g = _ , ⋀≃-isEq f g
+  where
+  help : (x : _) → (idfun∙ B ⋀→ idfun∙ D) x ≡ x
+  help (inl x) = refl
+  help (inr x) = refl
+  help (push (inl x) i) j = rUnit (push (inl x)) (~ j) i
+  help (push (inr x) i) j = rUnit (push (inr x)) (~ j) i
+  help (push (push a i) j) k =
+    hcomp (λ r → λ {(i = i0) → rUnit (push (inl (snd B))) (~ k ∧ r) j
+                   ; (i = i1) → rUnit (push (inr (snd D))) (~ k ∧ r) j
+                   ; (j = i0) → inl tt
+                   ; (j = i1) → inr (snd B , snd D)
+                   ; (k = i1) → push (push tt i) j})
+           (push (push tt i) j)
+
+  ⋀≃-isEq : {A : Pointed ℓ} {C : Pointed ℓ'}
+    (f : A ≃∙ B) (g : C ≃∙ D) → isEquiv (≃∙map f ⋀→ ≃∙map g)
+  ⋀≃-isEq {C = C} =
+    Equiv∙J (λ A f → (g : C ≃∙ D)
+                   → isEquiv (≃∙map f ⋀→ ≃∙map g))
+     (Equiv∙J (λ _ g → isEquiv (idfun∙ _ ⋀→ ≃∙map g))
+       (subst isEquiv (sym (funExt help)) (idIsEquiv _)))
+
+
 ⋀→Smash : A ⋀ B → Smash A B
 ⋀→Smash (inl x) = basel
 ⋀→Smash (inr (x , x₁)) = proj x x₁
@@ -918,3 +951,343 @@ module ⋀-fun≡' {C : Type ℓ} (f g : A ⋀ B → C)
 
     main : (x : _) → f x ≡ g x
     main = ⋀-fun≡ {A = A} {B = B} f g p pr lp lem
+
+-- Suspension of a smash product is a join
+module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} where
+ private
+   sm-fillᵣ : ∀ {ℓ} {A : Type ℓ} {x* : A} (y* : A) (p* : x* ≡ y*)
+     (y : A) → (p : x* ≡ y)
+       → sym p* ≡ (sym p* ∙∙ p ∙∙ sym p)
+   sm-fillᵣ y* p* y p j i =
+     hcomp (λ r → λ {(i = i0) → p* r
+                    ; (i = i1) → p (~ r ∧ j)
+                    ; (j = i0) → p* (~ i ∧ r)
+                    ; (j = i1) → doubleCompPath-filler
+                                   (sym p*) p (sym p) r i})
+       (p (i ∧ j))
+
+   sm-fillₗ : ∀ {ℓ} {A : Type ℓ} {x* : A} (y* : A) (p* : x* ≡ y*)
+        (y : A) (p : x* ≡ y)
+     → p* ≡ (p ∙∙ sym p ∙∙ p*)
+   sm-fillₗ y* p* y p j i =
+       hcomp (λ r → λ {(i = i0) → p (~ r ∧ j)
+                      ; (i = i1) → p* r
+                      ; (j = i0) → p* (r ∧ i)
+                      ; (j = i1) → doubleCompPath-filler
+                                     p (sym p) p* r i})
+         (p (~ i ∧ j))
+
+   sm-fillₗᵣ≡ : ∀ {ℓ} {A : Type ℓ} {x* : A} (y* : A) (p* : x* ≡ y*)
+     → sm-fillₗ _ (sym p*) _ (sym p*) ≡ sm-fillᵣ _ p* _ p*
+   sm-fillₗᵣ≡ = J> refl
+
+ SuspSmash→Join : Susp (A ⋀ B) → (join (typ A) (typ B))
+ SuspSmash→Join north = inr (pt B)
+ SuspSmash→Join south = inl (pt A)
+ SuspSmash→Join (merid (inl x) i) =
+   push (pt A) (pt B) (~ i)
+ SuspSmash→Join (merid (inr (x , b)) i) =
+   (sym (push x (pt B)) ∙∙ push x b ∙∙ sym (push (pt A) b)) i
+ SuspSmash→Join (merid (push (inl x) j) i) =
+   sm-fillₗ {A = join (typ A) (typ B)} _
+     (sym (push (pt A) (pt B))) _ (sym (push x (pt B))) j i
+ SuspSmash→Join (merid (push (inr x) j) i) =
+   sm-fillᵣ {A = join (typ A) (typ B)} _
+     (push (pt A) (pt B)) _  (push (pt A) x) j i
+ SuspSmash→Join (merid (push (push a k) j) i) =
+   sm-fillₗᵣ≡ _ (push (pt A) (pt B)) k j i
+
+ Join→SuspSmash : join (typ A) (typ B) → Susp (A ⋀ B)
+ Join→SuspSmash (inl x) = north
+ Join→SuspSmash (inr x) = south
+ Join→SuspSmash (push a b i) = merid (inr (a , b)) i
+
+ Join→SuspSmash→Join : (x : join (typ A) (typ B))
+   → SuspSmash→Join (Join→SuspSmash x) ≡ x
+ Join→SuspSmash→Join (inl x) = sym (push x (pt B))
+ Join→SuspSmash→Join (inr x) = push (pt A) x
+ Join→SuspSmash→Join (push a b i) j =
+   doubleCompPath-filler
+     (sym (push a (pt B))) (push a b) (sym (push (pt A) b)) (~ j) i
+
+ SuspSmash→Join→SuspSmash : (x : Susp (A ⋀ B))
+   → Join→SuspSmash (SuspSmash→Join x) ≡ x
+ SuspSmash→Join→SuspSmash north = sym (merid (inr (pt A , pt B)))
+ SuspSmash→Join→SuspSmash south = merid (inr (pt A , pt B))
+ SuspSmash→Join→SuspSmash (merid a i) j =
+   hcomp (λ r
+     → λ {(i = i0) → merid (inr (pt A , pt B)) (~ j ∨ ~ r)
+         ; (i = i1) → merid (inr (pt A , pt B)) (j ∧ r)
+         ; (j = i0) → Join→SuspSmash (SuspSmash→Join (merid a i))
+         ; (j = i1) → doubleCompPath-filler
+                        (sym (merid (inr (pt A , pt B))))
+                        (merid a)
+                        (sym (merid (inr (pt A , pt B)))) (~ r) i})
+       (f₁₂ j .fst a i)
+   where
+   f₁ f₂ : A ⋀∙ B →∙ (Path (Susp (A ⋀ B)) south north
+                     , sym (merid (inr (snd A , snd B))))
+   (fst f₁) a i = Join→SuspSmash (SuspSmash→Join (merid a i))
+   snd f₁ = refl
+   (fst f₂) a =
+        sym (merid (inr (pt A , pt B)))
+     ∙∙ merid a
+     ∙∙ sym (merid (inr (pt A , pt B)))
+   snd f₂ = cong₂ (λ x y → sym x ∙∙ y ∙∙ sym x)
+             refl (cong merid (push (inl (pt A))))
+          ∙ doubleCompPath≡compPath
+             (sym (merid (inr (pt A , pt B)))) _ _
+          ∙ cong₂ _∙_ refl (rCancel (merid (inr (pt A , pt B))))
+          ∙ sym (rUnit _)
+
+   f₁₂ : f₁ ≡ f₂
+   f₁₂ = ⋀→∙Homogeneous≡ (isHomogeneousPath _ _)
+     λ x y → cong-∙∙ Join→SuspSmash
+                    (sym (push x (pt B)))
+                    (push x y)
+                    (sym (push (pt A) y))
+           ∙ (λ i → sym (merid ((sym (push (inl x))
+                               ∙ push (inl (pt A))) i))
+                  ∙∙ merid (inr (x , y))
+                  ∙∙ sym (merid ((sym (push (inr y))
+                               ∙ push (inl (pt A))) i)))
+
+ SmashJoinIso : Iso (Susp (A ⋀ B)) (join (typ A) (typ B))
+ Iso.fun SmashJoinIso = SuspSmash→Join
+ Iso.inv SmashJoinIso = Join→SuspSmash
+ Iso.rightInv SmashJoinIso = Join→SuspSmash→Join
+ Iso.leftInv SmashJoinIso = SuspSmash→Join→SuspSmash
+
+-- Suspension commutes with smash products
+module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} where
+
+  -- some fillers
+  merid-fill : typ A → I → I → I → Susp (A ⋀ B)
+  merid-fill a i j k =
+    hfill (λ k → λ {(i = i0) → north
+                   ; (i = i1) → merid (push (inl a) k) j
+                   ; (j = i0) → north
+                   ; (j = i1) → merid (inl tt) i})
+          (inS (merid (inl tt) (i ∧ j))) k
+
+  inl-fill₁ : typ A → I → I → I → (Susp∙ (typ A)) ⋀ B
+  inl-fill₁ a i j k =
+    hfill (λ k → λ {(i = i0) → inl tt
+                   ; (i = i1) → inr (σ A a j , snd B)
+                   ; (j = i0) → push (push tt k) i
+                   ; (j = i1) → push (push tt k) i})
+           (inS (push (inl (σ A a j)) i)) k
+
+  inl-fill : typ A → I → I → I → (Susp∙ (typ A)) ⋀ B
+  inl-fill a i j k =
+    hfill (λ k → λ {(i = i0) → inl tt
+                   ; (i = i1) → doubleCompPath-filler
+                                   (push (inr (snd B)))
+                                   (λ i₂ → inr (σ A a i₂ , snd B))
+                                   (sym (push (inr (snd B)))) k j
+                   ; (j = i0) → push (inr (snd B)) (~ k ∧ i)
+                   ; (j = i1) → push (inr (snd B)) (~ k ∧ i)})
+          (inS (inl-fill₁ a i j i1)) k
+
+  inr-fill₁ : typ B → I → I → I → (Susp∙ (typ A)) ⋀ B
+  inr-fill₁ b i j k =
+    hfill (λ k → λ {(i = i0) → inl tt
+                   ; (i = i1) → inr (rCancel (merid (pt A)) (~ k) j , b)
+                   ; (j = i0) → push (inr b) i
+                   ; (j = i1) → push (inr b) i})
+          (inS (push (inr b) i)) k
+
+  inr-fill : typ B → I → I → I → (Susp∙ (typ A)) ⋀ B
+  inr-fill b i j k =
+    hfill (λ k → λ {(i = i0) → inl tt
+                   ; (i = i1) → doubleCompPath-filler
+                                   (push (inr b))
+                                   (λ i₂ → inr (σ A (pt A) i₂ , b))
+                                   (sym (push (inr b))) k j
+                   ; (j = i0) → push (inr b) (~ k ∧ i)
+                   ; (j = i1) → push (inr b) (~ k ∧ i)})
+          (inS (inr-fill₁ b i j i1)) k
+
+  SuspL→Susp⋀ : (Susp∙ (typ A)) ⋀ B → Susp (A ⋀ B)
+  SuspL→Susp⋀ (inl x) = north
+  SuspL→Susp⋀ (inr (north , y)) = north
+  SuspL→Susp⋀ (inr (south , y)) = south
+  SuspL→Susp⋀ (inr (merid a i , y)) = merid (inr (a , y)) i
+  SuspL→Susp⋀ (push (inl north) i) = north
+  SuspL→Susp⋀ (push (inl south) i) = merid (inl tt) i
+  SuspL→Susp⋀ (push (inl (merid a j)) i) = merid-fill a i j i1
+  SuspL→Susp⋀ (push (inr x) i) = north
+  SuspL→Susp⋀ (push (push a i₁) i) = north
+
+  Susp⋀→SuspL : Susp (A ⋀ B) → (Susp∙ (typ A)) ⋀ B
+  Susp⋀→SuspL north = inl tt
+  Susp⋀→SuspL south = inl tt
+  Susp⋀→SuspL (merid (inl x) i) = inl tt
+  Susp⋀→SuspL (merid (inr (x , y)) i) =
+    (push (inr y) ∙∙ (λ i → inr (σ A x i , y)) ∙∙ sym (push (inr y))) i
+  Susp⋀→SuspL (merid (push (inl x) i₁) i) = inl-fill x i₁ i i1
+  Susp⋀→SuspL (merid (push (inr x) i₁) i) = inr-fill x i₁ i i1
+  Susp⋀→SuspL (merid (push (push a k) j) i) =
+    hcomp (λ r → λ {(i = i0) → inl-fill (snd A) j i r
+                   ; (i = i1) → inr-fill (snd B) j i r
+                   ; (j = i0) → inl tt
+                   ; (j = i1) → doubleCompPath-filler
+                                   (push (inr (pt B)))
+                                   (λ i₂ → inr (σ A (pt A) i₂ , (pt B)))
+                                   (sym (push (inr (pt B)))) r i
+                   ; (k = i0) → inl-fill (snd A) j i r
+                   ; (k = i1) → inr-fill (snd B) j i r})
+      (hcomp (λ r → λ {(i = i0) → push (push tt (r ∨ k)) j
+                      ; (i = i1) → push (push tt (r ∨ k)) j
+                      ; (j = i0) → inl tt
+                      ; (j = i1) → inr (rCancel (merid (pt A))
+                                                 (~ r ∧ k) i , pt B)
+                      ; (k = i0) → inl-fill₁ (snd A) j i r
+                      ; (k = i1) → inr-fill₁ (snd B) j i r})
+         (hcomp (λ r → λ {(i = i0) → push (push tt k) j
+                         ; (i = i1) → push (push tt k) j
+                         ; (j = i0) → inl tt
+                         ; (j = i1) → inr (rCancel (merid (pt A))
+                                                    (~ r ∨ k) i , pt B)
+                         ; (k = i0) → push (inl (rCancel (merid (pt A))
+                                                          (~ r) i)) j
+                         ; (k = i1) → push (inr (snd B)) j})
+                   (push (push tt k) j)))
+
+  SuspSmashCommIso : Iso (Susp∙ (typ A) ⋀ B) (Susp (A ⋀ B))
+  Iso.fun SuspSmashCommIso = SuspL→Susp⋀
+  Iso.inv SuspSmashCommIso = Susp⋀→SuspL
+  Iso.rightInv SuspSmashCommIso north = refl
+  Iso.rightInv SuspSmashCommIso south = merid (inl tt)
+  Iso.rightInv SuspSmashCommIso (merid a i) j =
+    hcomp (λ r → λ {(i = i0) → north
+                   ; (i = i1) → merid (inl tt) (j ∧ r)
+                   ; (j = i0) → f₁≡f₂ (~ r) .fst a i
+                   ; (j = i1) → compPath-filler
+                                  (merid a) (sym (merid (inl tt))) (~ r) i })
+           (f₂ .fst a i)
+    where
+    f₁ f₂ : (A ⋀∙ B) →∙ Ω (Susp∙ (A ⋀ B))
+    fst f₁ x = cong SuspL→Susp⋀ (cong Susp⋀→SuspL (merid x))
+    snd f₁ = refl
+    fst f₂ = σ (A ⋀∙ B)
+    snd f₂ = rCancel (merid (inl tt))
+
+    inr' : (Susp (typ A)) × (typ B) → (Susp∙ (typ A)) ⋀ B
+    inr' = inr
+
+    f₁≡f₂ : f₁ ≡ f₂
+    f₁≡f₂ =
+      ⋀→∙Homogeneous≡ (isHomogeneousPath _ _)
+          λ x y
+       →  cong (cong SuspL→Susp⋀) (cong (push (inr y) ∙∙_∙∙ sym (push (inr y)))
+            (cong-∙ (λ x → inr' (x , y)) (merid x) (sym (merid (pt A)))))
+       ∙∙ cong-∙∙ SuspL→Susp⋀ (push (inr y))
+            (cong (λ x → inr' (x , y)) (merid x)
+           ∙ cong (λ x → inr' (x , y)) (sym (merid (pt A)))) (sym (push (inr y)))
+          ∙∙ (sym (rUnit _)
+           ∙ cong-∙ SuspL→Susp⋀
+              (λ i → inr' (merid x i , y)) (λ i → inr' (merid (pt A) (~ i) , y))
+           ∙ cong (merid (inr (x , y)) ∙_)
+              λ j i → merid (push (inr y) (~ j)) (~ i) )
+  Iso.leftInv SuspSmashCommIso =
+    ⋀-fun≡ _ _ refl
+      (λ x → main (snd x) (fst x))
+      (λ { north i j → sₙ i j i1
+         ; south i j → sₛ i j i1
+         ; (merid a k) i j → cube a j k i})
+      λ x i j → push (inr x) (i ∧ j)
+    where
+    inr' : Susp (typ A) × (typ B) → (Susp∙ (typ A)) ⋀ B
+    inr' = inr
+    sₙ : I → I → I → (Susp∙ (typ A)) ⋀ B
+    sₙ i j k =
+      hfill (λ k → λ {(i = i0) → inl tt
+                     ; (i = i1) → push (inr (pt B)) (j ∨ ~ k)
+                     ; (j = i0) → push (inr (pt B)) (i ∧ ~ k)
+                     ; (j = i1) → push (inl north) i})
+            (inS (push (push tt (~ j)) i))
+            k
+
+    sₛ : I → I → I → (Susp∙ (typ A)) ⋀ B
+    sₛ i j k =
+      hfill (λ k → λ {(i = i0) → inl tt
+                     ; (i = i1) → compPath-filler
+                                    (push (inr (pt B)))
+                                    (λ i → inr (merid (pt A) i , pt B)) k j
+                     ; (j = i0) → inl tt
+                     ; (j = i1) → push (inl (merid (pt A) k)) i})
+            (inS (sₙ i j i1))
+            k
+
+    filler : fst A → fst B → I → I → I → (Susp∙ (typ A)) ⋀ B
+    filler a y i j k =
+     hfill (λ k → λ {(i = i0) → push (inr y) j
+                    ; (i = i1) → compPath-filler
+                                   (push (inr y))
+                                   (λ i₁ → inr (merid (pt A) i₁ , y)) k j
+                    ; (j = i0) → Susp⋀→SuspL (SuspL→Susp⋀ (inr (merid a i , y)))
+                    ; (j = i1) → inr (compPath-filler
+                                        (merid a)
+                                        (sym (merid (pt A))) (~ k) i , y)})
+           (inS (doubleCompPath-filler
+                  (push (inr y))
+                  (λ i₁ → inr' (σ A a i₁ , y))
+                  (sym (push (inr y))) (~ j) i)) k
+
+    cube₁ : (a : typ A)
+      → Cube (λ k i → Iso.inv SuspSmashCommIso (merid-fill a k i i1))
+              (λ k i → inl-fill a k i i1)
+              (λ _ _ → inl tt)
+              refl
+              (λ _ _ → inl tt)
+              λ _ _ → inl tt
+    cube₁ a j k i =
+      hcomp (λ r → λ {(i = i0) → inl tt
+                     ; (i = i1) → inl tt
+                     ; (j = i0) → Iso.inv SuspSmashCommIso (merid-fill a k i r)
+                     ; (j = i1) → inl-fill a k i i1
+                     ; (k = i0) → inl tt
+                     ; (k = i1) → inl-fill a (j ∨ r) i i1})
+             (inl-fill a (j ∧ k) i i1)
+
+    cube : (a : typ A)
+      → Cube (λ k i → Iso.inv SuspSmashCommIso
+                         (Iso.fun SuspSmashCommIso (push (inl (merid a k)) i)))
+              (λ k i → push (inl (merid a k)) i)
+              (λ j i → sₙ i j i1) (λ j i → sₛ i j i1)
+              (λ j k → inl tt) (λ j k → filler a (pt B) k j i1)
+    cube a = (λ j k i → cube₁ a j i k) ◁
+     (λ j k i →
+      hcomp (λ r
+        → λ {(i = i0) → inl tt
+            ; (i = i1) → filler a (pt B) k j r
+            ; (j = i0) → inl-fill a i k i1
+            ; (j = i1) → push (inl (compPath-filler
+                           (merid a) (sym (merid (pt A))) (~ r) k)) i
+            ; (k = i0) → sₙ i j i1
+            ; (k = i1) → sₛ i j r})
+       (hcomp (λ r
+         → λ {(i = i0) → inl tt
+             ; (i = i1) → doubleCompPath-filler
+                             (push (inr (pt B)))
+                             (λ i₁ → inr' (σ A a i₁ , (pt B)))
+                             (sym (push (inr (pt B)))) (~ j ∧ r) k
+             ; (j = i0) → inl-fill a i k r
+             ; (j = i1) → push (inl (σ A a k)) i
+             ; (k = i0) → sₙ i j r
+             ; (k = i1) → sₙ i j r})
+         (hcomp (λ r
+           → λ {(i = i0) → inl tt
+               ; (i = i1) → inl-fill₁ a i k r
+               ; (j = i0) → inl-fill₁ a i k r
+               ; (j = i1) → push (inl (σ A a k)) i
+               ; (k = i0) → push (push tt (r ∧ (~ j))) i
+               ; (k = i1) → push (push tt (r ∧ (~ j))) i})
+       (push (inl (σ A a k)) i))))
+
+    main : (y : typ B) (x : Susp (typ A))
+      → Susp⋀→SuspL (SuspL→Susp⋀ (inr (x , y))) ≡ inr (x , y)
+    main y north = push (inr y)
+    main y south = push (inr y) ∙ λ i → inr (merid (pt A) i , y)
+    main y (merid a i) j = filler a y i j i1
diff --git a/Cubical/HITs/Sn/Multiplication.agda b/Cubical/HITs/Sn/Multiplication.agda
new file mode 100644
index 0000000000..00ca912c0c
--- /dev/null
+++ b/Cubical/HITs/Sn/Multiplication.agda
@@ -0,0 +1,898 @@
+{-# OPTIONS --safe #-}
+
+{-
+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
+-}
+
+module Cubical.HITs.Sn.Multiplication where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Pointed.Homogeneous
+
+open import Cubical.Data.Sum
+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.Susp renaming (toSusp to σ)
+open import Cubical.HITs.Join
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.SmashProduct
+
+open import Cubical.Homotopy.Loopspace
+
+open Iso
+
+open PlusBis
+
+
+---- Sphere multiplication
+-- auxiliary function
+sphereFun↑ : {n m k : ℕ}
+  → (f : S₊ n → S₊ m → S₊ k)
+  → S₊ (suc n) → S₊ m → S₊ (suc k)
+sphereFun↑ {n = zero} {m = m} f base y = ptSn _
+sphereFun↑ {n = zero} {m = m} f (loop i) y = σS (f false y) i
+sphereFun↑ {n = suc n} {m = m} f north y = ptSn _
+sphereFun↑ {n = suc n} {m = m} f south y = ptSn _
+sphereFun↑ {n = suc n} {m = m} f (merid a i) y = σS (f a y) i
+
+-- sphere multiplication
+_⌣S_ : {n m : ℕ} → S₊ n → S₊ m → S₊ (n + m)
+_⌣S_ {n = zero} {m = m} false y = y
+_⌣S_ {n = zero} {m = m} true y = ptSn m
+_⌣S_ {n = suc n} {m = m} = sphereFun↑ (_⌣S_ {n = n})
+
+-- Left- and right-unit laws
+IdR⌣S : {n m : ℕ} (y : S₊ m)
+  → Path (S₊ (n + m)) (ptSn n ⌣S y) (ptSn (n + m))
+IdR⌣S {n = zero} {m = m} y = refl
+IdR⌣S {n = suc zero} {m = m} y = refl
+IdR⌣S {n = suc (suc n)} {m = m} y = refl
+
+IdL⌣S : {n m : ℕ} (x : S₊ n)
+  → Path (S₊ (n + m)) (x ⌣S (ptSn m)) (ptSn (n + m))
+IdL⌣S {n = zero} false = refl
+IdL⌣S {n = zero} true = refl
+IdL⌣S {n = suc zero} base = refl
+IdL⌣S {n = suc zero} {zero} (loop i) j = base
+IdL⌣S {n = suc zero} {suc m} (loop i) j = rCancel (merid (ptSn (suc m))) j i
+IdL⌣S {n = suc (suc n)} {m} north j = north
+IdL⌣S {n = suc (suc n)} {m} south j = north
+IdL⌣S {n = suc (suc n)} {m} (merid a i) j =
+  (cong σS (IdL⌣S a)
+  ∙ rCancel (merid (ptSn _))) j i
+
+IdL⌣S≡IdR⌣S : (n m : ℕ)
+  → IdL⌣S {n = n} {m = m} (ptSn n) ≡ IdR⌣S (ptSn m)
+IdL⌣S≡IdR⌣S zero m = refl
+IdL⌣S≡IdR⌣S (suc zero) m = refl
+IdL⌣S≡IdR⌣S (suc (suc n)) m = refl
+
+-- Multiplication induced on smash products of spheres
+⋀S∙ : (n m : ℕ) → S₊∙ n ⋀∙ S₊∙ m →∙ S₊∙ (n + m)
+fst (⋀S∙ n m) (inl x) = ptSn _
+fst (⋀S∙ n m) (inr x) = (fst x) ⌣S (snd x)
+fst (⋀S∙ n m) (push (inl x) i) = IdL⌣S x (~ i)
+fst (⋀S∙ n m) (push (inr x) i) = IdR⌣S x (~ i)
+fst (⋀S∙ n m) (push (push a i₁) i) = IdL⌣S≡IdR⌣S n m i₁ (~ i)
+snd (⋀S∙ n m) = refl
+
+⋀S : (n m : ℕ) → S₊∙ n ⋀ S₊∙ m → S₊ (n + m)
+⋀S n m = fst (⋀S∙ n m)
+
+-- Proof that it is an equivalence
+⋀S-base : (m : ℕ)
+  → Iso (S₊∙ zero ⋀ S₊∙ m) (S₊ m)
+fun (⋀S-base m) = ⋀S zero m
+inv (⋀S-base m) x = inr (false , x)
+rightInv (⋀S-base m) x = refl
+leftInv (⋀S-base m) =
+  ⋀-fun≡ _ _
+    (sym (push (inl false)))
+    (λ { (false , y) → refl
+       ; (true , y) → sym (push (inl false)) ∙ push (inr y)})
+     (λ { false i j → push (inl false) (i ∨ ~ j)
+        ; true → compPath-filler (sym (push (inl false))) (push (inl true))
+        ▷ cong (sym (push (inl false)) ∙_)
+                (λ i → push (push tt i) )})
+        λ x → compPath-filler (sym (push (inl false))) (push (inr x))
+{-
+Proof that ⋀S respects suspension, i.e. that the following diagram commutes
+                ⋀S
+Sⁿ⁺¹ ∧ Sᵐ ---------------> Sⁿ⁺ᵐ⁺¹
+|                          |
+|                          |
+v                          v
+Σ (Sⁿ ∧ Sᵐ)  -----------> Σ Sⁿ⁺ᵐ
+                Σ(⋀S)
+-}
+
+⋀S-ind : (n m : ℕ) (x : _)
+  → ⋀S (suc n) m x
+   ≡ Iso.inv (IsoSucSphereSusp (n + m))
+      (suspFun (⋀S n m) (Iso.fun SuspSmashCommIso
+        (((Iso.fun (IsoSucSphereSusp n) , IsoSucSphereSusp∙' n)
+      ⋀→ idfun∙ (S₊∙ m)) x)))
+⋀S-ind zero m = ⋀-fun≡ _ _
+  (sym (IsoSucSphereSusp∙ m))
+    (λ x → main m (fst x) (snd x))
+    (mainₗ m)
+    mainᵣ
+  where
+  F' :  (m : ℕ) → Susp ((Bool , true) ⋀ S₊∙ m) → _
+  F' m = inv (IsoSucSphereSusp (zero + m)) ∘ suspFun (⋀S zero m)
+
+  F : (m : ℕ) → Susp∙ Bool ⋀ S₊∙ m → _
+  F m = F' m ∘ fun SuspSmashCommIso
+
+  G : (m : ℕ) → _ → _
+  G m = _⋀→_ {A = S₊∙ 1} {B = S₊∙ m}
+         (fun (IsoSucSphereSusp zero) , (λ _ → north))
+         (idfun∙ (S₊∙ m))
+
+  main : (m : ℕ) (x : S¹) (y : S₊ m)
+    → x ⌣S y
+    ≡ F m (inr (S¹→SuspBool x , y))
+  main m base y = sym (IsoSucSphereSusp∙ m)
+  main zero (loop i) false j =
+    ((cong-∙ (λ x → F zero (inr (x , false)))
+             (merid false) (sym (merid true)))
+    ∙ sym (rUnit loop)) (~ j) i
+  main zero (loop i) true j =
+    F zero (inr (rCancel (merid true) (~ j) i , false))
+  main (suc m) (loop i) y j =
+    cong-∙ (λ x → F (suc m) (inr (x , y)))
+           (merid false) (sym (merid true)) (~ j) i
+
+  mainₗ : (m : ℕ) (x : S¹)
+    → PathP (λ i → IdL⌣S {m = m} x (~ i)
+            ≡ F m (G m (push (inl x) i)))
+             (sym (IsoSucSphereSusp∙ m))
+             (main m x (ptSn m))
+  mainₗ zero =
+    toPropElim (λ _ → isOfHLevelPathP' 1 (isGroupoidS¹ _ _) _ _)
+     (flipSquare (cong (cong (F zero)) (rUnit (push (inl north)))))
+  mainₗ (suc m) x = flipSquare (help x
+    ▷ (cong (cong (F (suc m))) (rUnit (push (inl (S¹→SuspBool x))))))
+    where
+    help : (x : S¹)
+      → PathP (λ i → north ≡ main (suc m) x (ptSn (suc m)) i)
+           (sym (IdL⌣S {n = 1} x))
+           (cong (F (suc m)) (push (inl (S¹→SuspBool x))))
+    help base = refl
+    help (loop i) j k =
+      hcomp (λ r
+        → λ {(i = i0) → north
+            ; (i = i1) → F' (suc m)
+                           (merid-fill
+                            {A = Bool , true}
+                            {B = S₊∙ (suc m)} true (~ r) k j)
+            ; (j = i0) → rCancel-filler (merid (ptSn (suc m))) r (~ k) i
+            ; (j = i1) → F (suc m)
+                           (push (inl (compPath-filler
+                             (merid false) (sym (merid true)) r i)) k)
+            ; (k = i0) → north
+            ; (k = i1) → cong-∙∙-filler
+                            (λ x₁ → F (suc m) (inr (x₁ , ptSn (suc m))))
+                            refl (merid false) (sym (merid true)) r (~ j) i})
+       (F' (suc m) (merid-fill {A = Bool , true} {B = S₊∙ (suc m)} false k i j))
+  mainᵣ : (x : S₊ m)
+    → PathP (λ i → ptSn (suc m) ≡ F m (G m (push (inr x) i)))
+             (sym (IsoSucSphereSusp∙ m))
+             (sym (IsoSucSphereSusp∙ m))
+  mainᵣ x = flipSquare ((λ i j → (IsoSucSphereSusp∙ m) (~ i))
+                       ▷ cong (cong (F m)) (rUnit (push (inr x))))
+⋀S-ind (suc n) m = ⋀-fun≡ _ _ refl
+  (λ x → h (fst x) (snd x))
+  hₗ
+  λ x → flipSquare (cong (cong (suspFun (⋀S (suc n) m)
+                              ∘ fun SuspSmashCommIso))
+                    (rUnit (push (inr x))))
+  where
+  h : (x : S₊ (suc (suc n))) (y : S₊ m)
+    → (x ⌣S y)
+    ≡ suspFun (⋀S (suc n) m)
+       (SuspL→Susp⋀ (inr (idfun (Susp (S₊ (suc n))) x , y)))
+  h north y = refl
+  h south y = merid (ptSn _)
+  h (merid a i) y j = compPath-filler
+           (merid (a ⌣S y)) (sym (merid (ptSn (suc (n + m))))) (~ j) i
+
+  hₗ-lem : (x : Susp (S₊ (suc n)))
+    → PathP (λ i → north ≡ h x (ptSn m) i)
+             (sym (IdL⌣S x))
+             (cong (suspFun (⋀S (suc n) m)
+                  ∘ fun SuspSmashCommIso)
+                   (push (inl x)))
+  hₗ-lem north = refl
+  hₗ-lem south i j = merid (ptSn (suc (n + m))) (i ∧ j)
+  hₗ-lem (merid a i) j k = help j k i
+    where
+    help : Cube (sym (cong σS
+                  (IdL⌣S {n = suc n} {m = m} a)
+                 ∙ rCancel (merid (ptSn (suc n + m)))))
+                (λ k i → suspFun (⋀S (suc n) m)
+                           (SuspL→Susp⋀ (push (inl (merid a i)) k)))
+                (λ j i → north)
+                (λ j i → compPath-filler
+                           (merid (a ⌣S ptSn m))
+                           (sym (merid (ptSn (suc (n + m))))) (~ j) i)
+                (λ j k → north)
+                λ j k → merid (ptSn (suc (n + m))) (j ∧ k)
+    help j k i =
+      hcomp (λ r
+        → λ {(i = i0) → north
+            ; (i = i1) → merid (ptSn (suc (n + m))) (j ∧ k)
+            ; (j = i0) → compPath-filler'
+                           (cong σS
+                            (IdL⌣S {n = suc n} {m = m} a))
+                           (rCancel (merid (ptSn (suc n + m)))) r (~ k) i
+            ; (j = i1) → suspFun (⋀S (suc n) m)
+                           (merid-fill a k i r)
+            ; (k = i0) → north
+            ; (k = i1) → compPath-filler
+                           (merid (IdL⌣S a (~ r)))
+                           (sym (merid (ptSn (suc (n + m))))) (~ j) i})
+         (hcomp (λ r → λ {(i = i0) → north
+                        ; (i = i1) → merid (ptSn (suc (n + m))) ((j ∨ ~ r) ∧ k)
+                        ; (j = i0) → rCancel-filler (merid (ptSn _)) r (~ k) i
+                        ; (j = i1) → merid (ptSn (suc (n + m))) (i ∧ k)
+                        ; (k = i0) → north
+                        ; (k = i1) → compPath-filler
+                                       (merid (ptSn _))
+                                       (sym (merid (ptSn (suc (n + m)))))
+                                       (~ j ∧ r) i})
+                  (merid (ptSn (suc (n + m))) (i ∧ k)))
+
+  hₗ : (x : Susp (S₊ (suc n)))
+    → PathP (λ i → IdL⌣S x (~ i)
+      ≡ inv (IsoSucSphereSusp (suc n + m))
+         (suspFun (⋀S (suc n) m)
+          (fun SuspSmashCommIso
+           (((fun (IsoSucSphereSusp (suc n)) , IsoSucSphereSusp∙' (suc n)) ⋀→
+             idfun∙ (S₊∙ m))
+            (push (inl x) i))))) refl (h x (ptSn m))
+  hₗ x =
+    flipSquare
+       ((hₗ-lem x
+      ▷ sym (cong (cong (inv (IsoSucSphereSusp (suc n + m))
+                  ∘ suspFun (⋀S (suc n) m)
+                  ∘ fun SuspSmashCommIso))
+                  (sym (rUnit (push (inl x)))))))
+
+
+isEquiv-⋀S : (n m : ℕ) → isEquiv (⋀S n m)
+isEquiv-⋀S zero m = isoToIsEquiv (⋀S-base m)
+isEquiv-⋀S (suc n) m =
+  subst isEquiv (sym (funExt (⋀S-ind n m)))
+    (snd (helpEq (isEquiv-⋀S n m)))
+  where
+  r = isoToEquiv (IsoSucSphereSusp n)
+
+  helpEq : isEquiv (⋀S n m) → (S₊∙ (suc n) ⋀ S₊∙ m) ≃ S₊ (suc n + m)
+  helpEq iseq =
+    compEquiv
+     (compEquiv
+       (compEquiv
+         (⋀≃ (r , IsoSucSphereSusp∙' n) (idEquiv (S₊ m) , refl))
+         (isoToEquiv SuspSmashCommIso))
+       (isoToEquiv
+         (congSuspIso (equivToIso (⋀S n m , iseq)))))
+      (isoToEquiv (invIso (IsoSucSphereSusp (n + m))))
+
+SphereSmashIso : (n m : ℕ) → Iso (S₊∙ n ⋀ S₊∙ m) (S₊ (n + m))
+SphereSmashIso n m = equivToIso (⋀S n m , isEquiv-⋀S n m)
+
+-- Proof that the pinch map Sⁿ * Sᵐ → Sⁿ⁺ᵐ⁺¹ is an equivalence
+join→Sphere : (n m : ℕ)
+  → join (S₊ n) (S₊ m) → S₊ (suc (n + m))
+join→Sphere n m (inl x) = ptSn _
+join→Sphere n m (inr x) = ptSn _
+join→Sphere n m (push a b i) = σS (a ⌣S b) i
+
+join→Sphere∙ : (n m : ℕ)
+  → join∙ (S₊∙ n) (S₊∙ m) →∙ S₊∙ (suc (n + m))
+fst (join→Sphere∙ n m) = join→Sphere n m
+snd (join→Sphere∙ n m) = refl
+
+joinSphereIso' : (n m : ℕ)
+  → Iso (join (S₊ n) (S₊ m)) (S₊ (suc (n + m)))
+joinSphereIso' n m =
+  compIso (invIso (SmashJoinIso {A = S₊∙ n} {B = S₊∙ m}))
+   (compIso (congSuspIso (SphereSmashIso n m))
+    (invIso (IsoSucSphereSusp (n + m))))
+
+join→Sphere≡ : (n m : ℕ) (x : _)
+  → join→Sphere n m x ≡ joinSphereIso' n m .Iso.fun x
+join→Sphere≡ zero zero (inl x) = refl
+join→Sphere≡ zero (suc m) (inl x) = refl
+join→Sphere≡ (suc n) m (inl x) = refl
+join→Sphere≡ zero zero (inr x) = refl
+join→Sphere≡ zero (suc m) (inr x) = merid (ptSn (suc m))
+join→Sphere≡ (suc n) zero (inr x) = merid (ptSn (suc n + zero))
+join→Sphere≡ (suc n) (suc m) (inr x) = merid (ptSn (suc n + suc m))
+join→Sphere≡ zero zero (push false false i) j = loop i
+join→Sphere≡ zero zero (push false true i) j = base
+join→Sphere≡ zero zero (push true b i) j = base
+join→Sphere≡ zero (suc m) (push a b i) j =
+  compPath-filler
+    (merid (a ⌣S b)) (sym (merid (ptSn (suc m)))) (~ j) i
+join→Sphere≡ (suc n) zero (push a b i) j =
+  compPath-filler
+    (merid (a ⌣S b)) (sym (merid (ptSn (suc n + zero)))) (~ j) i
+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
+
+-- 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
+rightInv (IsoSphereJoin n m) x =
+  join→Sphere≡ n m (joinSphereIso' n m .Iso.inv x)
+  ∙ joinSphereIso' n m .Iso.rightInv x
+leftInv (IsoSphereJoin n m) x =
+  cong (joinSphereIso' n m .inv) (join→Sphere≡ n m x)
+  ∙ 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
+
+
+-- Associativity ⌣S
+-- Preliminary lemma
+⌣S-false : {n : ℕ} (x : S₊ n) → PathP (λ i → S₊ (+-comm n zero i)) (x ⌣S false) x
+⌣S-false {n = zero} false = refl
+⌣S-false {n = zero} true = refl
+⌣S-false {n = suc zero} base = refl
+⌣S-false {n = suc zero} (loop i) = refl
+⌣S-false {n = suc (suc n)} north i = north
+⌣S-false {n = suc (suc n)} south i = merid (ptSn (suc (+-zero n i))) i
+⌣S-false {n = suc (suc n)} (merid a i) j =
+  hcomp (λ k → λ {(i = i0) → north
+                 ; (i = i1) → merid (ptSn (suc (+-zero n j))) (j ∨ ~ k)
+                 ; (j = i1) → merid a i})
+        (merid (⌣S-false a j) i)
+
+assoc⌣S : {n m l : ℕ} (x : S₊ n) (y : S₊ m) (z : S₊ l)
+  → PathP (λ i → S₊ (+-assoc n m l i))
+           (x ⌣S (y ⌣S z)) ((x ⌣S y) ⌣S z)
+assoc⌣S {n = zero} {m = m} false y z = refl
+assoc⌣S {n = zero} {m = m} true y z = sym (IdR⌣S z)
+assoc⌣S {n = suc zero} {m = m} base y z = sym (IdR⌣S z)
+assoc⌣S {n = suc zero} {m = m} (loop i) y z j = help m y j i
+  where
+  help : (m : ℕ) (y : S₊ m)
+    → Square (σS (y ⌣S z)) (cong (λ w → sphereFun↑ _⌣S_ w z) (σS y))
+                (sym (IdR⌣S z)) (sym (IdR⌣S z))
+  help zero false = refl
+  help zero true = σS∙
+  help (suc m) y =
+      rUnit (σS (y ⌣S z))
+    ∙ cong (σS (y ⌣S z) ∙_)
+           (cong sym ((sym σS∙)
+                ∙ congS σS (sym (IdR⌣S z))))
+    ∙ sym (cong-∙ (λ k → sphereFun↑ _⌣S_ k z)
+           (merid y)
+           (sym (merid (ptSn (suc m)))))
+assoc⌣S {n = suc (suc n)} {m = m} north y z k = north
+assoc⌣S {n = suc (suc n)} {m = m} south y z k = north
+assoc⌣S {n = suc (suc n)} {m = m} {l} (merid a i) y z j =
+  help m y (assoc⌣S a y z) j i
+  where
+  help : (m : ℕ) (y : S₊ m)
+    → PathP (λ i₁ → S₊ (suc (+-assoc n m l i₁)))
+             (a ⌣S (y ⌣S z))
+             ((a ⌣S y) ⌣S z)
+    → SquareP (λ j i → S₊ (+-assoc (suc (suc n)) m l j))
+              (σS (a ⌣S (y ⌣S z)))
+              (λ i → (merid a i ⌣S y) ⌣S z)
+              (λ _ → north) (λ _ → north)
+  help zero false _ =
+      (λ i j → σ (S₊∙ (suc (+-assoc n zero l i))) (lem i) j)
+    ▷ rUnit _
+     ∙ cong₂ _∙_ (congS σS (λ _ → (a ⌣S false) ⌣S z))
+                 (cong sym (sym σS∙
+                 ∙ congS σS
+                     (sym (IdR⌣S z))))
+     ∙ sym (cong-∙ (_⌣S z)
+           (merid (a ⌣S false))
+           (sym (merid (ptSn (suc (n + zero))))))
+    where
+    lem : PathP (λ i → S₊ (suc (+-assoc n zero l i)))
+                (a ⌣S z) ((a ⌣S false) ⌣S z)
+    lem = toPathP ((λ i → subst (S₊ ∘ suc)
+                            (isSetℕ _ _ (+-assoc n zero l)
+                                         (λ j → +-zero n (~ j) + l) i)
+                            (a ⌣S z))
+                  ∙ fromPathP (λ i → ⌣S-false a (~ i) ⌣S z))
+  help zero true _ =
+    (congS σS (IdL⌣S a) ∙ σS∙)
+    ◁ (λ i j → north)
+    ▷ (cong (cong (_⌣S z))
+           (sym σS∙
+         ∙ congS σS (sym (IdL⌣S a))))
+  help (suc m) y q =
+      (λ i j → σS (q i) j)
+    ▷ (rUnit _
+     ∙ cong₂ _∙_ refl
+             (cong sym (sym σS∙ ∙ cong σS (sym (IdR⌣S z))))
+     ∙ sym (cong-∙ (_⌣S z) (merid (a ⌣S y))
+           (sym (merid (ptSn (suc (n + suc m)))))))
+
+-- Goal: graded commutativity
+
+-- 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)
+
+-- The folowing is an explicit definition of -S^ (n · m) which is
+-- often easier to reason about
+-S^-expl : {k : ℕ} (n m : ℕ)
+  → isEvenT n ⊎ isOddT n
+  → isEvenT m ⊎ isOddT m
+  → S₊ k → S₊ k
+-S^-expl {k = zero} n m (inl x₁) q x = x
+-S^-expl {k = zero} n m (inr x₁) (inl x₂) x = x
+-S^-expl {k = zero} n m (inr x₁) (inr x₂) false = true
+-S^-expl {k = zero} n m (inr x₁) (inr x₂) true = false
+-S^-expl {k = suc zero} n m p q base = base
+-S^-expl {k = suc zero} n m (inl x) q (loop i) = loop i
+-S^-expl {k = suc zero} n m (inr x) (inl x₁) (loop i) = loop i
+-S^-expl {k = suc zero} n m (inr x) (inr x₁) (loop i) = loop (~ i)
+-S^-expl {k = suc (suc k)} n m p q north = north
+-S^-expl {k = suc (suc k)} n m p q south = north
+-S^-expl {k = suc (suc k)} n m (inl x) q (merid a i) = σS a i
+-S^-expl {k = suc (suc k)} n m (inr x) (inl x₁) (merid a i) = σS a i
+-S^-expl {k = suc (suc k)} n m (inr x) (inr x₁) (merid a i) = σS a (~ i)
+
+--  invSphere commutes with S^
+invSphere-S^ : {k : ℕ} (n : ℕ) (x : S₊ k)
+  → invSphere (-S^ n x) ≡ -S^ n (invSphere x)
+invSphere-S^ zero x = refl
+invSphere-S^ (suc n) x = cong invSphere (invSphere-S^ n x)
+
+-S^² : {k : ℕ} (n : ℕ) (x : S₊ k) → -S^ n (-S^ n x) ≡ x
+-S^² zero x = refl
+-S^² (suc n) x =
+  cong invSphere (sym (invSphere-S^ n (-S^ n x)))
+  ∙ invSphere² _ (-S^ n (-S^ n x))
+  ∙ -S^² n x
+
+-S^Iso : {k : ℕ} (n : ℕ) → Iso (S₊ k) (S₊ k)
+fun (-S^Iso n) = -S^ n
+inv (-S^Iso n) = -S^ n
+rightInv (-S^Iso n) = -S^² n
+leftInv (-S^Iso n) = -S^² n
+
+-S^-comp : {k : ℕ} (n m : ℕ) (x : S₊ k)
+  → -S^ n (-S^ m x) ≡ -S^ (n + m) x
+-S^-comp zero m x = refl
+-S^-comp (suc n) m x = cong invSphere (-S^-comp n m x)
+
+-S^·2 : {k : ℕ} (n : ℕ) (x : S₊ k) → -S^ (n + n) x ≡ x
+-S^·2 zero x = refl
+-S^·2 (suc n) x =
+    cong invSphere (λ i → -S^ (+-comm n (suc n) i) x)
+  ∙ invSphere² _ (-S^ (n + n) x)
+  ∙ -S^·2 n x
+
+-- technical transport lemma
+private
+  -S^-transp : {k : ℕ} (m : ℕ) (p : k ≡ m) (n : ℕ) (x : S₊ k)
+    → subst S₊ p (-S^ n x) ≡ -S^ n (subst S₊ p x)
+  -S^-transp =
+    J> λ n x → transportRefl _
+              ∙ sym (cong (-S^ n) (transportRefl x))
+
+-- 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)
+
+-- Interaction between -S^ and sym^
+σS-S^ : {k : ℕ} (n : ℕ) (x : S₊ (suc k))
+  → σS (-S^ n x) ≡ sym^ n (σS x)
+σS-S^ {k = k} zero x = refl
+σS-S^ {k = k} (suc n) x =
+  σ-invSphere k _ ∙ cong sym (σS-S^ n x)
+
+sphereFun↑-subst : {n m : ℕ} (k' k : ℕ) (p : k' ≡ k)
+  → (f : S₊ n → S₊ m → S₊ k') (x : S₊ _) (y : S₊ _)
+  → sphereFun↑ (λ x y → subst S₊ p (f x y)) x y
+   ≡ subst S₊ (cong suc p) (sphereFun↑ f x y)
+sphereFun↑-subst k' = J> λ f x y
+  → (λ i → sphereFun↑ (λ x₁ y₁ → transportRefl (f x₁ y₁) i) x y)
+   ∙ sym (transportRefl _)
+
+sphereFun↑-invSphere : {n m k : ℕ}
+  → (f : S₊ (suc n) → S₊ (suc m) → S₊ (suc k)) (x : S₊ _) (y : S₊ _)
+  → sphereFun↑ (λ x y → invSphere' (f x y)) x y
+   ≡ invSphere' (sphereFun↑ (λ x y → (f x y)) x y)
+sphereFun↑-invSphere {n = n} {m = m} {k = k} f north y = refl
+sphereFun↑-invSphere {n = n} {m = m} {k = k} f south y = refl
+sphereFun↑-invSphere {n = n} {m = m} {k = k} f (merid a i) y j =
+  lem k (f a y) j i
+  where
+  lem : (k : ℕ) (x : S₊ (suc k))
+    → (σS (invSphere' x)) ≡ (cong invSphere' (σS x))
+  lem k x =
+    sym (cong-∙ invSphere' (merid x) (sym (merid (ptSn _)))
+      ∙∙ cong (cong invSphere' (merid x) ∙_)
+          (rCancel (merid (ptSn _)))
+      ∙∙ (sym (rUnit _)
+        ∙ sym (σ-invSphere k x)
+        ∙ cong (σ (S₊∙ (suc k)))
+           (sym (invSphere'≡ x))))
+
+sphereFun↑^ : {n m k : ℕ} (l : ℕ)
+  → (f : S₊ (suc n) → S₊ (suc m) → S₊ (suc k)) (x : S₊ _) (y : S₊ _)
+  → sphereFun↑ (λ x y → -S^ l (f x y)) x y
+   ≡ -S^ l (sphereFun↑ (λ x y → (f x y)) x y)
+sphereFun↑^ zero f x y = refl
+sphereFun↑^ (suc l) f x y =
+    (λ i → sphereFun↑ (λ x₁ y₁ → invSphere'≡ (-S^ l (f x₁ y₁)) (~ i)) x y)
+  ∙ sphereFun↑-invSphere (λ x₁ y₁ → (-S^ l (f x₁ y₁))) x y
+  ∙ invSphere'≡ ((sphereFun↑ (λ x₁ y₁ → -S^ l (f x₁ y₁)) x y))
+  ∙ cong invSphere (sphereFun↑^ l f x y)
+
+S^-even : {k : ℕ} (n : ℕ) (x : S₊ k) → isEvenT n → -S^ n x ≡ x
+S^-even zero x p = refl
+S^-even (suc (suc n)) x p = invSphere² _ (-S^ n x) ∙ S^-even n x p
+
+private
+  move-transp-S^ : {k : ℕ} (n : ℕ) (p : k ≡ n) (m : ℕ)
+    → (x : S₊ k) (y : S₊ n)
+    → subst S₊ p (-S^ m x) ≡ y
+    → subst S₊ (sym p) (-S^ m y) ≡ x
+  move-transp-S^ =
+    J> λ m x → J> transportRefl _
+    ∙ cong (-S^ m) (transportRefl _)
+    ∙ -S^² m x
+
+  master-lem : ∀ {ℓ} {A : Type ℓ} {x : A} (p : x ≡ x) (coh : refl ≡ p)
+    (q : p ≡ p)
+    → Cube (λ j k → coh j (~ k)) (λ j k → coh j (~ k))
+            (λ i k → q k i) (λ i k → q i (~ k))
+            (λ j k → coh (~ k) j) λ j k → coh (~ k) j
+  master-lem = J> λ q → λ i j k → sym≡flipSquare q j (~ k) i
+
+  comm⌣S₁ : {m : ℕ} → (x : S¹) (y : S₊ (suc m))
+    → (x ⌣S y)
+     ≡ subst S₊ (+-comm (suc m) 1)
+                (-S^ (suc m) (y ⌣S x))
+  comm⌣S₁ {m = zero} x y =
+      (main x y ∙ invSphere'≡ (y ⌣S x))
+    ∙ sym (transportRefl (invSusp (y ⌣S x)))
+    where
+    pp-main : (x : S¹) → PathP (λ i → IdL⌣S {m = 1} x i
+            ≡ IdL⌣S {m = 1} x i) (cong (x ⌣S_) loop) (sym (σS x))
+    pp-main base i j = rCancel (merid base) (~ i) (~ j)
+    pp-main (loop k) i j =
+      master-lem _ (sym (rCancel (merid base)))
+                   (λ j k → σS (loop j) k) k i j
+
+    pp-help : (x : S¹) → PathP (λ i → IdL⌣S {m = 1} x i
+            ≡ IdL⌣S {m = 1} x i)
+                     (cong (x ⌣S_) loop) (cong invSphere' (σS x))
+    pp-help x = pp-main x
+      ▷ (rUnit _
+      ∙∙ cong (sym (σS x) ∙_) (sym (rCancel (merid base)))
+      ∙∙ sym (cong-∙ invSphere' (merid x) (sym (merid base))))
+
+    main : (x y : S¹) → (x ⌣S y) ≡ invSphere' (y ⌣S x)
+    main x base = IdL⌣S {m = 1} x
+    main x (loop i) = flipSquare (pp-help x) i
+  comm⌣S₁ {m = suc m} x y =
+      (main-lem x y
+     ∙ sym (transportRefl (invSphere' (sphereFun↑ (λ x₂ x₃ → x₃ ⌣S x₂) y x)))
+    ∙ sym (compSubstℕ {A = S₊} (cong suc (sym (+-comm (suc m) 1)))
+                                (+-comm (suc (suc m)) 1) refl
+       {x = invSphere' (sphereFun↑ (λ x₂ x₃ → x₃ ⌣S x₂) y x)}))
+    ∙ cong (subst S₊ (+-comm (suc (suc m)) 1))
+        (cong (subst S₊ (cong suc (sym (+-comm (suc m) 1))))
+          (sym (S^-lem (suc m) (sphereFun↑ (λ x₂ x₃ → x₃ ⌣S x₂) y x)))
+        ∙ -S^-transp _ (cong suc (sym (+-comm (suc m) 1)))
+           (suc (suc m) + suc m)
+           (sphereFun↑ (λ x₂ x₃ → x₃ ⌣S x₂) y x)
+        ∙ sym (-S^-comp (suc (suc m)) (suc m)
+           (subst S₊ (cong suc (sym (+-comm (suc m) 1)))
+             (sphereFun↑ (λ x₂ x₃ → x₃ ⌣S x₂) y x))))
+    ∙ cong (subst S₊ (+-comm (suc (suc m)) 1)
+         ∘ -S^ (suc (suc m)))
+         ((sym (-S^-transp _ (cong suc (sym (+-comm (suc m) 1))) (suc m)
+               (sphereFun↑ (λ x₂ x₃ → x₃ ⌣S x₂) y x))
+         ∙ cong (subst S₊ (cong suc (sym (+-comm (suc m) 1))))
+               (sym (sphereFun↑^ (suc m)
+                (λ x₂ x₃ →  (x₃ ⌣S x₂)) y x))
+         ∙ sym (sphereFun↑-subst _ _ (sym (+-comm (suc m) 1))
+           (λ x₂ x₃ →  (-S^ (suc m) (x₃ ⌣S x₂))) y x))
+         ∙ cong (λ (s : S₊ (suc m) → S¹ → S₊ (suc m + 1))
+                  → sphereFun↑ s y x)
+                 (refl
+               ∙ sym (funExt λ x → funExt λ y
+               → sym (move-transp-S^ _ (+-comm (suc m) 1)
+               (suc m) (x ⌣S y) (y ⌣S x)
+                (sym (comm⌣S₁ y x)))
+               ∙ refl)))
+    where
+    S^-lem : {k : ℕ} (m : ℕ) (x : S₊ k)
+      → -S^ (suc m + m) x ≡ invSphere' x
+    S^-lem m x =
+         sym (invSphere'≡ (-S^ (m + m) x))
+       ∙ cong invSphere' (-S^·2 m x)
+
+    ⌣S-south : (x : S¹) → x ⌣S south ≡ north
+    ⌣S-south base = refl
+    ⌣S-south (loop i) j =
+      (cong σS (sym (merid (ptSn (suc m))) )
+      ∙ rCancel (merid (ptSn _))) j i
+
+    PathP-main : (x : S¹) (a : S₊ (suc m))
+      → PathP (λ i → IdL⌣S x i ≡ ⌣S-south x i) (cong (x ⌣S_) (merid a))
+          (sym (σS (x ⌣S a)))
+    PathP-main base a j i = rCancel (merid north) (~ j) (~ i)
+    PathP-main (loop k) a j i =
+      hcomp (λ r → λ {(i = i0) → rCancel (merid north) j k
+                     ; (i = i1) → compPath-filler'
+                                   (cong σS (sym (merid (ptSn (suc m)))))
+                                   (rCancel (merid north)) r j k
+                     ; (j = i0) → σS (compPath-filler (merid a)
+                                        (sym (merid (ptSn (suc m)))) (~ r) i) k
+                     ; (j = i1) → σS (σS a k) (~ i)
+                     ; (k = i0) → rCancel (merid north) (~ j) (~ i)
+                     ; (k = i1) → rCancel (merid north) (~ j) (~ i)})
+            (master-lem _ (sym (rCancel (merid north)))
+             (λ i k → σS (loop i ⌣S a) k) k j i)
+
+    pp : (x : S¹) (a : S₊ (suc m))
+      → PathP (λ i → IdL⌣S x i ≡ ⌣S-south x i) (cong (x ⌣S_) (merid a))
+          (cong invSphere' (σS (x ⌣S a)))
+    pp x a = PathP-main x a
+        ▷ (rUnit _
+       ∙∙ cong (sym (σS (x ⌣S a)) ∙_) (sym (rCancel (merid north)))
+       ∙∙ sym (cong-∙ invSphere' (merid (x ⌣S a)) (sym (merid north))))
+
+    main-lem : (x : S¹) (y : S₊ (2 + m))
+      → (x ⌣S y)
+        ≡ invSphere' (sphereFun↑ (λ x₂ x₃ → x₃ ⌣S x₂) y x)
+    main-lem x north = IdL⌣S x
+    main-lem x south = ⌣S-south x
+    main-lem x (merid a i) j = pp x a j i
+
+  comm⌣S-lem : {n m : ℕ}
+    → ((x : S₊ (suc n)) (y : S₊ (suc (suc m)))
+       → (x ⌣S y) ≡ subst S₊ (+-comm (suc (suc m)) (suc n))
+                              (-S^ (suc (suc m) · (suc n)) (y ⌣S x)))
+    → (((x : S₊ (suc m)) (y : S₊ (suc (suc n)))
+       → (x ⌣S y) ≡ subst S₊ (+-comm (suc (suc n)) (suc m))
+                              (-S^ ((suc (suc n)) · (suc m)) (y ⌣S x))))
+    → (((x : S₊ (suc n)) (y : S₊ (suc m))
+       → (y ⌣S x) ≡ subst S₊ (sym (+-comm (suc m) (suc n)))
+                              (-S^ ((suc n) · (suc m)) (x ⌣S y))))
+    → (x : S₊ (suc (suc n))) (y : S₊ (suc (suc m)))
+    → (x ⌣S y) ≡ subst S₊ (+-comm (suc (suc m)) (suc (suc n)))
+                           (-S^ (suc (suc m) · (suc (suc n))) (y ⌣S x))
+  comm⌣S-lem {n = n} {m = m} ind1 ind2 ind3 x y =
+       cong (λ (s : S₊ (suc n) → S₊ (suc (suc m))
+            → S₊ ((suc n) + (suc (suc m)))) → sphereFun↑ s x y)
+            (funExt (λ x → funExt λ y
+            → ind1 x y))
+    ∙ (sphereFun↑-subst _ _ (+-comm (suc (suc m)) (suc n))
+                            (λ x y → -S^ (suc (suc m) · suc n) (y ⌣S x)) x y
+    ∙ cong (subst S₊ (cong suc (+-comm (suc (suc m)) (suc n))))
+        (sphereFun↑^ (suc (suc m) · suc n)  (λ x y → y ⌣S x) x y
+        ∙ cong (-S^ (suc (suc m) · suc n))
+           (cong (λ (s : S₊ (suc n) → S₊ (suc (suc m))
+                  → S₊ ((suc (suc m)) + (suc n))) → sphereFun↑ s x y)
+             (funExt (λ x → funExt λ y →
+              cong (λ (s : S₊ (suc m) → S₊ (suc n) → S₊ ((suc m) + (suc n)))
+                    → sphereFun↑ s y x)
+               (funExt λ x
+                      → funExt λ y
+                       → ind3 y x)
+            ∙ sphereFun↑-subst _ _ (sym (+-comm (suc m) (suc n)))
+                (λ x y → -S^ (suc n · suc m) (y ⌣S x)) y x
+            ∙ cong (subst S₊ (cong suc (sym (+-comm (suc m) (suc n)))))
+                   (sphereFun↑^ (suc n · suc m) (λ x y → (y ⌣S x)) y x)))
+            ∙ sphereFun↑-subst _ _  (sym (cong suc (+-comm (suc m) (suc n))))
+                ((λ x₁ x₂ →
+                 (-S^ (suc n · suc m)
+                      (sphereFun↑ (λ x₃ y₁ → y₁ ⌣S x₃) x₂ x₁)))) x y
+            ∙ cong (subst S₊ (sym (cong (suc ∘ suc) (+-comm (suc m) (suc n)))))
+                     ((sphereFun↑^ (suc n · suc m)
+                       ((λ x₁ x₂ → (sphereFun↑ (λ x₃ y₁ → y₁ ⌣S x₃) x₂ x₁))) x y
+                    ∙ cong (-S^ (suc n · suc m)) (lem₃ x y)))))
+    ∙ big-lem (suc n) (suc m)
+        _ (λ i → suc (suc (+-comm (suc m) (suc n) (~ i))))
+        _ (λ i → suc (+-comm (suc (suc m)) (suc n) i)) _
+        (sym (+-comm (suc (suc m)) (suc (suc n))))
+        (λ i → suc (+-comm (suc (suc n)) (suc m) i))
+        (sphereFun↑ (λ x₁ y₂ → y₂ ⌣S x₁) y x)
+    ∙ sym (cong (subst S₊ (+-comm (suc (suc m)) (suc (suc n))))
+           (cong (-S^ (suc (suc m) · suc (suc n)))
+            ((λ i → sphereFun↑ (λ x y → ind2 x y i) y x)
+           ∙ sphereFun↑-subst _ _
+               (+-comm (suc (suc n)) (suc m))
+                 (λ x y → -S^ (suc (suc n) · suc m) (y ⌣S x)) y x
+           ∙ cong (subst S₊ (cong suc (+-comm (suc (suc n)) (suc m))))
+              (sphereFun↑^ (suc (suc n) · suc m) (λ x y → y ⌣S x) y x)))))
+      where
+      ℕ-p : (n m : ℕ)
+        → (suc m · suc n + suc n · m)
+         ≡ (m + m) + ((n · m + n · m) + (suc n))
+      ℕ-p n m =
+        cong suc (cong (_+ (m + n · m)) (cong (n +_) (·-comm m (suc n)))
+               ∙ sym (+-assoc n (m + n · m) _)
+               ∙ +-comm n _
+               ∙ cong (_+ n) (+-assoc (m + n · m) m (n · m)
+                           ∙ cong (_+ (n · m))
+                                (sym (+-assoc m (n · m) m)
+                              ∙ cong (m +_) (+-comm (n · m) m)
+                              ∙ +-assoc m m (n · m))
+                              ∙ sym (+-assoc (m + m) (n · m) (n · m))))
+        ∙ sym (+-suc (m + m + (n · m + n · m)) n)
+        ∙ sym (+-assoc (m + m) (n · m + n · m) (suc n))
+
+      ℕ-p2 : (n m : ℕ) → suc m · n + n · m + 1 ≡ (((n · m) + (n · m)) + (suc n))
+      ℕ-p2 n m = (λ _ → ((n + m · n) + n · m) + 1)
+        ∙ cong (_+ 1) (sym (+-assoc n (m · n) (n · m))
+                      ∙ (λ i → +-comm n ((·-comm m n i) + n · m) i))
+        ∙ sym (+-assoc (n · m + n · m) n 1)
+        ∙ cong (n · m + n · m +_) (+-comm n 1)
+
+      big-lem : (n m : ℕ) {x : ℕ} (y : ℕ) (p : x ≡ y) (z : ℕ) (s : y ≡ z)
+                (d : ℕ) (r : z ≡ d) (t : x ≡ d)
+         (a : S₊ x)
+        → subst S₊ s (-S^ (suc m · n) (subst S₊ p (-S^ (n · m) (invSphere' a))))
+        ≡ subst S₊ (sym r)
+            (-S^ (suc m · suc n)
+             (subst S₊ t (-S^ (suc n · m) a)))
+      big-lem n m =
+        J> (J> (J> λ t a
+        → transportRefl _
+        ∙ cong (-S^ (n + m · n)) (transportRefl _)
+        ∙ sym (transportRefl _
+             ∙ cong (-S^ (suc m · suc n))
+                    ((λ i → subst S₊ (isSetℕ _ _ t refl i) (-S^ (m + n · m) a))
+                 ∙ transportRefl (-S^ (m + n · m) a) )
+             ∙ -S^-comp (suc m · suc n) (suc n · m) a
+             ∙ ((funExt⁻ (cong -S^ (ℕ-p n m)) a
+               ∙ (sym (-S^-comp (m + m) _ a)
+                ∙ -S^·2 m (-S^ (n · m + n · m + suc n) a))
+               ∙ funExt⁻ (cong -S^ (sym (ℕ-p2 n m))) a)
+              ∙ sym (-S^-comp (suc m · n + n · m) 1 a)
+              ∙ cong (-S^ (suc m · n + n · m))
+                 (sym (invSphere'≡ a)))
+             ∙ sym (-S^-comp (suc m · n) (n · m) (invSphere' a)) )))
+
+      lem₁ : (x :  S₊ (2 + n))
+        → sphereFun↑ (λ x₂ x₃ → sphereFun↑ (λ x₄ y₁ → y₁ ⌣S x₄) x₃ x₂) x north ≡ north
+      lem₁ north = refl
+      lem₁ south = refl
+      lem₁ (merid a i) j = rCancel (merid north) j i
+
+      lem₂ : (x :  S₊ (2 + n))
+        → sphereFun↑ (λ x₂ x₃
+          → sphereFun↑ (λ x₄ y₁ → y₁ ⌣S x₄) x₃ x₂) x south
+          ≡ north
+      lem₂ north = refl
+      lem₂ south = refl
+      lem₂ (merid a i) j = rCancel (merid north) j i
+
+      lem₃ : (x : S₊ (2 + n)) (y : S₊ (2 + m))
+         → (sphereFun↑ (λ x₁ x₂
+            → sphereFun↑ (λ x₃ y₁ → y₁ ⌣S x₃) x₂ x₁) x y)
+          ≡ invSphere' (sphereFun↑ (λ x₁ y₂ → y₂ ⌣S x₁) y x)
+      lem₃ x north = lem₁ x
+      lem₃ x south = lem₂ x
+      lem₃ x (merid a i) j = h j i
+        where
+        main : (x : _) → PathP (λ i → lem₁ x i ≡ lem₂ x i)
+               (cong (sphereFun↑ (λ x₂ x₃
+                → sphereFun↑ (λ x₄ y₁ → y₁ ⌣S x₄) x₃ x₂) x )
+                 (merid a))
+               (sym (σS (x ⌣S a)))
+        main north = cong sym (sym (rCancel (merid north)))
+        main south = cong sym (sym (rCancel (merid north)))
+        main (merid z i) j k =
+          master-lem _
+            (sym (rCancel (merid north)))
+            (cong (λ x → σS (x ⌣S a)) (merid z)) i j k
+
+        h : PathP (λ i → lem₁ x i ≡ lem₂ x i)
+                  (cong (sphereFun↑
+                   (λ x₂ x₃ → sphereFun↑ (λ x₄ y₁ → y₁ ⌣S x₄) x₃ x₂) x)
+                    (merid a)) (cong invSphere' (σS (x ⌣S a)))
+        h = main x
+          ▷ ((rUnit _ ∙ cong (sym (σS (x ⌣S a)) ∙_)
+              (sym (rCancel (merid north))))
+             ∙ sym (cong-∙ invSphere'
+                (merid (x ⌣S a)) (sym (merid (ptSn _)))))
+
+  comm⌣S₀ : (x : Bool) (m : ℕ) (y : S₊ m)
+    → PathP (λ i → S₊ (+-zero m (~ i))) (x ⌣S y) (y ⌣S x)
+  comm⌣S₀ false =
+    elim+2 (λ { false → refl ; true → refl})
+           (λ { base → refl ; (loop i) → refl})
+      ind
+    where
+    ind : (n : ℕ) →
+        ((y : S₊ (suc n)) →
+         PathP (λ i → S₊ (suc (+-zero n (~ i)))) y (y ⌣S false)) →
+        (y : Susp (S₊ (suc n))) →
+        PathP (λ i → Susp (S₊ (suc (+-zero n (~ i))))) y (y ⌣S false)
+    ind n p north i = north
+    ind n p south i = merid (ptSn (suc (+-zero n (~ i)))) (~ i)
+    ind n p (merid a j) i =
+      comp (λ k → Susp (S₊ (suc (+-zero n (~ i ∨ ~ k)))))
+           (λ r →
+           λ {(i = i0) → merid a j
+            ; (i = i1) →
+              σ (S₊∙ (suc (+-zero n (~ r)))) (p a r) j
+            ; (j = i0) → north
+            ; (j = i1) → merid (ptSn (suc (+-zero n (~ i ∨ ~ r)))) (~ i)})
+           (compPath-filler (merid a) (sym (merid (ptSn _))) i j)
+  comm⌣S₀ true m y = (λ i → ptSn (+-zero m (~ i))) ▷ (sym (IdL⌣S y))
+
+-- Graded commutativity
+comm⌣S : {n m : ℕ} (x : S₊ n) (y : S₊ m)
+  → (x ⌣S y) ≡ subst S₊ (+-comm m n) (-S^ (m · n) (y ⌣S x))
+comm⌣S {n = zero} {m = m} x y =
+  sym (fromPathP (symP {A = λ i → S₊ (+-zero m i)} ((comm⌣S₀ x m y))))
+  ∙ sym (cong (subst S₊ (+-zero m))
+        ((λ i → -S^ (0≡m·0 m (~ i)) (y ⌣S x))))
+comm⌣S {n = suc n} {m = zero} x y =
+  sym (fromPathP (comm⌣S₀ y (suc n) x))
+  ∙ (λ i → subst S₊ (isSetℕ _ _
+             (sym (+-comm (suc n) zero))
+             (+-comm zero (suc n)) i) (y ⌣S x))
+comm⌣S {n = suc zero} {m = suc m} x y =
+    comm⌣S₁ x y
+  ∙ cong (subst S₊ (+-comm (suc m) 1))
+     λ i → -S^ (·-identityʳ (suc m) (~ i)) (y ⌣S x)
+comm⌣S {n = suc (suc n)} {m = suc zero} x y =
+    sym (substSubst⁻ S₊ (+-comm 1 (suc (suc n))) (x ⌣S y))
+  ∙ cong (subst S₊ (+-comm 1 (suc (suc n))))
+        ((λ i → subst S₊ (isSetℕ _ _
+           (sym (+-comm 1 (suc (suc n)))) (+-comm (suc (suc n)) 1) i)
+           (x ⌣S y))
+      ∙ (sym (sym
+         (-S^-transp _ (+-comm (suc (suc n)) 1) (1 · suc (suc n))
+           (-S^ (suc (suc n)) (x ⌣S y)))
+            ∙ cong (subst S₊ (+-comm (suc (suc n)) 1))
+               (cong (-S^ (1 · suc (suc n)))
+                 (λ i → -S^ (·-identityˡ (suc (suc n)) (~ i)) (x ⌣S y))
+              ∙ -S^² (1 · suc (suc n)) (x ⌣S y)))))
+  ∙ sym (cong (subst S₊ (+-comm 1 (suc (suc n)))
+             ∘ -S^ (1 · suc (suc n))) (comm⌣S₁ y x))
+comm⌣S {n = suc (suc n)} {m = suc (suc m)} x y =
+  comm⌣S-lem comm⌣S comm⌣S
+    (λ x y → (sym (cong (subst S₊ (sym (+-comm (suc m) (suc n))))
+               (sym (-S^-transp _ (+-comm (suc m) (suc n))
+                 (suc n · suc m) (-S^ (suc m · suc n) (y ⌣S x)))
+             ∙ cong (subst S₊ (+-comm (suc m) (suc n)))
+                (cong (-S^ (suc n · suc m))
+                    (λ i → -S^ (·-comm (suc m) (suc n) i) (y ⌣S x))
+                  ∙ -S^² (suc n · suc m) (y ⌣S x) ))
+            ∙ subst⁻Subst S₊ (+-comm (suc m) (suc n)) (y ⌣S x) ))
+      ∙ sym (cong (subst S₊ (sym (+-comm (suc m) (suc n)))
+                 ∘ -S^ (suc n · suc m))
+         (comm⌣S x y))) x y
diff --git a/Cubical/HITs/Sn/Properties.agda b/Cubical/HITs/Sn/Properties.agda
index a3085a2f82..7eb740a4c0 100644
--- a/Cubical/HITs/Sn/Properties.agda
+++ b/Cubical/HITs/Sn/Properties.agda
@@ -20,6 +20,8 @@ open import Cubical.HITs.Sn.Base
 open import Cubical.HITs.Susp
 open import Cubical.HITs.Truncation
 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.HITs.Join renaming (joinS¹S¹→S³ to joinS¹S¹→S3)
 open import Cubical.Data.Bool hiding (elim)
@@ -35,6 +37,13 @@ open Iso
 σSn zero true = refl
 σSn (suc n) x = toSusp (S₊∙ (suc n)) x
 
+σS : {n : ℕ} → S₊ n → Path (S₊ (suc n)) (ptSn _) (ptSn _)
+σS {n = n} = σSn n
+
+σS∙ : {n : ℕ} → σS (ptSn n) ≡ refl
+σS∙ {n = zero} = refl
+σS∙ {n = suc n} = rCancel (merid (ptSn (suc n)))
+
 IsoSucSphereSusp : (n : ℕ) → Iso (S₊ (suc n)) (Susp (S₊ n))
 IsoSucSphereSusp zero = S¹IsoSuspBool
 IsoSucSphereSusp (suc n) = idIso
@@ -44,6 +53,11 @@ IsoSucSphereSusp∙ : (n : ℕ)
 IsoSucSphereSusp∙ zero = refl
 IsoSucSphereSusp∙ (suc n) = refl
 
+IsoSucSphereSusp∙' : (n : ℕ)
+  → Iso.fun (IsoSucSphereSusp n) (ptSn (suc n)) ≡ north
+IsoSucSphereSusp∙' zero = refl
+IsoSucSphereSusp∙' (suc n) = refl
+
 suspFunS∙ : {n : ℕ} → (S₊ n → S₊ n) → S₊∙ (suc n) →∙ S₊∙ (suc n)
 suspFunS∙ {n = zero} f =
   (λ x → Iso.inv S¹IsoSuspBool (suspFun f (Iso.fun S¹IsoSuspBool x))) , refl
@@ -643,6 +657,22 @@ invSphere {n = zero} = not
 invSphere {n = (suc zero)} = invLooper
 invSphere {n = (suc (suc n))} = invSusp
 
+-- sometimes also this version is useful
+invSphere' : {n : ℕ} → S₊ n → S₊ n
+invSphere' {n = zero} = not
+invSphere' {n = (suc zero)} = invLooper
+invSphere' {n = suc (suc n)} north = north
+invSphere' {n = suc (suc n)} south = north
+invSphere' {n = suc (suc n)} (merid a i) = σSn (suc n) a (~ i)
+
+invSphere'≡ : {n : ℕ} → (x : S₊ n) → invSphere' x ≡ invSphere x
+invSphere'≡ {n = zero} x = refl
+invSphere'≡ {n = suc zero} x = refl
+invSphere'≡ {n = suc (suc n)} north = merid (ptSn _)
+invSphere'≡ {n = suc (suc n)} south = refl
+invSphere'≡ {n = suc (suc n)} (merid a i) j =
+  compPath-filler (merid a) (sym (merid (ptSn _))) (~ j) (~ i)
+
 invSphere² : (n : ℕ) (x : S₊ n) → invSphere (invSphere x) ≡ x
 invSphere² zero = notnot
 invSphere² (suc zero) base = refl
diff --git a/Cubical/HITs/Susp/Base.agda b/Cubical/HITs/Susp/Base.agda
index 184d4a5b03..da71aa98ef 100644
--- a/Cubical/HITs/Susp/Base.agda
+++ b/Cubical/HITs/Susp/Base.agda
@@ -37,11 +37,19 @@ suspFun f south = south
 suspFun f (merid a i) = merid (f a) i
 
 -- pointed version
-suspFun∙ : {A B : Type ℓ} (f : A → B)
+suspFun∙ : {A : Type ℓ} {B : Type ℓ'} (f : A → B)
        → Susp∙ A →∙ Susp∙ B
 fst (suspFun∙ f) = suspFun f
 snd (suspFun∙ f) = refl
 
+suspFun↑ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
+  → (b : B)
+  → ((a : A) → Path B b b)
+  → Susp A → B
+suspFun↑ b f north = b
+suspFun↑ b f south = b
+suspFun↑ b f (merid a i) = f a i
+
 UnitIsoSuspUnit : Iso Unit (Susp Unit)
 fun UnitIsoSuspUnit _ = north
 inv UnitIsoSuspUnit _ = tt
diff --git a/Cubical/Homotopy/Group/Join.agda b/Cubical/Homotopy/Group/Join.agda
new file mode 100644
index 0000000000..e3015ab4c7
--- /dev/null
+++ b/Cubical/Homotopy/Group/Join.agda
@@ -0,0 +1,326 @@
+{-# OPTIONS --safe --lossy-unification #-}
+{-
+This file contains definition of homotopy groups in terms of joins:
+π*ₙₘ(A) := ∥ Sⁿ * Sᵐ →∙ A ∥₀
+and the fact that it agrees with the usual definition of homotopy groups.
+-}
+module Cubical.Homotopy.Group.Join where
+
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Base
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.Nat
+open import Cubical.Data.Bool
+
+open import Cubical.HITs.SetTruncation as ST
+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.Sn.Multiplication
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+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)
+  → (-Π f) ∘∙ join→Sphere∙ n m
+   ≡ -* (f ∘∙ join→Sphere∙ n m)
+fst (-Π≡-* f i) (inl x) = snd (-Π f) i
+fst (-Π≡-* f i) (inr x) = snd (-Π f) i
+fst (-Π≡-* {A = A} {n = n} {m = m} f i) (push a b j) = main i j
+  where
+  lem : (n : ℕ) (f : S₊∙ (suc n) →∙ A) (a : S₊ n)
+    → Square (cong (fst (-Π f)) (σS a))
+              (sym (snd f) ∙∙ cong (fst f) (sym (σS a)) ∙∙ snd f)
+              (snd (-Π f)) (snd (-Π f))
+  lem zero f false =
+    doubleCompPath-filler (sym (snd f)) (cong (fst f) (sym loop)) (snd f)
+  lem zero f true = doubleCompPath-filler (sym (snd f)) refl (snd f)
+  lem (suc n) f a =
+    (cong-∙ (fst (-Π f)) (merid a) (sym (merid (ptSn (suc n))))
+      ∙ cong₂ _∙_ refl (cong (cong (fst f)) (rCancel _))
+      ∙ sym (rUnit _))
+    ◁ doubleCompPath-filler
+      (sym (snd f)) (cong (fst f) (sym (σS a))) (snd f)
+
+  main : Square (cong (fst (-Π f)) (σS (a ⌣S b)))
+                (sym (Ω→ (f ∘∙ join→Sphere∙ n m) .fst (ℓS a b)))
+                (snd (-Π f)) (snd (-Π f))
+  main = lem _ f (a ⌣S b)
+    ▷ sym ((λ j → (sym (lUnit (snd f) (~ j))
+             ∙∙ sym (cong (fst f) (cong-∙ (join→Sphere n m)
+                       (push (ptSn n) (ptSn m))
+                       ((push a (ptSn m) ⁻¹)
+                     ∙∙ push a b
+                     ∙∙ (push (ptSn n) b ⁻¹)) j))
+             ∙∙ lUnit (snd f) (~ j)))
+      ∙ cong (sym (snd f) ∙∙_∙∙ snd f)
+             (cong (cong (fst f))
+                (congS sym
+                  ((cong₂ _∙_
+                    (cong σS (IdL⌣S _) ∙ σS∙)
+                    (cong-∙∙ (join→Sphere n m)
+                      (push a (ptSn m) ⁻¹) (push a b) (push (ptSn n) b ⁻¹)
+                  ∙ (cong₂ (λ p q → p ⁻¹ ∙∙ σS (a ⌣S b) ∙∙ q ⁻¹)
+                          (cong σS (IdL⌣S _) ∙ σS∙)
+                          (cong σS (IdR⌣S _) ∙ σS∙))
+                  ∙ sym (rUnit (σS (a ⌣S b)))))
+                ∙ sym (lUnit _)))))
+snd (-Π≡-* f i) j = lem i j
+  where
+  lem : Square (refl ∙ snd (-Π f)) refl (snd (-Π f)) refl
+  lem = sym (lUnit (snd (-Π f))) ◁ λ i j → (snd (-Π f)) (i ∨ j)
+
+-- ·Π is the same as +*
+·Π≡+* : ∀ {ℓ} {A : Pointed ℓ} {n m : ℕ}
+    (f g : S₊∙ (suc (n + m)) →∙ A)
+  → (∙Π f g ∘∙ join→Sphere∙ n m)
+   ≡ ((f ∘∙ join→Sphere∙ n m)
+   +* (g ∘∙ join→Sphere∙ n m))
+fst (·Π≡+* {A = A} f g i) (inl x) = snd (∙Π f g) i
+fst (·Π≡+* {A = A} f g i) (inr x) = snd (∙Π f g) i
+fst (·Π≡+* {A = A} {n = n} {m} f g i) (push a b j) = main i j
+  where
+  help : (n : ℕ) (f g : S₊∙ (suc n) →∙ A) (a : S₊ n)
+    → Square (cong (fst (∙Π f g)) (σS a))
+              (Ω→ f .fst (σS a) ∙ Ω→ g .fst (σS a))
+              (snd (∙Π f g)) (snd (∙Π f g))
+  help zero f g false = refl
+  help zero f g true =
+      rUnit refl
+    ∙ cong₂ _∙_ (sym (∙∙lCancel (snd f))) (sym (∙∙lCancel (snd g)))
+  help (suc n) f g a =
+      cong-∙ (fst (∙Π f g)) (merid a) (sym (merid (ptSn (suc n))))
+    ∙ cong (cong (fst (∙Π f g)) (merid a) ∙_)
+        (congS sym
+          (cong₂ _∙_
+            (cong (sym (snd f) ∙∙_∙∙ snd f)
+              (cong (cong (fst f)) (rCancel (merid (ptSn (suc n)))))
+              ∙ Ω→ f .snd)
+            (cong (sym (snd g) ∙∙_∙∙ snd g)
+              (cong (cong (fst g)) (rCancel (merid (ptSn (suc n)))))
+              ∙ Ω→ g .snd)
+           ∙ sym (rUnit refl)))
+    ∙ sym (rUnit _)
+
+  Ω→σ : ∀ {ℓ} {A : Pointed ℓ} (f : S₊∙ (suc (n + m)) →∙ A)
+    → Ω→ f .fst (σS (a ⌣S b))
+     ≡ Ω→ (f ∘∙ join→Sphere∙ n m) .fst (ℓS a b)
+  Ω→σ f =
+      cong (sym (snd f) ∙∙_∙∙ snd f)
+        (cong (cong (fst f))
+          (sym main))
+    ∙ λ i → Ω→ (lem (~ i)) .fst (ℓS a b)
+    where
+    main : cong (join→Sphere n m) (ℓS a b) ≡ σS (a ⌣S b)
+    main = cong-∙ (join→Sphere n m) _ _
+         ∙ cong₂ _∙_
+             (cong σS (IdL⌣S _) ∙ σS∙)
+             (cong-∙∙ (join→Sphere n m) _ _ _
+           ∙ (λ i → sym ((cong σS (IdL⌣S a) ∙ σS∙) i)
+                  ∙∙ σS (a ⌣S b)
+                  ∙∙ sym ((cong σS (IdR⌣S b) ∙ σS∙) i))
+           ∙ sym (rUnit (σS (a ⌣S b))) )
+         ∙ sym (lUnit (σS (a ⌣S b)))
+    lem : f ∘∙ join→Sphere∙ n m ≡ (fst f ∘ join→Sphere n m , snd f)
+    lem = ΣPathP (refl , (sym (lUnit _)))
+
+  main : Square (cong (fst (∙Π f g)) (σS (a ⌣S b)))
+                (Ω→ (f ∘∙ join→Sphere∙ n m) .fst (ℓS a b)
+               ∙ Ω→ (g ∘∙ join→Sphere∙ n m) .fst (ℓS a b))
+                (snd (∙Π f g)) (snd (∙Π f g))
+  main = help _ f g (a ⌣S b) ▷ cong₂ _∙_ (Ω→σ f) (Ω→σ g)
+snd (·Π≡+* {A = A} f g i) j = lem i j
+  where
+  lem : Square (refl ∙ snd (∙Π f g)) refl (snd (∙Π f g)) refl
+  lem = sym (lUnit (snd (∙Π f g))) ◁ λ i j → (snd (∙Π f g)) (i ∨ j)
+
+-- Homotopy groups in terms of joins
+π* : ∀ {ℓ} (n m : ℕ) (A : Pointed ℓ) → Type ℓ
+π* n m A = ∥ join∙ (S₊∙ n) (S₊∙ m) →∙ A ∥₂
+
+-- multiplication
+·π* : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} (f g : π* n m A) → π* n m A
+·π* = ST.rec2 squash₂ λ f g → ∣ f +* g ∣₂
+
+-π* : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} (f : π* n m A) → π* n m A
+-π* = ST.map -*
+
+1π* : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} → π* n m A
+1π* = ∣ const∙ _ _ ∣₂
+
+Iso-JoinMap-SphereMap : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ)
+  → Iso (join∙ (S₊∙ n) (S₊∙ m) →∙ A)
+         (S₊∙ (suc (n + m)) →∙ A)
+Iso-JoinMap-SphereMap n m = post∘∙equiv (joinSphereEquiv∙ n m)
+
+Iso-π*-π' : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ)
+  → Iso ∥ (join∙ (S₊∙ n) (S₊∙ m) →∙ A) ∥₂
+         ∥ (S₊∙ (suc (n + m)) →∙ A) ∥₂
+Iso-π*-π' n m = setTruncIso (Iso-JoinMap-SphereMap n m)
+
+private
+  J≃∙map : ∀ {ℓ ℓ' ℓ''} {A1 A2 : Pointed ℓ} {A : Pointed ℓ'}
+         → (e : A1 ≃∙ A2) {P : A1 →∙ A → Type ℓ''}
+       → ((f : A2 →∙ A) → P (f ∘∙ ≃∙map e))
+       → (f : _) → P f
+  J≃∙map  {ℓ'' = ℓ''} {A2 = A2} {A = A} =
+    Equiv∙J (λ A1 e → {P : A1 →∙ A → Type ℓ''}
+         → ((f : A2 →∙ A) → P (f ∘∙ ≃∙map e))
+          → (f : _) → P f)
+      λ {P} ind f
+      → subst P (ΣPathP (refl , sym (lUnit (snd f)))) (ind f)
+
+π*≡π' : ∀ {ℓ} {A : Pointed ℓ} {n m : ℕ}
+  (f g : π* n m A)
+  → Iso.fun (Iso-π*-π' n m) (·π* f g)
+  ≡ ·π' _ (Iso.fun (Iso-π*-π' n m) f) (Iso.fun (Iso-π*-π' n m) g)
+π*≡π' {A = A} {n} {m} = ST.elim2 (λ _ _ → isSetPathImplicit)
+  (J≃∙map (joinSphereEquiv∙ n m)
+    λ f → J≃∙map (joinSphereEquiv∙ n m)
+      λ g → cong ∣_∣₂
+        (cong (fun (Iso-JoinMap-SphereMap n m)) (sym (·Π≡+* f g))
+        ∙ ∘∙-assoc _ _ _
+        ∙ cong (∙Π f g ∘∙_) ret
+        ∙ ∘∙-idˡ (∙Π f g)
+        ∙ cong₂ ∙Π
+              ((sym (∘∙-idˡ f) ∙ cong (f ∘∙_) (sym ret)) ∙ sym (∘∙-assoc _ _ _))
+              (sym (∘∙-idˡ g) ∙ cong (g ∘∙_) (sym ret) ∙ sym (∘∙-assoc _ _ _))))
+  where
+  ret = ≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))}
+          (joinSphereEquiv∙ n m) .snd
+
+-π*≡-π' : ∀ {ℓ} {A : Pointed ℓ} {n m : ℕ}
+  (f : π* n m A)
+  → Iso.fun (Iso-π*-π' n m) (-π* f)
+  ≡ -π' _ (Iso.fun (Iso-π*-π' n m) f)
+-π*≡-π' {n = n} {m} =
+  ST.elim (λ _ → isSetPathImplicit)
+   (J≃∙map (joinSphereEquiv∙ n m)
+    λ f → cong ∣_∣₂
+      (cong (_∘∙ (≃∙map (invEquiv∙ (joinSphereEquiv∙ n m))))
+            (sym (-Π≡-* f))
+    ∙ ∘∙-assoc _ _ _
+    ∙ cong (-Π f ∘∙_) ret
+    ∙ ∘∙-idˡ (-Π f)
+    ∙ cong -Π (sym (∘∙-assoc _ _ _ ∙ cong (f ∘∙_) ret ∙ ∘∙-idˡ f))))
+  where
+  ret = ≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))}
+          (joinSphereEquiv∙ n m) .snd
+
+-- Homotopy groups in terms of joins
+π*Gr : ∀ {ℓ} (n m : ℕ) (A : Pointed ℓ) → Group ℓ
+fst (π*Gr n m A) = π* n m A
+1g (snd (π*Gr n m A)) = 1π*
+GroupStr._·_ (snd (π*Gr n m A)) = ·π*
+inv (snd (π*Gr n m A)) = -π*
+isGroup (snd (π*Gr n m A)) =
+  transport (λ i → IsGroup (p1 (~ i)) (p2 (~ i)) (p3 (~ i)))
+            (isGroup (π'Gr (n + m) A .snd))
+  where
+  p1 : PathP (λ i → isoToPath (Iso-π*-π' {A = A} n m) i)
+             1π* (1π' (suc (n + m)))
+  p1 = toPathP (cong ∣_∣₂ (transportRefl _ ∙ ΣPathP (refl , sym (rUnit refl))))
+
+  p2 : PathP (λ i → (f g : isoToPath (Iso-π*-π' {A = A} n m) i)
+                  → isoToPath (Iso-π*-π' {A = A} n m) i)
+              ·π* (·π' _)
+  p2 = toPathP (funExt λ f
+    → funExt λ g → transportRefl _
+    ∙ π*≡π' _ _
+    ∙ cong₂ (·π' (n + m))
+            (Iso.rightInv (Iso-π*-π' n m) _ ∙ transportRefl f)
+            (Iso.rightInv (Iso-π*-π' n m) _ ∙ transportRefl g))
+
+  p3 : PathP (λ i → isoToPath (Iso-π*-π' {A = A} n m) i
+                   → isoToPath (Iso-π*-π' {A = A} n m) i)
+             -π* (-π' _)
+  p3 = toPathP (funExt λ f → transportRefl _
+    ∙ -π*≡-π' _
+    ∙ cong (-π' (n + m))
+           (Iso.rightInv (Iso-π*-π' n m) _ ∙ transportRefl f))
+
+-- Homotopy groups in terms of joins agrees with usual definition
+π*Gr≅π'Gr : ∀ {ℓ} (n m : ℕ) (A : Pointed ℓ)
+  → GroupIso (π*Gr n m A) (π'Gr (n + m) A)
+fst (π*Gr≅π'Gr n m A) = Iso-π*-π' {A = A} n m
+snd (π*Gr≅π'Gr n m A) = makeIsGroupHom π*≡π'
+
+-- Functoriality
+π*∘∙fun : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
+  (n m : ℕ) (f : A →∙ B)
+   → π* n m A → π* n m B
+π*∘∙fun n m f  = ST.map (f ∘∙_)
+
+π*∘∙Hom : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
+  (n m : ℕ) (f : A →∙ B)
+  → GroupHom (π*Gr n m A) (π*Gr n m B)
+fst (π*∘∙Hom {A = A} {B = B} n m f) = π*∘∙fun n m f
+snd (π*∘∙Hom {A = A} {B = B} n m f) =
+  subst (λ ϕ → IsGroupHom (π*Gr n m A .snd) ϕ (π*Gr n m B .snd))
+        π*∘∙Hom'≡
+        (snd π*∘∙Hom')
+  where
+  GroupHomπ≅π*PathP : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') (n m : ℕ)
+    → GroupHom (π'Gr (n + m) A) (π'Gr (n + m) B)
+     ≡ GroupHom (π*Gr n m A) (π*Gr n m B)
+  GroupHomπ≅π*PathP A B n m i =
+    GroupHom (fst (GroupPath _ _) (GroupIso→GroupEquiv (π*Gr≅π'Gr n m A)) (~ i))
+             (fst (GroupPath _ _) (GroupIso→GroupEquiv (π*Gr≅π'Gr n m B)) (~ i))
+
+  π*∘∙Hom' : _
+  π*∘∙Hom' = transport (λ i → GroupHomπ≅π*PathP A B n m i)
+                       (π'∘∙Hom (n + m) f)
+
+  π*∘∙Hom'≡ : π*∘∙Hom' .fst ≡ π*∘∙fun n m f
+  π*∘∙Hom'≡ =
+    funExt (ST.elim (λ _ → isSetPathImplicit)
+           λ g → cong ∣_∣₂ (cong (inv (Iso-JoinMap-SphereMap n m))
+                   (transportRefl _
+                   ∙ cong (f ∘∙_) (transportRefl _))
+                 ∙ ∘∙-assoc _ _ _
+                 ∙ cong (f ∘∙_ )
+                        (∘∙-assoc _ _ _ ∙ cong (g ∘∙_)
+                         (≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))}
+                          (joinSphereEquiv∙ n m) .fst)
+                       ∙ ∘∙-idˡ g)))
diff --git a/Cubical/Homotopy/Group/Pi4S3/BrunerieExperiments.agda b/Cubical/Homotopy/Group/Pi4S3/BrunerieExperiments.agda
index c65fba931e..63a49ba510 100644
--- a/Cubical/Homotopy/Group/Pi4S3/BrunerieExperiments.agda
+++ b/Cubical/Homotopy/Group/Pi4S3/BrunerieExperiments.agda
@@ -21,7 +21,7 @@ open import Cubical.Data.Int
 open import Cubical.HITs.S1 hiding (encode)
 open import Cubical.HITs.S2
 open import Cubical.HITs.S3
-open import Cubical.HITs.Join
+open import Cubical.HITs.Join hiding (join∙)
 open import Cubical.HITs.SetTruncation as SetTrunc
 open import Cubical.HITs.GroupoidTruncation as GroupoidTrunc
 open import Cubical.HITs.2GroupoidTruncation as 2GroupoidTrunc
diff --git a/Cubical/Homotopy/Whitehead.agda b/Cubical/Homotopy/Whitehead.agda
index 99abb89222..2daec9e530 100644
--- a/Cubical/Homotopy/Whitehead.agda
+++ b/Cubical/Homotopy/Whitehead.agda
@@ -20,6 +20,7 @@ open import Cubical.HITs.Wedge
 open import Cubical.HITs.SetTruncation
 
 open import Cubical.Homotopy.Group.Base
+open import Cubical.Homotopy.Loopspace
 
 open Iso
 open 3x3-span
@@ -408,3 +409,105 @@ module _ (A B : Type) (a₀ : A) (b₀ : B) where
       ∙∙ sym (lUnit (λ i₁ → north , σB a (~ i₁))))
        ∙ (λ 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)
+    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))
+      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)
diff --git a/Cubical/Papers/Pi4S3-JournalVersion.agda b/Cubical/Papers/Pi4S3-JournalVersion.agda
new file mode 100644
index 0000000000..212a444a0d
--- /dev/null
+++ b/Cubical/Papers/Pi4S3-JournalVersion.agda
@@ -0,0 +1,397 @@
+{-
+Please do not move this file. Changes should only be made if
+necessary.
+
+This file contains pointers to the code examples and main results from
+the paper:
+
+  Formalising and computing the fourth homotopy group of the 3-sphere in Cubical Agda
+-}
+
+-- The "--safe" flag ensures that there are no postulates or
+-- unfinished goals
+{-# OPTIONS --safe --cubical #-}
+
+module Cubical.Papers.Pi4S3-JournalVersion where
+
+-- Misc.
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+
+-- 2
+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
+  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 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²
+
+-- 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.BlakersMassey
+module BM = BlakersMassey□
+open BM
+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³
+  hiding (π)
+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
+
+
+------ 2. HOMOTOPY TYPE THEORY IN Cubical Agda ------
+
+--- 2.1 Elementary HoTT notions and Cubical Agda notations ---
+
+-- Booleans
+open Boolean using (Bool)
+
+-- Unit
+open UnitType renaming (Unit to 𝟙)
+
+-- S¹
+open Circle using (S¹)
+
+-- Non-dependent paths and refl
+open Prelude using (_≡_ ; refl)
+
+-- funExt, funExt⁻, cong
+open Prelude using (funExt; funExt⁻; cong)
+
+-- PathP
+open Prelude using (PathP)
+
+-- cirlce-indution
+open Circle using (elim)
+
+--- 2.2 More higher inductive types ---
+
+-- suspension
+open Suspensions using (Susp)
+
+-- spheres
+open Spheres using (S₊)
+
+-- pushouts
+open Pushouts using (Pushout)
+
+-- wedge sums
+open Wedges using (_⋁_)
+
+-- joins
+open Joins using (join)
+
+-- cofibres
+open Pushouts using (cofib)
+
+-- ∇ and i∨
+open Wedges using (fold⋁ ; ⋁↪)
+∇ = fold⋁
+i∨ = ⋁↪
+
+--- 2.3 Truncation levels and n-truncations  ---
+
+-- propositional and general truncation
+-- note that the indexing is off by 2!
+open PT using (∥_∥₁)
+open Trunc using (∥_∥_)
+
+--- 2.4 Univalence, loop spaces, and H-spaces ---
+
+-- Univalence, ua
+open Univ using (univalence ; ua)
+
+-- Loop spaces
+open Loopy using (Ω)
+
+-- H-spaces
+open H-Spaces using (HSpace)
+
+------ 3. First results on homotopy groups of spheres ------
+
+-- homotopy groups (function and loop space definition, respectively)
+-- Note that the indexing is off by 1.
+open HomotopyGroups using (π'Gr ; πGr)
+
+-- Proposition 3.2 - Long exact sequence of homotoy groups
+module ExactSeq = πLES
+
+-- σ (definition 3.3)
+open Suspensions renaming (toSusp to σ)
+
+-- Proposition 3.4: Sⁿ * Sᵐ ≃ Sⁿ⁺ᵐ⁺¹
+open Spheres using (IsoSphereJoin)
+
+-- Definition 3.5 and Proposition 3.6 (Hopf map),
+-- Phrased somewhat differently in the paper.
+open HopfMap using (HopfMap)
+open S¹Hopf using (IsoS³TotalHopf)
+
+-- Lemma 3.7 (connectedness of spheres)
+-- Note that the indexing is off by 2.
+open Spheres using (sphereConnected)
+
+-- Proposition 3.8 (πₙSᵐ vanishishing for n < m)
+isContr-πₙSᵐ-low : (n m : ℕ) → n < m → isContr (π n (S₊∙ m))
+isContr-πₙSᵐ-low n m l =
+  transport (cong isContr (sym (ua h)))
+     (∣ const∙ (S₊∙ n) _ ∣₂
+     , ST.elim (λ _ → isOfHLevelPath 2 squash₂ _ _)
+       λ f → refl)
+  where
+  open import Cubical.HITs.SetTruncation as ST
+  con-lem : isConnected (2 + n) (S₊ m)
+  con-lem = isConnectedSubtr (suc (suc n)) (fst l)
+             (subst (λ n → isConnected n (S₊ m))
+               (sym (+-suc (fst l) (suc n) ∙ cong suc (snd l)))
+                (sphereConnected m))
+
+  h : π n (S₊∙ m) ≃ π' n (Unit , tt)
+  h = compEquiv (isoToEquiv (πTruncIso n))
+       (compEquiv (pathToEquiv (cong (π n)
+          (ua∙ (isoToEquiv (isContr→Iso (con-lem) isContrUnit)) refl)))
+          (pathToEquiv (cong ∥_∥₂ (isoToPath (IsoΩSphereMap n)))))
+
+-- Theorem 3.9 (Freudenthal Suspension Theorem)
+open Freudenthal using (isConnectedσ) -- formalized by Evan Cavallo
+
+-- Corollary 3.10 (πₙSⁿ≅ℤ with identity as generator)
+open Stable using (πₙ'Sⁿ≅ℤ ; πₙ'Sⁿ≅ℤ-idfun∙)
+
+-- Proposition 3.11 and Corollary 3.12 (π₃S²≅ℤ with Hopf map as generator)
+open π₃S² using (π₃S²≅ℤ ; π₂S³-gen-by-HopfMap)
+
+------ 4. THE BRUNERIE NUMBER ------
+{- The formalisation of this part does not
+follow the paper exactly. For this reason, we only give
+the crucial results here -}
+
+--- 4.1 The James construction ---
+-- Expository section only. No formalisation following this part of
+-- the paper.
+
+--- 4.2 The James construction ---
+
+-- Lemma 3 (the family of automorphisms on ∥J₂S²∥₃
+open James₁ using (∥Pushout⋁↪fold⋁S²∥₅≃∥Pushout⋁↪fold⋁S²∥₅)
+
+
+---- B. Formalization of the James construction ----
+
+-- Definition 4.4: J₂S²
+open James₁ using (Pushout⋁↪fold⋁S₊2)
+
+-- S²-HIT
+open Sphere using (S²)
+
+-- Lemma 4.5
+-- Omitted (used implicitly)
+
+-- Lemma 4.6 (the family of automorphisms on ∥J₂S²∥₃
+open James₁ using (∥Pushout⋁↪fold⋁S²∥₅≃∥Pushout⋁↪fold⋁S²∥₅)
+
+-- Proposition 4.7: Ω ∥S³∥₄ ≃ ∥J₂S²∥₃
+open James₁ using (IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅)
+
+
+--- 4.3. Definition of the Brunerie number ---
+
+-- Definition 4.8: W + whitehead product
+W = joinTo⋁
+open Whitehead using ([_∣_]₂)
+
+-- Theorem 4.9 is omitted as it is used implicitly in the proof of the main result
+
+-- Theorem 4.10 Blakers-Massey
+open BM using (isConnected-toPullback) -- formalized primarily (in a different form) by Kang Rongji
+
+-- Definition 4.11: The Brunerie number (note that, in the formalization
+-- we have worked defined β as the image of the Hopf Invariant
+-- directly)
+open BNumber using (Brunerie)
+
+-- Corollary 4.12: π₄S³ ≅ ℤ/βℤ
+open BNumber using (BrunerieIso)
+
+
+------ 5. BRUNERIE'S PROOF THAT |β| ≡ 2 ------
+
+---- A. Cohomology Theory / B. Formalization of Chapter 5----
+-- All formalizations marked with (BLM22) are borrowed from Brunerie,
+-- Ljungström, and Mörtberg, “Synthetic Integral Cohomology in Cubical
+-- Agda"
+
+--- 5.1 Cohomology and the Hopf invariant ---
+
+-- Eilenberg-MacLane spaces and cohomology groups (BLM22)
+open cohom using (coHomK)
+open cohomGr using (coHomGr)
+
+-- addition (BLM22)
+open cohomGr using (_+ₖ_)
+
+-- the cup product (BLM22)
+open cup using (_⌣ₖ_ ; _⌣_)
+
+-- Kₙ ≃ ΩKₙ₊₁ (BLM22)
+open cohomProps using (Kn≃ΩKn+1)
+
+-- Mayer Vietoris (BLM22)
+open MV using ( Ker-i⊂Im-d ; Im-d⊂Ker-i
+              ; Ker-Δ⊂Im-i ; Im-i⊂Ker-Δ
+              ; Ker-d⊂Im-Δ ; Im-Δ⊂Ker-d)
+
+-- Lemma 5.1 (cohomology of cofibers S³ → S²)
+open HI using (Hopfβ-Iso)
+
+-- Definition 5.2 (Hopf Invariant)
+open HI using (HopfInvariant-π')
+
+-- Proposition 5.3 (The Hopf invariant is a homomorphism)
+open HI-hom using (GroupHom-HopfInvariant-π')
+
+-- Proposition 5.4 (The Hopf invariant of the Brunerie element is ±2)
+open HI-β using (Brunerie'≡2)
+
+-- Lemma 5.5 -- only included for presentation, omitted from frmalization
+
+--- 5.1 The Gysin sequence ---
+
+-- Proposition 5.6 (Gysin sequence)
+open Gysin using (Im-⌣e⊂Ker-p ; Ker-p⊂Im-⌣e
+                ; Im-Susp∘ϕ⊂Ker-⌣e ; Ker-⌣e⊂Im-Susp∘ϕ
+                ; Im-ϕ∘j⊂Ker-p ; Ker-p⊂Im-ϕ∘j)
+
+-- Proposition 5.7 : CP² fibration
+-- Indirect, but see in particular
+open HopfMap using (fibr)
+
+-- Proposition 5.8 : Iterated Hopf Construction.
+-- Indirect, but see in particular:
+open Hopf using (joinIso₂)
+
+-- Proposition 5.9 : ∣ HI hopf ∣ ≡ 1
+open HopfMap using (HopfInvariant-HopfMap)
+
+-- Theorem 5.10: π₄S³≅ℤ/2ℤ
+open π₄S³ using (π₄S³≃ℤ/2ℤ)
+
+--- Formalisation of the Gysin sequence. ---
+-- Lemma 5.11: (BLM22)
+open cupLaws using (assoc-helper)
+
+-- proof that e₂ : H²(CP²) is a generator by computation
+-- (the field with refl is where the computation happens)
+open HopfMap using (isGenerator≃ℤ-e)
+
+------ 6. THE SIMPLIFIED NEW PROOF AND NORMALISATION OF A BRUNERIE NUMBER ------
+
+--- 6.1. Interlude: joins and smash products of spheres ---
+
+-- Smash product (not defined as an implicit HIT)
+open SmashProd using (_⋀_)
+
+-- Lemmas 6.1 and 6.2
+-- Omitted (included for presentation purposes, not used explicitly in
+-- formalisation)
+
+-- Definition of pinch map
+open SmashProd renaming (Join→SuspSmash to pinch)
+
+-- Proposition 6.3 (pinch is an equivalence)
+open SmashProd using (SmashJoinIso)
+
+-- Definition of Fₙₘ
+open SMult renaming (join→Sphere to F)
+
+-- Proposition 6.4 (Fₙ,ₘ is an equivalence)
+open SMult using (IsoSphereJoin)
+
+-- Propositions 6.5 & 6.6 (graded commutativity and associativity)
+open SMult using (comm⌣S ; assoc⌣S)
+
+--- 6.2. Homotopy groups in terms of joins.
+
+-- Definition 6.7
+open JoinGroup using (π*)
+
+-- Addition +*
+open JoinGroup using (_+*_)
+
+-- Proposition 6.8
+open JoinGroup using (·Π≡+*)
+
+-- Proposition 6.9
+open JoinGroup using (π*Gr≅π'Gr)
+
+-- Proposition 6.10
+open JoinGroup using (π*∘∙Hom)
+
+--- 6.3. The new synthetic proof that π₄(S³) ≅ ℤ/2ℤ
+-- A relatively detailed accound of the proof is given in the formalisation:
+open Direct
+-- Note that the numbering of the ηs is shifted, with
+-- η₁ being ∣ ∇ ∘ W ∣, η₂ being η₁ and η₃ being η₂.
+open Direct using (η₁ ; η₂ ; η₃)
+
+-- computation of η₂: the alternative definition and the computation
+open Direct using (η₃' ; computerIsoη₃)
+
+--- 6.4. A stand-alone proof of Brunerie’s theorem?
+-- Theorem 6.18
+-- Not formalised explicitly
+
+-- Definition of generalised Whitehead products ·w
+open Whitehead using (_·w_)
+
+-- Proposition 6.22 (including Lemmas 19 and 20 and Proposition 6.21)
+open Whitehead using (isConst-Susp·w)
+
+-- Theorem 6.23
+-- Follows directly from above but not formalised explicitly (awaiting
+-- refactoring of some code in the library)