change def of wh prod

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/Sn/Properties.agda

@@ -33,8 +33,7 @@ private
 open Iso
 
 σSn : (n : ℕ) → S₊ n → Path (S₊ (suc n)) (ptSn (suc n)) (ptSn (suc n))
-σSn zero false = loop
-σSn zero true = refl
+σSn zero = cong SuspBool→S¹ ∘ merid
 σSn (suc n) x = toSusp (S₊∙ (suc n)) x
 
 σS : {n : ℕ} → S₊ n → Path (S₊ (suc n)) (ptSn _) (ptSn _)

Cubical/HITs/Susp/Properties.agda

@@ -378,3 +378,12 @@ toSusp-invSusp A (merid a i) j =
           λ r → flipSquare (sym (rUnit refl)
                 ◁ (flipSquare (sym (sym≡cong-sym r))
                 ▷ rUnit refl)))
+
+-- co-H-space structure
+·Susp : ∀ {ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
+        (f g : Susp∙ (typ A) →∙ B) → Susp∙ (typ A) →∙ B
+fst (·Susp A {B = B} f g) north = pt B
+fst (·Susp A {B = B} f g) south = pt B
+fst (·Susp A {B = B} f g) (merid a i) =
+  (Ω→ f .fst (toSusp A a) ∙ Ω→ g .fst (toSusp A a)) i
+snd (·Susp A f g) = refl

Cubical/Homotopy/Group/Base.agda

@@ -117,12 +117,7 @@ fst (∙Π {A = A} {n = suc zero} (f , p) (g , q)) base = pt A
 fst (∙Π {A = A} {n = suc zero} (f , p) (g , q)) (loop j) =
   ((sym p ∙∙ cong f loop ∙∙ p) ∙ (sym q ∙∙ cong g loop ∙∙ q)) j
 snd (∙Π {A = A} {n = suc zero} (f , p) (g , q)) = refl
-fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) north = pt A
-fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) south = pt A
-fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) (merid a j) =
-   ((sym p ∙∙ cong f (merid a ∙ sym (merid (ptSn (suc n)))) ∙∙ p)
-  ∙ (sym q ∙∙ cong g (merid a ∙ sym (merid (ptSn (suc n)))) ∙∙ q)) j
-snd (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) = refl
+∙Π {A = A} {n = suc (suc n)} = ·Susp (S₊∙ (suc n))
 
 -Π : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
   → (S₊∙ n →∙ A)

Cubical/Homotopy/Group/Pi4S3/BrunerieNumber.agda

@@ -38,6 +38,7 @@ open import Cubical.Data.Int
 open import Cubical.HITs.S1
 open import Cubical.HITs.Sn
 open import Cubical.HITs.Sn.Multiplication
+open import Cubical.HITs.Join
 open import Cubical.HITs.Susp
 open import Cubical.HITs.Wedge
 open import Cubical.HITs.Pushout
@@ -399,21 +400,22 @@ module _ where
 -- first need the following:
 fold∘W≡Whitehead :
         fst (π'∘∙Hom 2 (fold∘W , refl)) ∣ idfun∙ (S₊∙ 3) ∣₂
-      ≡ ∣ [ idfun∙ (S₊∙ 2) ∣ idfun∙ (S₊∙ 2) ]₂ ∣₂
+      ≡ ∣ [ idfun∙ (S₊∙ 2) ∣ idfun∙ (S₊∙ 2) ] ∣₂
 fold∘W≡Whitehead =
-  pRec (squash₂ _ _)
-    (cong ∣_∣₂)
-    (indΠ₃S₂ _ _
-      (funExt (λ x → funExt⁻ (sym (cong fst (id∨→∙id {A = S₊∙ 2}))) (W x))))
+  cong ∣_∣₂ (ΣPathP (funExt (main ∘ sphere→Join 1 1) , refl))
   where
-  indΠ₃S₂ : ∀ {ℓ} {A : Pointed ℓ}
-    → (f g : A →∙ S₊∙ 2)
-      → fst f ≡ fst g → ∥ f ≡ g ∥₁
-  indΠ₃S₂ {A = A} f g p =
-    trRec squash₁
-     (λ r → ∣ ΣPathP (p , r) ∣₁)
-      (isConnectedPathP 1 {A = (λ i → p i (snd A) ≡ north)}
-        (isConnectedPathSⁿ 1 (fst g (pt A)) north) (snd f) (snd g) .fst )
+  main : (x : _) → fold⋁ (joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1} x)
+                  ≡ fst [ idfun∙ (Susp S¹ , north)
+                         ∣ idfun∙ (Susp S¹ , north) ]-pre x
+  main (inl x) = refl
+  main (inr x) = refl
+  main (push a b i) j = help j i
+    where
+    help : cong (fold⋁ ∘ joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1}) (push a b)
+         ≡ (σS b ∙ refl) ∙ σS a ∙ refl
+    help = cong-∙∙ fold⋁ _ _ _
+         ∙ doubleCompPath≡compPath _ _ _
+         ∙ cong₂ _∙_ (rUnit _) (sym (lUnit (σS a)) ∙ rUnit (σS a))
 
 BrunerieIsoAbstract : GroupEquiv (π'Gr 3 (S₊∙ 3)) (abstractℤGroup/ Brunerie)
 BrunerieIsoAbstract =
@@ -431,12 +433,10 @@ BrunerieIsoAbstract =
     fst (π'∘∙Hom 2 (fold∘W , refl))
          (Iso.inv (fst (πₙ'Sⁿ≅ℤ 2)) 1)
      ≡ [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π'
-  mainPath =
-      cong (fst (π'∘∙Hom 2 (fold∘W , refl)))
+  mainPath = cong (fst (π'∘∙Hom 2 (fold∘W , refl)))
            (cong (Iso.inv (fst (πₙ'Sⁿ≅ℤ 2))) (sym (πₙ'Sⁿ≅ℤ-idfun∙ 2))
            ∙ (Iso.leftInv (fst (πₙ'Sⁿ≅ℤ 2)) ∣ idfun∙ (S₊∙ 3) ∣₂))
-    ∙ fold∘W≡Whitehead
-    ∙ cong ∣_∣₂ (sym ([]≡[]₂ (idfun∙ (S₊∙ 2)) (idfun∙ (S₊∙ 2))))
+           ∙ fold∘W≡Whitehead
 
   main : _ ≡ Brunerie
   main i = abs (HopfInvariant-π' 0 (mainPath i))

Cubical/Homotopy/HopfInvariant/Brunerie.agda

@@ -391,8 +391,7 @@ Brunerie'≡2 = BrunerieNumLem.main (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1) Hⁿ
 -- number in Brunerie (2016)
 Brunerie'≡Brunerie : [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π' ≡ ∣ fold∘W , refl ∣₂
 Brunerie'≡Brunerie =
-    cong ∣_∣₂ ([]≡[]₂ (idfun∙ (S₊∙ 2)) (idfun∙ (S₊∙ 2)) )
-  ∙ sym fold∘W≡Whitehead
+    sym fold∘W≡Whitehead
   ∙ cong ∣_∣₂ (∘∙-idˡ (fold∘W , refl))
 
 -- And we get the main result

Cubical/Homotopy/Whitehead.agda

@@ -26,6 +26,25 @@ open import Cubical.Homotopy.Loopspace
 open Iso
 open 3x3-span
 
+-- Whitehead product (main definition)
+[_∣_]-pre : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (S₊∙ (suc n) →∙ X)
+       → (S₊∙ (suc m) →∙ X)
+       → join∙ (S₊∙ n) (S₊∙ m) →∙ X
+fst ([_∣_]-pre {X = X} {n = n} {m = m} f g) (inl x) = pt X
+fst ([_∣_]-pre {X = X} {n = n} {m = m} f g) (inr x) = pt X
+fst ([_∣_]-pre {n = n} {m = m} f g) (push a b i) =
+  (Ω→ g .fst (σS b) ∙ Ω→ f .fst (σS a)) i
+snd ([_∣_]-pre {n = n} {m = m} f g) = refl
+
+[_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (S₊∙ (suc n) →∙ X)
+       → (S₊∙ (suc m) →∙ X)
+       → S₊∙ (suc (n + m)) →∙ X
+[_∣_] {n = n} {m = m} f g =
+  [ f ∣ g ]-pre ∘∙ (sphere→Join n m , IsoSphereJoin⁻Pres∙ n m)
+
+-- Whitehead product (as a composition)
 joinTo⋁ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
  → join (typ A) (typ B)
  → (Susp (typ A) , north) ⋁ (Susp (typ B) , north)
@@ -36,63 +55,100 @@ joinTo⋁ {A = A} {B = B} (push a b i) =
   ∙∙ sym (push tt)
   ∙∙ λ i → inl (σ A a i)) i
 
--- Whitehead product (main definition)
-[_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+[_∣_]comp : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
        → (S₊∙ (suc n) →∙ X)
        → (S₊∙ (suc m) →∙ X)
        → S₊∙ (suc (n + m)) →∙ X
-fst ([_∣_] {X = X} {n = n} {m = m} f g) x =
-  _∨→_ (f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
-        (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))
-        (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}
-          (inv (IsoSphereJoin n m) x))
-snd ([_∣_] {n = n} {m = m} f g) =
-  cong (_∨→_ (f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
-       (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m)))
-       (cong (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}) (IsoSphereJoin⁻Pres∙ n m))
-    ∙ cong (fst g) (IsoSucSphereSusp∙ m)
-    ∙ snd g
-
--- For Sⁿ, Sᵐ with n, m ≥ 2, we can avoid some bureaucracy. We make
--- a separate definition and prove it equivalent.
-[_∣_]-pre : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (S₊∙ (suc (suc n)) →∙ X)
-       → (S₊∙ (suc (suc m)) →∙ X)
-       → join (typ (S₊∙ (suc n))) (typ (S₊∙ (suc m))) → fst X
-[_∣_]-pre {n = n} {m = m} f g x =
-  _∨→_ f g
-        (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
-        x)
-
-[_∣_]₂ : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (S₊∙ (suc (suc n)) →∙ X)
-       → (S₊∙ (suc (suc m)) →∙ X)
-       → S₊∙ (suc ((suc n) + (suc m))) →∙ X
-fst ([_∣_]₂ {n = n} {m = m} f g) x =
-  [ f ∣ g ]-pre (inv (IsoSphereJoin (suc n) (suc m)) x)
-snd ([_∣_]₂ {n = n} {m = m} f g) =
-    cong ([ f ∣ g ]-pre) (IsoSphereJoin⁻Pres∙ (suc n) (suc m))
-  ∙ snd g
-
-[]≡[]₂ : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
-       → (f : (S₊∙ (suc (suc n)) →∙ X))
-       → (g : (S₊∙ (suc (suc m)) →∙ X))
-       → [ f ∣ g ] ≡ [ f ∣ g ]₂
-[]≡[]₂ {n = n} {m = m} f g =
-  ΣPathP (
-    (λ i x → _∨→_ (∘∙-idˡ f i)
-                    (∘∙-idˡ g i)
-                (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
-                 (inv (IsoSphereJoin (suc n) (suc m)) x)))
-  , (cong (cong (_∨→_ (f ∘∙ idfun∙ _)
-                       (g ∘∙ idfun∙ _))
-       (cong (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)})
-             (IsoSphereJoin⁻Pres∙ (suc n) (suc m))) ∙_)
-                (sym (lUnit (snd g)))
-  ◁ λ j → (λ i → _∨→_ (∘∙-idˡ f j)
-                        (∘∙-idˡ g j)
-           ( joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
-          ((IsoSphereJoin⁻Pres∙ (suc n) (suc m)) i))) ∙ snd g))
+[_∣_]comp {n = n} {m = m} f g =
+    (((f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
+  ∨→ (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))
+    , cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f)
+  ∘∙ ((joinTo⋁ {A = S₊∙ n} {B = S₊∙ m} , sym (push tt))))
+  ∘∙ (inv (IsoSphereJoin n m) , IsoSphereJoin⁻Pres∙ n m)
+
+[]comp≡[] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (f : (S₊∙ (suc n) →∙ X))
+       → (g : (S₊∙ (suc m) →∙ X))
+       → [ f ∣ g ]comp ≡ [ f ∣ g ]
+[]comp≡[] {X = X} {n = n} {m} f g =
+  cong (_∘∙ (sphere→Join n m , IsoSphereJoin⁻Pres∙ n m)) (main n m f g)
+    where
+    ∨fun : {n m : ℕ} (f : (S₊∙ (suc n) →∙ X)) (g : (S₊∙ (suc m) →∙ X))
+      → ((_ , inl north) →∙ X)
+    ∨fun {n = n} {m} f g =
+       ((f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n)) ∨→
+       (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))
+       , cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f)
+
+    open import Cubical.Foundations.Path
+    main : (n m : ℕ) (f : (S₊∙ (suc n) →∙ X)) (g : (S₊∙ (suc m) →∙ X))
+      → (∨fun f g ∘∙ (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m} , sym (push tt)))
+      ≡ [ f ∣ g ]-pre
+    main n m f g =
+      ΣPathP ((funExt (λ { (inl x) → rp
+                         ; (inr x) → lp
+                         ; (push a b i) j → pushcase a b j i}))
+          , ((cong₂ _∙_ (symDistr _ _) refl
+          ∙ sym (assoc _ _ _)
+          ∙ cong (rp ∙_) (rCancel _)
+          ∙ sym (rUnit rp))
+          ◁ λ i j → rp (i ∨ j)))
+      where
+      lp = cong (fst f) (IsoSucSphereSusp∙ n) ∙ snd f
+      rp = cong (fst g) (IsoSucSphereSusp∙ m) ∙ snd g
+
+      help : (n : ℕ) (a : _)
+        → Square (cong (inv (IsoSucSphereSusp n)) (σ (S₊∙ n) a)) (σS a)
+                  (IsoSucSphereSusp∙ n) (IsoSucSphereSusp∙ n)
+      help zero a = cong-∙ SuspBool→S¹ (merid a) (sym (merid (pt (S₊∙ zero))))
+                  ∙ sym (rUnit _)
+      help (suc n) a = refl
+
+      ∙∙Distr∙ : ∀ {ℓ} {A : Type ℓ} {x y z w u : A}
+                 {p : x ≡ y} {q : y ≡ z} {r : z ≡ w} {s : w ≡ u}
+               → p ∙∙ q ∙ r ∙∙ s ≡ ((p ∙ q) ∙ r ∙ s)
+      ∙∙Distr∙ = doubleCompPath≡compPath _ _ _
+               ∙ assoc _ _ _
+               ∙ cong₂ _∙_ (assoc _ _ _) refl
+               ∙ sym (assoc _ _ _)
+
+
+      pushcase : (a : S₊ n) (b : S₊ m)
+        → Square (cong (∨fun f g .fst ∘ joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}) (push a b))
+                  (cong (fst [ f ∣ g ]-pre) (push a b))
+                  rp lp
+      pushcase a b =
+        (cong-∙∙ (∨fun f g .fst) _ _ _
+        ∙ (λ i → cong (fst g) (PathP→compPathR∙∙ (help _ b) i)
+              ∙∙ symDistr lp (sym rp) i
+              ∙∙ cong (fst f) (PathP→compPathR∙∙ (help _ a) i))
+        ∙ (λ i → cong (fst g)
+                      (IsoSucSphereSusp∙ m
+                     ∙∙ σS b
+                     ∙∙ (λ j → IsoSucSphereSusp∙ m (~ j ∨ i)))
+              ∙∙ compPath-filler' (cong (fst g) (IsoSucSphereSusp∙ m)) (snd g) (~ i)
+               ∙ sym (compPath-filler' (cong (fst f) (IsoSucSphereSusp∙ n)) (snd f) (~ i))
+              ∙∙ cong (fst f)
+                      ((λ j → IsoSucSphereSusp∙ n (i ∨ j))
+                      ∙∙ σS a
+                      ∙∙ sym (IsoSucSphereSusp∙ n))))
+       ◁ compPathR→PathP∙∙
+           ( ∙∙Distr∙
+          ∙ cong₂ _∙_ (cong₂ _∙_ (cong (cong (fst g)) (sym (compPath≡compPath' _ _)))
+                                 refl)
+                      refl
+          ∙ cong₂ _∙_ (cong (_∙ snd g) (cong-∙ (fst g) (IsoSucSphereSusp∙ m) (σS b))
+                                     ∙ sym (assoc _ _ _))
+                      (cong (sym (snd f) ∙_)
+                        (cong-∙ (fst f) (σS a)
+                          (sym (IsoSucSphereSusp∙ n)))
+                         ∙ assoc _ _ _)
+          ∙ sym ∙∙Distr∙
+          ∙ cong₃ _∙∙_∙∙_ refl (cong₂ _∙_ refl (compPath≡compPath' _ _)) refl
+         ∙ λ i → compPath-filler (cong (fst g) (IsoSucSphereSusp∙ m)) (snd g) i
+               ∙∙ ((λ j → snd g (~ j ∧ i)) ∙∙ cong (fst g) (σS b) ∙∙ snd g)
+                ∙ (sym (snd f) ∙∙ cong (fst f) (σS a) ∙∙ λ j → snd f (j ∧ i))
+               ∙∙ sym (compPath-filler (cong (fst f) (IsoSucSphereSusp∙ n)) (snd f) i))
 
 -- Homotopy group version
 [_∣_]π' : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}

Cubical/Papers/Pi4S3-JournalVersion.agda

@@ -243,7 +243,7 @@ open James₁ using (IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅)
 
 -- Definition 4.8: W + whitehead product
 W = joinTo⋁
-open Whitehead using ([_∣_]₂)
+open Whitehead using ([_∣_])
 
 -- Theorem 4.9 is omitted as it is used implicitly in the proof of the main result
 

Cubical/Papers/Pi4S3.agda

@@ -217,7 +217,7 @@ open SMult using (IsoSphereJoin)
 
 -- Definition 6: W + whitehead product
 W = joinTo⋁
-open Whitehead using ([_∣_]₂)
+open Whitehead using ([_∣_])
 
 -- Theorem 3 is omitted as it is used implicitly in the proof of the main result