Devalapurkar & Haine

Cubical/Foundations/Pointed/Properties.agda

@@ -245,6 +245,14 @@ compPathlEquiv∙ : {A : Type ℓ} {a b c : A} {q : b ≡ c} (p : a ≡ b)
 fst (compPathlEquiv∙ p) = compPathlEquiv p
 snd (compPathlEquiv∙ p) = refl
 
+-- Pointed version of Σ-cong-equiv-snd
+Σ-cong-equiv-snd∙ : ∀ {ℓ ℓ'} {A : Type ℓ} {B₁ B₂ : A → Type ℓ'}
+  → {a : A} {b₁ : B₁ a} {b₂ : B₂ a}
+  → (e : ∀ a → B₁ a ≃ B₂ a)
+  → fst (e a) b₁ ≡ b₂
+  → Path (Pointed _) (Σ A B₁ , a , b₁) (Σ A B₂ , a , b₂)
+Σ-cong-equiv-snd∙ e p = ua∙ (Σ-cong-equiv-snd e) (ΣPathP (refl , p))
+
 -- a pointed map is constant iff its non-pointed part is constant
 constantPointed≡ : {A B : Pointed ℓ} (f : A →∙ B)
                  → fst f ≡ fst (const∙ A B) → f ≡ const∙ A B

Cubical/HITs/James/Stable.agda

@@ -0,0 +1,87 @@
+{-# OPTIONS --safe #-}
+
+{-
+  The stable version of the James splitting:
+    ΣΩΣX ≃ ΣX ⋁ Σ(X ⋀ ΩΣX)
+-}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.Unit
+
+open import Cubical.HITs.Susp
+open import Cubical.HITs.Susp.SuspProduct
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Pushout.Flattening
+open import Cubical.HITs.Wedge
+open import Cubical.HITs.SmashProduct
+
+open import Cubical.Homotopy.Loopspace
+
+module Cubical.HITs.James.Stable {ℓ} (X∙@(X , x₀) : Pointed ℓ) where
+
+module ContrPushout where
+  Code : Pushout (terminal X) (terminal X) → Type ℓ
+  Code x = inl _ ≡ x
+
+  ΩΣX = Code (inl _)
+  ΩΣX∙ : Pointed _
+  ΩΣX∙ = ΩΣX , refl
+
+  α : X × ΩΣX → ΩΣX
+  α (x , p) = (p ∙ push x) ∙ sym (push x₀)
+
+  open FlatteningLemma
+    (terminal X) (terminal X)
+    (Code ∘ inl) (Code ∘ inr)
+    (pathToEquiv ∘ cong (inl tt ≡_) ∘ push)
+
+  pushoutEq : Pushout Σf Σg ≃ Pushout snd α
+  pushoutEq = pushoutEquiv _ _ _ _
+    (idEquiv (X × ΩΣX)) (ΣUnit _)
+    (ΣUnit _ ∙ₑ compPathrEquiv (sym (push x₀)))
+    refl (funExt λ (x , p)
+      → cong (_∙ sym (push x₀)) (substInPathsL (push x) p))
+
+  Code≡E : ∀ x → Code x ≡ E x
+  Code≡E (inl _) = refl
+  Code≡E (inr _) = refl
+  Code≡E (push a i) j = uaη (cong Code (push a)) (~ j) i
+
+  isContrΣE : isContr (Σ _ E)
+  isContrΣE = subst isContr (Σ-cong-snd Code≡E) (isContrSingl (inl tt))
+
+  isContrPushout : isContr (Pushout snd α)
+  isContrPushout = isOfHLevelRespectEquiv _ (flatten ∙ₑ pushoutEq) isContrΣE
+
+open ContrPushout
+
+LoopSuspSquare : commSquare
+LoopSuspSquare = record
+  { sp = record { f1 = snd ; f3 = α }
+  ; P = Unit* {ℓ}
+  ; comm = refl }
+
+LoopSuspPushoutSquare : PushoutSquare
+LoopSuspPushoutSquare = (LoopSuspSquare , isContr→≃Unit* isContrPushout .snd)
+
+open PushoutPasteLeft LoopSuspPushoutSquare
+  (λ _ → lift {j = ℓ} tt) _ _ (funExt merid)
+
+cofib-snd-James : cofib (λ (r : X × ΩΣX) → snd r) ≃ Susp ΩΣX
+cofib-snd-James = pushoutSwitchEquiv
+  ∙ₑ pushoutEquiv snd _ snd _
+    (idEquiv _) (idEquiv _) Unit≃Unit* refl refl
+  ∙ₑ (_ , isPushoutRightSquare→isPushoutTotSquare
+    (SuspPushoutSquare _ _ ΩΣX))
+
+StableJames : Susp ΩΣX ≃ Susp∙ X ⋁ Susp∙ (X∙ ⋀ ΩΣX∙)
+StableJames = invEquiv cofib-snd-James ∙ₑ cofib-snd X∙ (ΩΣX , refl)

Cubical/HITs/Join/Properties.agda

@@ -36,6 +36,15 @@ private
   variable
     ℓ ℓ' : Level
 
+-- the inclusion maps are null-homotopic
+join-inl-null : {X : Pointed ℓ} {Y : Pointed ℓ'} (x : typ X)
+  → Path (join (typ X) (typ Y)) (inl x) (inl (pt X))
+join-inl-null {X = X} {Y} x = push x (pt Y) ∙ sym (push (pt X) (pt Y))
+
+join-inr-null : {X : Pointed ℓ} {Y : Type ℓ'} (y : Y)
+  → Path (join (typ X) Y) (inr y) (inl (pt X))
+join-inr-null {X = X} y = sym (push (pt X) y)
+
 open Iso
 
 -- Characterisation of function type join A B → C

Cubical/HITs/Pushout/Properties.agda

@@ -75,6 +75,28 @@ pushoutSwitchEquiv = isoToEquiv (iso f inv leftInv rightInv)
         leftInv = λ {(inl x) → refl; (inr x) → refl; (push a i) → refl}
         rightInv = λ {(inl x) → refl; (inr x) → refl; (push a i) → refl}
 
+
+{-
+  Direct proof that pushout along the identity gives an equivalence.
+-}
+pushoutIdfunEquiv : ∀ {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'} (f : X → Y)
+  → Y ≃ Pushout f (idfun X)
+pushoutIdfunEquiv f = isoToEquiv (iso inl inv leftInv λ _ → refl)
+  where
+    inv : Pushout f (idfun _) → _
+    inv (inl y) = y
+    inv (inr x) = f x
+    inv (push x i) = f x
+
+    leftInv : section inl inv
+    leftInv (inl y) = refl
+    leftInv (inr x) = push x
+    leftInv (push a i) j = push a (i ∧ j)
+
+pushoutIdfunEquiv' : ∀ {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'} (f : X → Y)
+  → Y ≃ Pushout (idfun X) f
+pushoutIdfunEquiv' f = compEquiv (pushoutIdfunEquiv _) pushoutSwitchEquiv
+
 {-
   Definition of pushout diagrams
 -}
@@ -809,6 +831,44 @@ module _ {ℓ₀ ℓ₂ ℓ₄ ℓP : Level} where
   PushoutSquare : Type (ℓ-suc ℓ*)
   PushoutSquare = Σ commSquare isPushoutSquare
 
+module _ {ℓ₀ ℓ₂ ℓ₄ ℓP ℓP' : Level}
+  {P' : Type ℓP'} where
+  open commSquare
+  extendCommSquare : (sk : commSquare {ℓ₀} {ℓ₂} {ℓ₄} {ℓP})
+    → (sk .P → P') → commSquare
+  extendCommSquare sk f = record
+    { sp = sk .sp
+    ; P = P'
+    ; inlP = f ∘ sk .inlP
+    ; inrP = f ∘ sk .inrP
+    ; comm = cong (f ∘_) (sk .comm)
+    }
+
+  extendPushoutSquare : (sk : PushoutSquare {ℓ₀} {ℓ₂} {ℓ₄} {ℓP})
+    → (e : sk .fst .P ≃ P') → PushoutSquare
+  extendPushoutSquare sk e = (extendCommSquare (sk .fst) (e .fst) ,
+    subst isEquiv H (compEquiv (_ , sk .snd) e .snd))
+    where
+      H : e .fst ∘ _ ≡ _
+      H = funExt λ
+        { (inl x) → refl
+        ; (inr x) → refl
+        ; (push a i) → refl }
+
+-- Pushout itself fits into a pushout square
+pushoutToSquare : 3-span {ℓ} {ℓ'} {ℓ''} → PushoutSquare
+pushoutToSquare sp = record {
+    sp = sp ;
+    P = spanPushout sp ;
+    inlP = inl ;
+    inrP = inr ;
+    comm = funExt push
+  } , subst isEquiv (λ {
+    _ (inl x) → inl x ;
+    _ (inr x) → inr x ;
+    _ (push a j) → push a j
+  }) (idIsEquiv _)
+
 -- Rotations of commutative squares and pushout squares
 module _ {ℓ₀ ℓ₂ ℓ₄ ℓP : Level} where
   open commSquare

Cubical/HITs/SmashProduct/Base.agda

@@ -67,13 +67,8 @@ commK (gluer b x) = refl
 
 --- Alternative definition
 
-i∧ : {A : Pointed ℓ} {B : Pointed ℓ'} → A ⋁ B → (typ A) × (typ B)
-i∧ {A = A , ptA} {B = B , ptB} (inl x) = x , ptB
-i∧ {A = A , ptA} {B = B , ptB} (inr x) = ptA , x
-i∧ {A = A , ptA} {B = B , ptB} (push tt i) = ptA , ptB
-
 _⋀_ : Pointed ℓ → Pointed ℓ' → Type (ℓ-max ℓ ℓ')
-A ⋀ B = Pushout {A = (A ⋁ B)} (λ _ → tt) i∧
+A ⋀ B = Pushout {A = (A ⋁ B)} (λ _ → tt) ⋁↪
 
 _⋀∙_ : Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
 A ⋀∙ B = (A ⋀ B) , (inl tt)

Cubical/HITs/Susp/Properties.agda

@@ -10,12 +10,15 @@ open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Pointed.Homogeneous
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Univalence
 
 open import Cubical.Data.Bool
 open import Cubical.Data.Sigma
+open import Cubical.Data.Unit
 
 open import Cubical.HITs.Join
 open import Cubical.HITs.Susp.Base
+open import Cubical.HITs.Pushout
 open import Cubical.Homotopy.Loopspace
 
 private
@@ -73,6 +76,42 @@ Susp≃joinBool = isoToEquiv Susp-iso-joinBool
 Susp≡joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≡ join A Bool
 Susp≡joinBool = isoToPath Susp-iso-joinBool
 
+-- Here Unit* types are more convenient for general A
+SuspSquare : ∀ {ℓ} ℓ' ℓ'' (A : Type ℓ) → commSquare
+SuspSquare ℓ' ℓ'' A = record
+  { sp = record { A2 = A ; A0 = Unit* {ℓ'} ; A4 = Unit* {ℓ''} }
+  ; P = Susp A
+  ; inlP = λ _ → north
+  ; inrP = λ _ → south
+  ; comm = funExt merid
+  }
+
+SuspPushoutSquare : ∀ {ℓ} ℓ' ℓ'' (A : Type ℓ)
+  → isPushoutSquare (SuspSquare ℓ' ℓ'' A)
+SuspPushoutSquare ℓ' ℓ'' A = isoToIsEquiv (iso _ inverse rInv lInv)
+  where
+    inverse : _
+    inverse north = inl _
+    inverse south = inr _
+    inverse (merid a i) = push a i
+
+    rInv : _
+    rInv north = refl
+    rInv south = refl
+    rInv (merid a i) = refl
+
+    lInv : _
+    lInv (inl x) = refl
+    lInv (inr x) = refl
+    lInv (push a i) = refl
+
+Susp≃PushoutSusp* : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} → Susp A ≃ Pushout _ _
+Susp≃PushoutSusp* {ℓ} {ℓ'} {ℓ''} {A} = invEquiv (_ , SuspPushoutSquare ℓ' ℓ'' A)
+
+Susp≡PushoutSusp* : ∀ {ℓ ℓ' ℓ''} {A : Type _} → Susp A ≡ Pushout _ _
+Susp≡PushoutSusp* {ℓ} {ℓ'} {ℓ''} = ua
+  (Susp≃PushoutSusp* {ℓ-max ℓ (ℓ-max ℓ' ℓ'')} {ℓ'} {ℓ''})
+
 congSuspIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Iso A B → Iso (Susp A) (Susp B)
 fun (congSuspIso is) = suspFun (fun is)
 inv (congSuspIso is) = suspFun (inv is)