Minor fix: improved definition of whitehead products

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

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)

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

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