wip

Cubical/Data/Nat/Base.agda

@@ -34,6 +34,11 @@ iter : ∀ {ℓ} {A : Type ℓ} → ℕ → (A → A) → A → A
 iter zero f z    = z
 iter (suc n) f z = f (iter n f z)
 
+iterswap : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (f : A → A) (z : A)
+  → iter n f (f z) ≡ f (iter n f z)
+iterswap zero f z _ = f z
+iterswap (suc n) f z i = f (iterswap n f z i)
+
 elim : ∀ {ℓ} {A : ℕ → Type ℓ}
   → A zero
   → ((n : ℕ) → A n → A (suc n))

Cubical/HITs/Join/CoHSpace.agda

@@ -44,7 +44,6 @@ open Iso
 ℓ* A B a b = push (pt A) (pt B)
            ∙ (push a (pt B) ⁻¹ ∙∙ push a b ∙∙ (push (pt A) b ⁻¹))
 
-
 ℓ*IdL : (A : Pointed ℓ) (B : Pointed ℓ')
   → (b : fst B) → ℓ* A B (pt A) b ≡ refl
 ℓ*IdL A B b =
@@ -81,6 +80,12 @@ fst (-* {C = C} f) (inr x) = pt C
 fst (-* {A = A} {B} f) (push a b i) = Ω→ f .fst (ℓ* A B a b) (~ i)
 snd (-* f) = refl
 
+-- Iterated inversion
+-*^ : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+      (n : ℕ) (f : join∙ A B →∙ C)
+     → join∙ A B →∙ C
+-*^ n = iter n -*
+
 -- Neutral element
 0* : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
   → join∙ A B →∙ C
@@ -331,3 +336,15 @@ module _ {ℓ ℓ' ℓ'' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Poin
     where
     help : (-* (-* f)) +* (-* f) ≡ f +* (-* f)
     help = +*InvL (-* f) ∙ sym (+*InvR f)
+
+join-commFun-ℓ* : (A : Pointed ℓ) (B : Pointed ℓ') (a : fst A) (b : fst B)
+  → cong join-commFun (ℓ* A B a b)
+   ≡ (sym (push (pt B) (pt A)) ∙∙ sym (ℓ* B A b a) ∙∙ push (pt B) (pt A))
+join-commFun-ℓ* A B a b =
+    cong-∙ join-commFun (push (pt A) (pt B)) _
+  ∙ cong₂ _∙_ refl (cong-∙∙ join-commFun _ _ _)
+  ∙ sym (doubleCompPath≡compPath _ _ _
+      ∙ cong₂ _∙_ refl
+         (cong₂ _∙_ (symDistr _ _) refl
+        ∙ sym (assoc _ _ _) ∙ cong₂ _∙_ refl (lCancel _)
+        ∙ sym (rUnit _)))

Cubical/HITs/Join/Properties.agda

@@ -707,3 +707,15 @@ module _ {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
   inv GaneaIso = join→GaneaFib
   rightInv GaneaIso = join→GaneaFib→join
   leftInv GaneaIso = GaneaFib→join→GaneaFib
+
+-- Pinch map
+joinPinch : ∀ {ℓ''} {A : Type ℓ} {B : Type ℓ'} (C : Pointed ℓ'')
+  → ((a : A) (b : B) → Ω C .fst) → join A B → fst C
+joinPinch C p (inl x) = pt C
+joinPinch C p (inr x) = pt C
+joinPinch C p (push a b i) = p a b i
+
+joinPinch∙ : ∀ {ℓ''} (A : Pointed ℓ) (B : Pointed ℓ') (C : Pointed ℓ'')
+  → ((a : typ A) (b : typ B) → Ω C .fst) → join∙ A B →∙ C
+proj₁ (joinPinch∙ A B C p) = joinPinch C p
+snd (joinPinch∙ A B C p) = refl

Cubical/HITs/Sn/Multiplication.agda

@@ -480,8 +480,7 @@ assoc⌣S {n = suc (suc n)} {m = m} {l} (merid a i) y z j =
 
 -- To state it: we'll need iterated negations
 -S^ : {k : ℕ} (n : ℕ) → S₊ k → S₊ k
--S^ zero x = x
--S^ (suc n) x = invSphere (-S^ n x)
+-S^ n = iter n invSphere
 
 -- The folowing is an explicit definition of -S^ (n · m) which is
 -- often easier to reason about
@@ -544,8 +543,11 @@ private
 
 -- Iterated path inversion
 sym^ : ∀ {ℓ} {A : Type ℓ} {x : A} (n : ℕ) → x ≡ x → x ≡ x
-sym^ zero p = p
-sym^ (suc n) p = sym (sym^ n p)
+sym^ n = iter n sym
+
+sym^-refl : ∀ {ℓ} {A : Type ℓ} {x : A} (n : ℕ) → sym^ {x = x} n refl ≡ refl
+sym^-refl zero = refl
+sym^-refl (suc n) = cong sym (sym^-refl n)
 
 -- Interaction between -S^ and sym^
 σS-S^ : {k : ℕ} (n : ℕ) (x : S₊ (suc k))

Cubical/HITs/Susp/Properties.agda

@@ -577,6 +577,13 @@ Susp·→Ωcomm A {B = B} f g = isoInvInjective ΩSuspAdjointIso _ _
                 ∙ sym (·Suspσ g f x)
                 ∙ rUnit _)
 
+Susp·→Ωcomm' : ∀ {ℓ ℓ'} (A A' : Pointed ℓ)
+  → A ≃∙ Susp∙ (typ A') → {B : Pointed ℓ'}
+  (f g : A →∙ Ω B) → ·→Ω f g ≡ ·→Ω g f
+Susp·→Ωcomm' A A' e {B = B} =
+  Equiv∙J (λ A _ → (f g : A →∙ Ω B) → ·→Ω f g ≡ ·→Ω g f)
+    (Susp·→Ωcomm A') e
+
 ·SuspComm : ∀ {ℓ ℓ'} (A : Pointed ℓ) {B : Pointed ℓ'}
   (f g : Susp∙ (Susp (typ A)) →∙ B)
   → ·Susp (Susp∙ (typ A)) f g ≡ ·Susp (Susp∙ (typ A)) g f

Cubical/Homotopy/Group/Join.agda

@@ -14,9 +14,14 @@ open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
 
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
 open import Cubical.Data.Bool
 
 open import Cubical.HITs.SetTruncation as ST
@@ -164,6 +169,9 @@ snd (·Π≡+* {A = A} f g i) j = lem i j
 -π* : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} (f : π* n m A) → π* n m A
 -π* = ST.map -*
 
+-π*^ : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} (k : ℕ) (f : π* n m A) → π* n m A
+-π*^ n = iter n -π*
+
 1π* : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} → π* n m A
 1π* = ∣ const∙ _ _ ∣₂
 
@@ -308,3 +316,81 @@ snd (π*∘∙Hom {A = A} {B = B} n m f) =
   → GroupEquiv (π*Gr n m A) (π*Gr n m B)
 fst (π*∘∙Equiv n m f) = isoToEquiv (setTruncIso (pre∘∙equiv f))
 snd (π*∘∙Equiv n m f) = π*∘∙Hom n m (≃∙map f) .snd
+
+-- Swapping indices
+π*SwapIso : ∀ {ℓ} (n m : ℕ) (A : Pointed ℓ)
+  → Iso (π* n m A) (π* m n A)
+π*SwapIso n m A =
+  setTruncIso (post∘∙equiv
+    (isoToEquiv join-comm , push (ptSn m) (ptSn n) ⁻¹))
+
+
+-- This is a group iso whenever n + m > 0
+π*GrSwapIso : ∀ {ℓ} (n m : ℕ) (A : Pointed ℓ)
+  → (n + m > 0)
+  → GroupIso (π*Gr n m A) (π*Gr m n A)
+fst (π*GrSwapIso n m A pos) = π*SwapIso n m A
+snd (π*GrSwapIso n m A pos) =
+  makeIsGroupHom (elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
+    λ f g → cong ∣_∣₂ (ΣPathP ((funExt
+      (λ { (inl x) → refl
+         ; (inr x) → refl
+        ; (push a b i) j → main f g b a j i}))
+          , (sym (rUnit _)
+           ∙ cong (cong (fst (f +* g)))
+             (cong₂ _∙_ refl (∙∙lCancel _) ∙ sym (rUnit _)))
+           ∙ cong sym
+             (cong₂ _∙_
+               (cong (Ω→ f .fst) (ℓ*IdL (S₊∙ n) (S₊∙ m) (ptSn m)) ∙ Ω→ f .snd)
+               ((cong (Ω→ g .fst) (ℓ*IdL (S₊∙ n) (S₊∙ m) (ptSn m)) ∙ Ω→ g .snd))
+               ∙ rCancel _))))
+  where
+  com : (n m : ℕ) → (n + m > 0)
+     → (f g : join∙ (S₊∙ n) (S₊∙ m) →∙ A) (a : _) (b : _)
+    → (Ω→ f .fst (ℓ* (S₊∙ n) (S₊∙ m) a b)
+      ∙ Ω→ g .fst (ℓ* (S₊∙ n) (S₊∙ m) a b))
+    ≡ (Ω→ g .fst (ℓ* (S₊∙ n) (S₊∙ m) a b)
+      ∙ Ω→ f .fst (ℓ* (S₊∙ n) (S₊∙ m) a b))
+  com zero zero p f g a b = ⊥.rec (snotz (+-comm 1 (fst p) ∙ snd p))
+  com zero (suc m) p f g a b i =
+    Susp·→Ωcomm' (S₊∙ (suc m)) (S₊∙ m)
+                  (isoToEquiv (IsoSucSphereSusp _) , IsoSucSphereSusp∙' m)
+      (F f) (F g) i .fst b
+    where
+    F : (f : join∙ (S₊∙ zero) (S₊∙ (suc m)) →∙ A) → Σ _ _
+    F f = (λ b → Ω→ f .fst (ℓ* (S₊∙ zero) (S₊∙ (suc m)) a b))
+      , cong (fst (Ω→ f)) (ℓ*IdR (S₊∙ zero) (S₊∙ (suc m)) a) ∙ Ω→ f .snd
+  com (suc n) m p f g a b i =
+    Susp·→Ωcomm' (S₊∙ (suc n)) (S₊∙ n)
+                  ((isoToEquiv (IsoSucSphereSusp _) , IsoSucSphereSusp∙' n))
+      (F f) (F g) i .fst a
+    where
+    F : (f : join∙ (S₊∙ (suc n)) (S₊∙ m) →∙ A) → Σ _ _
+    F f = (λ a → Ω→ f .fst (ℓ* (S₊∙ (suc n)) (S₊∙ m) a b))
+      , cong (fst (Ω→ f)) (ℓ*IdL (S₊∙ (suc n)) (S₊∙ m) b) ∙ Ω→ f .snd
+
+  main : (f g : join∙ (S₊∙ n) (S₊∙ m) →∙ A) (a : _) (b : _)
+    → (Ω→ f .fst (ℓ* (S₊∙ n) (S₊∙ m) a b)
+     ∙ Ω→ g .fst (ℓ* (S₊∙ n) (S₊∙ m) a b)) ⁻¹
+     ≡ Ω→ (f ∘∙ (join-commFun , _)) .fst (ℓ* (S₊∙ m) (S₊∙ n) b a)
+    ∙  Ω→ (g ∘∙ (join-commFun , _)) .fst (ℓ* (S₊∙ m) (S₊∙ n) b a)
+  main f g a b =
+   cong sym (com n m pos f g a b)
+    ∙ symDistr _ _
+    ∙ sym (cong₂ _∙_ (main-path f) (main-path g))
+    where
+    h : invEquiv∙ ((isoToEquiv join-comm , push (ptSn m) (ptSn n) ⁻¹)) .snd
+      ≡ push (ptSn n) (ptSn m) ⁻¹
+    h = cong₂ _∙_ refl (∙∙lCancel _) ∙ sym (rUnit _)
+
+    main-path : (f : join∙ (S₊∙ n) (S₊∙ m) →∙ A) → _
+    main-path  f =
+       (λ i → fst (Ω→∘∙ f (join-commFun , h i) i) ((ℓ* (S₊∙ m) (S₊∙ n) b a)))
+      ∙ cong (Ω→ f .fst)
+             (sym (PathP→compPathR∙∙
+               (symP (compPathR→PathP∙∙ (join-commFun-ℓ* _ _ _ _)))))
+
+-π*^≡ : ∀ {ℓ} {n m : ℕ} {A : Pointed ℓ} (k : ℕ)
+  (f : join∙ (S₊∙ n) (S₊∙ m) →∙ A) → -π*^ k ∣ f ∣₂ ≡ ∣ -*^ k f ∣₂
+-π*^≡ zero f = refl
+-π*^≡ (suc k) f = cong -π* (-π*^≡ k f)

Cubical/Homotopy/WhiteheadProducts/Base.agda

@@ -4,8 +4,16 @@ module Cubical.Homotopy.WhiteheadProducts.Base where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
+open import Cubical.Foundations.GroupoidLaws
 
 open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
+open import Cubical.Data.Bool
+open import Cubical.Data.Int using (ℤ ; pos)
 
 open import Cubical.HITs.Susp renaming (toSusp to σ)
 open import Cubical.HITs.Pushout
@@ -14,9 +22,14 @@ open import Cubical.HITs.Sn.Multiplication
 open import Cubical.HITs.Join
 open import Cubical.HITs.Wedge
 open import Cubical.HITs.SetTruncation
+open import Cubical.HITs.PropositionalTruncation as PT hiding (elim2)
+open import Cubical.HITs.Truncation as TR hiding (elim2)
+open import Cubical.HITs.S1
 
 open import Cubical.Homotopy.Group.Base
 open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Join
+open import Cubical.Homotopy.Connected
 
 open Iso
 
@@ -25,25 +38,75 @@ open Iso
        → (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
+[_∣_]-pre {X = X} {n = n} {m = m} f g =
+  joinPinch∙ (S₊∙ n) (S₊∙ m) X
+    (λ a b → (Ω→ g .fst (σS b) ∙ Ω→ f .fst (σS a)))
 
+open import Cubical.Homotopy.WhiteheadProducts.Generalised.Base
 [_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
        → (S₊∙ (suc n) →∙ X)
        → (S₊∙ (suc m) →∙ X)
        → S₊∙ (suc (n + m)) →∙ X
 [_∣_] {n = n} {m = m} f g =
   [ f ∣ g ]-pre ∘∙ (sphere→Join n m , IsoSphereJoin⁻Pres∙ n m)
 
--- Homotopy group version
+-- Homotopy group versions
 [_∣_]π' : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
        → π' (suc n) X → π' (suc m) X
        → π' (suc (n + m)) X
 [_∣_]π' = elim2 (λ _ _ → squash₂) λ f g → ∣ [ f ∣ g ] ∣₂
 
+-- Join version
+[_∣_]π* : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → π' (suc n) X → π' (suc m) X
+       → π* n m X
+[_∣_]π* = elim2 (λ _ _ → squash₂) λ f g → ∣ [ f ∣ g ]-pre ∣₂
+
+-- The two versions agree
+whπ*≡whπ' : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (f : π' (suc n) X) (g : π' (suc m) X)
+       → [ f ∣ g ]π' ≡ Iso.fun (Iso-π*-π' n m ) [ f ∣ g ]π*
+whπ*≡whπ' {n = n} {m} = elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
+  λ f g → TR.rec (squash₂ _ _)
+          (λ p → cong ∣_∣₂ (ΣPathP (refl , (sym (rUnit _)
+                ∙ cong (cong (fst [ f ∣ g ]-pre)) p
+                ∙ rUnit _))))
+          (help n m)
+  where
+  help : (n m : ℕ)
+    → hLevelTrunc 1 (IsoSphereJoin⁻Pres∙ n m
+                   ≡ snd (≃∙map (invEquiv∙ (joinSphereEquiv∙ n m))))
+  help zero zero = ∣ invEq (congEquiv F) (λ _ → pos 0) ∣ₕ
+    where
+    F : (Path (join (S₊ 0) (S₊ 0)) (inr true) (inl true)) ≃ ℤ
+    F = compEquiv ( (compPathlEquiv (push true true)))
+                (compEquiv ((Ω≃∙ (isoToEquiv (IsoSphereJoin 0 0) , refl) .fst))
+                (isoToEquiv ΩS¹Isoℤ))
+  help zero (suc m) =
+    isConnectedPath 1
+      (isConnectedPath 2
+        (isOfHLevelRetractFromIso 0
+          (mapCompIso (IsoSphereJoin zero (suc m)))
+            (isConnectedSubtr 3 m
+              (subst (λ p → isConnected p (S₊ (2 + m)))
+                (+-comm 3 m)
+                (sphereConnected (2 + m))))) _ _) _ _ .fst
+  help (suc n) m =
+    isConnectedPath 1
+      (isConnectedPath 2
+        (isOfHLevelRetractFromIso 0
+          (mapCompIso (IsoSphereJoin (suc n) m))
+            (isConnectedSubtr 3 (n + m)
+              (subst (λ p → isConnected p (S₊ (2 + (n + m))))
+                (+-comm 3 (n + m)) (sphereConnected (2 + (n + m)))))) _ _) _ _ .fst
+
+whπ'≡whπ* : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
+       → (f : π' (suc n) X) (g : π' (suc m) X)
+       → Iso.inv (Iso-π*-π' n m) [ f ∣ g ]π' ≡ [ f ∣ g ]π*
+whπ'≡whπ* {n = n} {m} f g =
+  cong (inv (Iso-π*-π' n m)) (whπ*≡whπ' f g)
+  ∙ Iso.leftInv (Iso-π*-π' n m) _
+
 -- Whitehead product (as a composition)
 joinTo⋁ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
  → join (typ A) (typ B)

Cubical/Homotopy/WhiteheadProducts/Generalised/Base.agda

@@ -28,10 +28,8 @@ module _ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
          (f : Susp∙ (typ A) →∙ C) (g : Susp∙ (typ B) →∙ C) where
 
   ·wh : join∙ A B →∙ C
-  fst ·wh (inl x) = pt C
-  fst ·wh (inr x) = pt C
-  fst ·wh (push a b i) = (Ω→ g .fst (σ B b) ∙ Ω→ f .fst (σ A a)) i
-  snd ·wh = refl
+  ·wh = joinPinch∙ A B C
+         (λ a b → (Ω→ g .fst (σ B b) ∙ Ω→ f .fst (σ A a)))
 
   -- alternative version using Suspension and smash
   private
@@ -60,7 +58,7 @@ module _ {ℓ ℓ' ℓ''} (A : Pointed ℓ)
   fst ·whΣ = fst ·whΣ' ∘ suspFun ⋀→Smash
   snd ·whΣ = refl
 
-  -- The two versions agree modulo the equivalnce Σ(A ⋀ B) ≃ A * B
+  -- The two versions agree modulo the equivalence Σ(A ⋀ B) ≃ A * B
   ·wh≡·whΣ : ·wh ∘∙ (SuspSmash→Join∙ A B) ≡ ·whΣ
   ·wh≡·whΣ = ΣPathP (funExt lem , (sym (rUnit _)
     ∙ cong sym (cong₂ _∙_