diff --git a/Cubical/Foundations/Pointed/Properties.agda b/Cubical/Foundations/Pointed/Properties.agda index ae24e72bf9..65bc99668c 100644 --- a/Cubical/Foundations/Pointed/Properties.agda +++ b/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 diff --git a/Cubical/HITs/James/Stable.agda b/Cubical/HITs/James/Stable.agda new file mode 100644 index 0000000000..48e6af5b73 --- /dev/null +++ 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) diff --git a/Cubical/HITs/Join/Properties.agda b/Cubical/HITs/Join/Properties.agda index ae82d7800d..c2a9c1bcb3 100644 --- a/Cubical/HITs/Join/Properties.agda +++ b/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 diff --git a/Cubical/HITs/Pushout/Properties.agda b/Cubical/HITs/Pushout/Properties.agda index e8fa8c5cd4..98cecb20ea 100644 --- a/Cubical/HITs/Pushout/Properties.agda +++ b/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 diff --git a/Cubical/HITs/SmashProduct/Base.agda b/Cubical/HITs/SmashProduct/Base.agda index 2c591a2797..0a5cfe16e4 100644 --- a/Cubical/HITs/SmashProduct/Base.agda +++ b/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) diff --git a/Cubical/HITs/Susp/Properties.agda b/Cubical/HITs/Susp/Properties.agda index 98f7c2a2ab..1cb0000ba1 100644 --- a/Cubical/HITs/Susp/Properties.agda +++ b/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) diff --git a/Cubical/HITs/Susp/SuspProduct.agda b/Cubical/HITs/Susp/SuspProduct.agda new file mode 100644 index 0000000000..6f00c0d62b --- /dev/null +++ b/Cubical/HITs/Susp/SuspProduct.agda @@ -0,0 +1,232 @@ +{-# OPTIONS --safe #-} + +{- + The suspension of a Cartesian product is given by a triple wedge sum + Σ (X × Y) = Σ X ⋁ Σ Y ⋁ Σ (X ⋀ Y) +-} + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Path +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Univalence + +open import Cubical.Data.Sigma +open import Cubical.Data.Unit + +open import Cubical.HITs.Pushout +open import Cubical.HITs.Susp +open import Cubical.HITs.SmashProduct +open import Cubical.HITs.Join +open import Cubical.HITs.Wedge + +module Cubical.HITs.Susp.SuspProduct where + +module PushoutNull {ℓ ℓ'} (X : Type ℓ) (Y : Type ℓ') (y₀ : Y) where + + {- The pushout of a null map is equivalent to a wedge with the suspension + X --> 1 --> Y + ↓ ↓ ↓ + 1 -> Σ X -> ? = B + -} + + module _ where + open PushoutPasteLeft + (rotatePushoutSquare (_ , SuspPushoutSquare ℓ-zero ℓ-zero X)) + {B = (Susp X , north) ⋁ (Y , y₀)} + (λ _ → y₀) inr inl (funExt (λ _ → push _)) + + squareL : commSquare + squareL = totSquare + + pushoutSquareL : PushoutSquare + pushoutSquareL = squareL , isPushoutRightSquare→isPushoutTotSquare + (snd (⋁-PushoutSquare _ _ ℓ-zero)) + + module _ where + open PushoutPasteDown + (_ , SuspPushoutSquare ℓ-zero ℓ-zero X) + {B = (Susp X , north) ⋁ (Y , y₀)} + (λ _ → y₀) inr inl (funExt (λ _ → sym (push _))) + + squareR : commSquare + squareR = totSquare + + pushoutSquareR : PushoutSquare + pushoutSquareR = squareR , isPushoutBottomSquare→isPushoutTotSquare + (snd (rotatePushoutSquare (⋁-PushoutSquare _ _ ℓ-zero))) + +module WedgePushout {ℓ ℓ' ℓ''} (A : Pointed ℓ) (B : Pointed ℓ') (C : Pointed ℓ'') where + + open 3x3-span + span : 3x3-span + span .A40 = typ A + span .A42 = typ A + span .A44 = typ A + span .A20 = Unit + span .A22 = Unit + span .A24 = Unit + span .A00 = typ B + span .A02 = Unit + span .A04 = typ C + span .f30 _ = pt A + span .f32 _ = pt A + span .f34 _ = pt A + span .f10 _ = pt B + span .f12 _ = _ + span .f14 _ = pt C + span .f41 = idfun (typ A) + span .f21 = _ + span .f01 _ = pt B + span .f43 = idfun (typ A) + span .f23 = _ + span .f03 _ = pt C + span .H11 _ = refl + span .H13 _ = refl + span .H31 _ = refl + span .H33 _ = refl + + A□2≃ : A□2 span ≃ typ A + A□2≃ = invEquiv (pushoutIdfunEquiv' _) + + f : typ A → B ⋁ A + f = inr + + g : typ A → C ⋁ A + g = inr + + A□○≃ : A□○ span ≃ Pushout f g + A□○≃ = pushoutEquiv _ _ _ _ + A□2≃ (idEquiv _) (idEquiv _) + (funExt λ + { (inl x) → push _ + ; (inr x) → refl + ; (push a i) j → sq (~ i) (~ j) }) + (funExt λ + { (inl x) → push _ + ; (inr x) → refl + ; (push a i) j → sq (~ i) (~ j) }) + where + sq : ∀ {ℓ} {C : Type ℓ} {c : C} + → Square refl (sym (Pushout.push _)) + refl (sym (push {f = λ x → c} {g = λ _ → pt A} + tt ∙ refl)) + sq = slideSquare (sym (rUnit _)) + + A4□≃ : A4□ span ≃ typ A + A4□≃ = invEquiv (pushoutIdfunEquiv _) + + A2□≃ : A2□ span ≃ Unit + A2□≃ = invEquiv (pushoutIdfunEquiv _) + + A2□isContr : isContr (A2□ span) + A2□isContr = isOfHLevelRespectEquiv 0 (pushoutIdfunEquiv _) isContrUnit + + A○□≃ : A○□ span ≃ (B ⋁∙ₗ C) ⋁ A + A○□≃ = pushoutEquiv _ _ _ _ + A2□≃ (idEquiv _) A4□≃ + (lemma A2□isContr refl) (lemma A2□isContr refl) + where + -- functions on contractible domains are determined by the basepoint + lemma : ∀ {ℓ ℓ'} + → {A : Type ℓ} {B : Type ℓ'} + → {f g : A → B} + → (c : isContr A) + → f (c .fst) ≡ g (c .fst) + → f ≡ g + lemma {f = f} {g} c p = funExt λ x + → cong f (sym (c .snd x)) + ∙ p + ∙ cong g (c .snd x) + + wedgePushout : PushoutSquare + wedgePushout = extendPushoutSquare + (pushoutToSquare record { f1 = f ; f3 = g }) + (invEquiv A□○≃ ∙ₑ pathToEquiv (3x3-lemma span) ∙ₑ A○□≃) + + +module _ {ℓ ℓ'} (X : Pointed ℓ) (Y : Pointed ℓ') where + open commSquare + open 3-span + + {- + X × Y ---> Y --------> 1 + ↓ A ↓ C ↓ + X ---> Σ(X∧Y) --> ΣY ∨ Σ(X∧Y) + ↓ B ↓ D ↓ + 1 -> ΣX ∨ Σ(X∧Y) --> ? = ΣX ∨ ΣY ∨ Σ(X∧Y) + -} + + pushoutA₀ : PushoutSquare -- inrP maps to south, but we want north + pushoutA₀ = extendPushoutSquare + (pushoutToSquare record { f1 = fst ; f3 = snd }) + (pathToEquiv (joinPushout≡join _ _) ∙ₑ + invEquiv (isoToEquiv (SmashJoinIso {A = X} {B = Y}))) + + squareA : I → commSquare + squareA i = record + { commSquare (pushoutA₀ .fst) + ; inrP = λ _ → merid (inl _) i + ; comm = transp (λ j → + Path (typ X × typ Y → Susp (X ⋀ Y)) + (λ _ → north) (λ _ → merid (inl _) (i ∨ ~ j))) + i (pushoutA₀ .fst .commSquare.comm) + } + + pushoutA : PushoutSquare + pushoutA = squareA i0 , + subst isPushoutSquare (λ i → squareA (~ i)) (pushoutA₀ .snd) + + module _ where + open PushoutNull (typ X) (Susp (X ⋀ Y)) north + open PushoutPasteDown pushoutA + (squareL .sp .f1) + (squareL .inlP) + (squareL .inrP) + (squareL .commSquare.comm) + + pushoutB : PushoutSquare + pushoutB = pushoutSquareL + + pushoutAB : PushoutSquare + pushoutAB = _ , isPushoutBottomSquare→isPushoutTotSquare (pushoutB .snd) + + cofib-snd : cofib snd ≃ Susp∙ (typ X) ⋁ Susp∙ (X ⋀ Y) + cofib-snd = pushoutEquiv _ _ _ _ + (idEquiv _) Unit≃Unit* (idEquiv _) + refl refl + ∙ₑ (_ , pushoutAB .snd) + + pushoutC : PushoutSquare + pushoutC = PushoutNull.pushoutSquareR (typ Y) (Susp (X ⋀ Y)) north + + pushoutD : PushoutSquare + pushoutD = WedgePushout.wedgePushout + (Susp∙ (X ⋀ Y)) (Susp∙ (typ X)) (Susp∙ (typ Y)) + + pushoutCD : PushoutSquare + pushoutCD = _ , isPushoutBottomSquare→isPushoutTotSquare (pushoutD .snd) + where + open PushoutPasteDown pushoutC + (pushoutD .fst .sp .f1) + (pushoutD .fst .inlP) + (pushoutD .fst .inrP) + (pushoutD .fst .commSquare.comm) + + pushoutTot : PushoutSquare + pushoutTot = _ , isPushoutRightSquare→isPushoutTotSquare (pushoutCD .snd) + where + open PushoutPasteLeft pushoutAB + (pushoutCD .fst .sp .f3) + (pushoutCD .fst .inrP) + (pushoutCD .fst .inlP) + (pushoutCD .fst .commSquare.comm) + + SuspProduct : (Susp∙ (typ X) ⋁∙ₗ Susp∙ (typ Y)) ⋁ Susp∙ (X ⋀ Y) + ≃ Susp (typ X × typ Y) + SuspProduct = invEquiv (_ , pushoutTot .snd) + ∙ₑ (_ , SuspPushoutSquare ℓ-zero ℓ-zero (typ X × typ Y)) diff --git a/Cubical/HITs/Wedge/Base.agda b/Cubical/HITs/Wedge/Base.agda index 192c7aedcc..cec20c9b41 100644 --- a/Cubical/HITs/Wedge/Base.agda +++ b/Cubical/HITs/Wedge/Base.agda @@ -34,6 +34,14 @@ _∨→_ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointe (f ∨→ g) (inr x) = fst g x (f ∨→ g) (push a i₁) = (snd f ∙ sym (snd g)) i₁ +⋁proj₁ : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') + → A ⋁ B → typ A +⋁proj₁ A B = idfun∙ A ∨→ ((λ _ → pt A) , refl) + +⋁proj₂ : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') + → A ⋁ B → typ B +⋁proj₂ A B = ((λ _ → pt B) , refl) ∨→ idfun∙ B + -- Pointed version ∨→∙ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''} → (f : A →∙ C) (g : B →∙ C) → ((A ⋁∙ₗ B) →∙ C) diff --git a/Cubical/HITs/Wedge/Properties.agda b/Cubical/HITs/Wedge/Properties.agda index c357e94d00..60043a6a86 100644 --- a/Cubical/HITs/Wedge/Properties.agda +++ b/Cubical/HITs/Wedge/Properties.agda @@ -12,7 +12,6 @@ open import Cubical.Data.Sigma open import Cubical.Data.Unit open import Cubical.Data.Sum as ⊎ -open import Cubical.HITs.Pushout.Base open import Cubical.HITs.Wedge.Base open import Cubical.HITs.Susp open import Cubical.HITs.Pushout @@ -44,6 +43,36 @@ Iso.inv ⋁-commIso = ⋁-commFun Iso.rightInv ⋁-commIso = ⋁-commFun² Iso.leftInv ⋁-commIso = ⋁-commFun² +-- Pushout square using Unit* for convenience +⋁-PushoutSquare : ∀ (A : Pointed ℓ) (B : Pointed ℓ') ℓ'' → PushoutSquare +⋁-PushoutSquare A B ℓ'' = record + { sp = record + { A0 = typ A + ; A2 = Unit* {ℓ''} + ; A4 = typ B + ; f1 = λ _ → pt A + ; f3 = λ _ → pt B } + ; P = A ⋁ B + ; inlP = inl + ; inrP = inr + ; comm = funExt λ _ → push _ } , + isoToIsEquiv (iso _ inv lInv rInv) + where + inv : _ + inv (inl a) = inl a + inv (inr b) = inr b + inv (push _ i) = push _ i + + rInv : _ + rInv (inl a) = refl + rInv (inr b) = refl + rInv (push _ i) = refl + + lInv : _ + lInv (inl a) = refl + lInv (inr b) = refl + lInv (push _ i) = refl + -- cofibre of A --inl→ A ⋁ B is B cofibInl-⋁ : {A : Pointed ℓ} {B : Pointed ℓ'} → Iso (cofib {B = A ⋁ B} inl) (fst B) @@ -548,3 +577,75 @@ module _ {ℓA ℓB ℓC : Level} {A : Type ℓA} {B : A → Pointed ℓB} (C : ⋁-cofib-Iso = compIso (compIso (invIso A○□Iso) (invIso (3x3-Iso inst))) A□○Iso + +{- + We prove the square + X ⋁ Y --> X + ↓ ↓ + Y ----> * + is a pushout. +-} + +module _ (X∙ @ (X , x₀) : Pointed ℓ) (Y∙ @ (Y , y₀) : Pointed ℓ') where + + private + fX : X∙ ⋁ Y∙ → X + fX = ⋁proj₁ X∙ Y∙ + + fY : X∙ ⋁ Y∙ → Y + fY = ⋁proj₂ X∙ Y∙ + + weirdSquare : ∀ {ℓ ℓ' ℓ''} {X : Type ℓ} {Y : Type ℓ'} {Z : Type ℓ''} + → (f : X → Y) (g : Y → Z) → commSquare + weirdSquare f g = record + { sp = record { f1 = idfun _ ; f3 = f } + ; inlP = f + ; inrP = idfun _ + ; comm = refl ∙ refl ∙ refl } + + weirdPushoutSquare : ∀ {ℓ ℓ' ℓ''} {X : Type ℓ} {Y : Type ℓ'} {Z : Type ℓ''} + → (f : X → Y) (g : Y → Z) → isPushoutSquare (weirdSquare f g) + weirdPushoutSquare f g = isoToIsEquiv (iso _ inr (λ _ → refl) + λ { (inl x) → sym (push _) + ; (inr x) → refl + ; (push a i) j → subst + (λ t → Square (sym (push _)) refl t (push _)) + (cong (cong Pushout.inr) (lUnit _ ∙ lUnit _)) + (λ i j → push a (i ∨ ~ j)) + i j + }) + + {- + The proof proceeds by applying the pasting lemma twice: + 1 ----> Y + ↓ ↓ + X --> X ⋁ Y --> X + ↓ mid ↓ bot ↓ + 1 ----> Y ----> 1 + -} + + midPushout : isPushoutSquare _ + midPushout = isPushoutTotSquare→isPushoutBottomSquare + (weirdPushoutSquare _ (terminal Y)) + where + open PushoutPasteDown (pushoutToSquare record + { A2 = Unit + ; f1 = λ _ → x₀ + ; f3 = λ _ → y₀ + }) (terminal X) (λ _ → y₀) fY refl + + -- slight help to the unifier here + botPushout : isPushoutSquare record { comm = refl } + botPushout = isPushoutTotSquare→isPushoutBottomSquare $ + rotatePushoutSquare (record { comm = refl } , isoToIsEquiv + (iso _ inl (λ _ → refl) λ { + (inl _) i → inl _ + ; (inr a) i → push a i + ; (push a j) i → push a (i ∧ j) + })) .snd + where + open PushoutPasteDown (rotatePushoutSquare (_ , midPushout)) + fX (terminal X) (terminal Y) refl + + Pushout⋁≃Unit : Pushout fX fY ≃ Unit + Pushout⋁≃Unit = _ , botPushout diff --git a/Cubical/Homotopy/HiltonMilnor.agda b/Cubical/Homotopy/HiltonMilnor.agda new file mode 100644 index 0000000000..425a5e7977 --- /dev/null +++ b/Cubical/Homotopy/HiltonMilnor.agda @@ -0,0 +1,96 @@ +{-# OPTIONS --safe --lossy-unification #-} + +{- + The finitary Hilton–Milnor splitting + Ω(X ⋁ Y) ≃ ΩX × ΩY × ΩΣ(ΩY ⋀ ΩX) + for pointed types X and Y. +-} + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Path +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism using (isoToPath; isoToEquiv) +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Function +open import Cubical.Foundations.Univalence + +open import Cubical.Homotopy.Loopspace + +open import Cubical.Data.Sigma +open import Cubical.Data.Unit + +open import Cubical.HITs.Pushout +open import Cubical.HITs.Pushout.Flattening +open import Cubical.HITs.SmashProduct +open import Cubical.HITs.Susp +open import Cubical.HITs.Join +open import Cubical.HITs.Wedge + +module Cubical.Homotopy.HiltonMilnor {ℓ} (X∙@(X , x₀) Y∙@(Y , y₀) : Pointed ℓ) where + +fun : X∙ ⋁ Y∙ → typ X∙ × typ Y∙ +fun = ⋁↪ {A = X∙} {B = Y∙} + +-- The required section, given by concatenating the paths +sect : typ (Ω (X∙ ×∙ Y∙)) → typ (Ω (X∙ ⋁∙ₗ Y∙)) +sect p = cong (inl ∘ fst) p ∙ push _ ∙ cong (inr ∘ snd) p ∙ sym (push _) + +rInv : ∀ c → cong fun (sect c) ≡ c +rInv c = congFunct fun _ _ + ∙ cong (cong (fun ∘ inl ∘ fst) c ∙_) + (congFunct fun (push _) _ + ∙ sym (lUnit _) + ∙ lemma₂ -- can't be inlined because lossy unification + ∙ sym (rUnit _)) + ∙ lemma₁ (cong fst c) (cong snd c) + where + lemma₁ : (p : x₀ ≡ x₀) (q : y₀ ≡ y₀) + → cong (_, y₀) p ∙ cong (x₀ ,_) q ≡ cong₂ _,_ p q + lemma₁ p q = cong ΣPathP (ΣPathP + (congFunct fst (cong (_, y₀) p) _ ∙ sym (rUnit _) , + congFunct snd (cong (_, y₀) p) _ ∙ sym (lUnit _))) + + lemma₂ : cong fun + (cong (inr ∘ snd) c ∙ sym (push _)) + ≡ cong (⋁↪ ∘ inr ∘ snd) c ∙ refl + lemma₂ = congFunct fun _ _ + +-- Now the splitting lemma gives us something in terms of the fiber of ⋁↪. +-- So we try to characterize the type. +module _ where + open FlatteningLemma + (λ (_ : Unit) → x₀) (λ _ → y₀) + (λ x → (x , y₀) ≡ (x₀ , y₀)) (λ y → (x₀ , y) ≡ (x₀ , y₀)) + (λ _ → idEquiv _) + + private + E≡ : ∀ u → E u ≡ (⋁↪ u ≡ (x₀ , y₀)) + E≡ (inl x) = refl + E≡ (inr x) = refl + E≡ (push a i) j = uaIdEquiv {A = typ (Ω (X∙ ×∙ Y∙))} j i + + Pushout≃ : Pushout Σf Σg ≃ join (typ (Ω Y∙)) (typ (Ω X∙)) + Pushout≃ = pushoutEquiv _ _ _ _ + (ΣUnit _ ∙ₑ invEquiv ΣPathP≃PathPΣ ∙ₑ Σ-swap-≃) + (Σ-cong-equiv-snd (λ _ → invEquiv ΣPathP≃PathPΣ ∙ₑ Σ-swap-≃) + ∙ₑ invEquiv Σ-assoc-≃ + ∙ₑ invEquiv (fiberProjEquiv X _ x₀)) + (Σ-cong-equiv-snd (λ _ → invEquiv ΣPathP≃PathPΣ) + ∙ₑ invEquiv Σ-assoc-≃ + ∙ₑ invEquiv (fiberProjEquiv Y _ y₀)) + (funExt λ _ → transportRefl _) + (funExt λ _ → transportRefl _) + ∙ₑ joinPushout≃join _ _ + + fiber⋁↪≃ : fiber fun (x₀ , y₀) ≃ join (typ (Ω Y∙)) (typ (Ω X∙)) + fiber⋁↪≃ = Σ-cong-equiv-snd (λ a → pathToEquiv (sym (E≡ a))) + ∙ₑ flatten ∙ₑ Pushout≃ + +HMSplit : typ (Ω (X∙ ⋁∙ₗ Y∙)) ≡ typ (Ω X∙) × typ (Ω Y∙) × typ (Ω (Susp∙ (Ω Y∙ ⋀ Ω X∙))) +HMSplit = splitting + ∙ cong₂ (λ A B∙ → A × typ (Ω B∙)) (sym ΣPathP≡PathPΣ) + (ua∙ fiber⋁↪≃ refl ∙ ΣPathP + (sym (isoToPath SmashJoinIso) , toPathP refl)) + ∙ ua Σ-assoc-≃ + where open Split (inl x₀) ⋁↪ sect rInv diff --git a/Cubical/Homotopy/Loopspace.agda b/Cubical/Homotopy/Loopspace.agda index 36fef7ea1f..2f687d7aba 100644 --- a/Cubical/Homotopy/Loopspace.agda +++ b/Cubical/Homotopy/Loopspace.agda @@ -13,8 +13,10 @@ open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.HalfAdjoint open import Cubical.Foundations.Function open import Cubical.Foundations.Path +open import Cubical.Foundations.Univalence open import Cubical.Functions.Morphism +open import Cubical.Functions.Fibration open import Cubical.Data.Nat open import Cubical.Data.Sigma @@ -460,3 +462,79 @@ EH-π : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (p q : ∥ typ ((Ω^ (2 + n)) A) → π-comp (1 + n) p q ≡ π-comp (1 + n) q p EH-π n = elim2 (λ x y → isOfHLevelPath 2 isSetSetTrunc _ _) λ p q → cong ∣_∣₂ (EH n p q) + +{- + If A -> B -> C is a fiber sequence, and Ω B -> Ω C has a section, + then Ω B is the product Ω A × Ω C. + + https://gist.github.com/ecavallo/5b75313d36977c51ca3563de82506123 +-} + +module _ {ℓ} {B C : Type ℓ} (b₀ : B) (π : B → C) where + private + c₀ = π b₀ + A = fiber π c₀ + a₀ : A + a₀ = b₀ , refl + ι : A → B + ι = fst + π∘ι≡0 : ∀ a → π (ι a) ≡ c₀ + π∘ι≡0 = snd + + A∙ B∙ C∙ : Pointed _ + A∙ = (A , a₀) + B∙ = (B , b₀) + C∙ = (C , c₀) + + TwistedProduct : Pointed _ + TwistedProduct = ((Σ[ p ∈ typ (Ω C∙) ] (b₀ , p) ≡ a₀) , refl , refl) + + -- The middle term of a fiber sequence always splits + -- as a twisted product without any conditions. + presplit : Ω B∙ ≡ TwistedProduct + presplit = cong Ω (ua∙ (totalEquiv π) refl) + ∙ sym (ua∙ ΣPath≃PathΣ refl) + ∙ Σ-cong-equiv-snd∙ (λ p + → PathP≃Path _ _ _ ∙ₑ + compPathlEquiv (sym (fromPathP + (ΣPathP (refl , λ i j → p (i ∧ j)))))) + (rCancel λ j → transp (λ _ → A) (~ j) a₀) + + module Split (s : typ (Ω C∙) → typ (Ω B∙)) + (section : ∀ p → cong π (s p) ≡ p) where + movePoint : ∀ p → a₀ ≡ (b₀ , sym p) + movePoint p = ΣPathP (s p , + λ i j → slideSquare (section p) i (~ j)) + + splitting : typ (Ω B∙) ≡ typ (Ω C∙) × typ (Ω A∙) + splitting = cong typ presplit ∙ ua + (Σ-cong-equiv-snd λ p → compPathlEquiv (movePoint _)) + + -- If the section furthermore respects the base point, then + -- the splitting does too. + module _ (h : s refl ≡ refl) (coh : cong (cong π) h ≡ section refl) where + movePoint-refl : movePoint refl ≡ refl + movePoint-refl i j = h i j , λ k → + slideSquare (cong sym coh ∙ lemma _ _) (~ i) (~ k) j + where + lemma : ∀ {ℓ} {X : Type ℓ} {x : X} (p : x ≡ x) (q : p ≡ refl) + → sym q ≡ flipSquare (slideSquare q) + lemma {x = x} p q = J (λ p (q : refl ≡ p) + → q ≡ flipSquare (slideSquare (sym q))) + (λ i j k → hfill + (slideSquareFaces + {a₀₀ = x} {a₋ = refl} {a₁₋ = refl} {a₋₀ = refl} + j k) (inS x) i) + (sym q) + + twisted∙ : TwistedProduct ≡ Ω C∙ ×∙ Ω A∙ + twisted∙ = Σ-cong-equiv-snd∙ + (λ p → compPathlEquiv (movePoint _)) + (cong (λ t → compPathlEquiv t .fst refl) movePoint-refl ∙ sym (rUnit _)) + + splitting∙ : Ω B∙ ≡ Ω C∙ ×∙ Ω A∙ + splitting∙ = presplit ∙ twisted∙ + + -- splitting and splitting∙ agrees + splitting-typ : cong typ splitting∙ ≡ splitting + splitting-typ = congFunct typ presplit twisted∙