Skip to content

Commit 35d2919

Browse files
ecavalloecavallo
authored
Merge pull request #1157 from Trebor-Huang/devalapurkar-haine
Devalapurkar & Haine
2 parents 385066b + cb0510c commit 35d2919

File tree

11 files changed

+732
-7
lines changed

11 files changed

+732
-7
lines changed

‎Cubical/Foundations/Pointed/Properties.agda‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -245,6 +245,14 @@ compPathlEquiv∙ : {A : Type ℓ} {a b c : A} {q : b ≡ c} (p : a ≡ b)
245245
fst (compPathlEquiv∙ p) = compPathlEquiv p
246246
snd (compPathlEquiv∙ p) = refl
247247

248+
-- Pointed version of Σ-cong-equiv-snd
249+
Σ-cong-equiv-snd∙ : ∀ {ℓ ℓ'} {A : Type ℓ} {B₁ B₂ : A → Type ℓ'}
250+
→ {a : A} {b₁ : B₁ a} {b₂ : B₂ a}
251+
→ (e : ∀ a → B₁ a ≃ B₂ a)
252+
→ fst (e a) b₁ ≡ b₂
253+
→ Path (Pointed _) (Σ∙ (A , a) B₁ b₁) (Σ∙ (A , a) B₂ b₂)
254+
Σ-cong-equiv-snd∙ e p = ua∙ (Σ-cong-equiv-snd e) (ΣPathP (refl , p))
255+
248256
-- a pointed map is constant iff its non-pointed part is constant
249257
constantPointed≡ : {A B : Pointed ℓ} (f : A →∙ B)
250258
→ fst f ≡ fst (const∙ A B) → f ≡ const∙ A B

‎Cubical/HITs/James/Stable.agda‎

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
{-# OPTIONS --safe #-}
2+
3+
{-
4+
The stable version of the James splitting:
5+
ΣΩΣX ≃ ΣX ⋁ Σ(X ⋀ ΩΣX)
6+
-}
7+
8+
open import Cubical.Foundations.Prelude
9+
open import Cubical.Foundations.Path
10+
open import Cubical.Foundations.Equiv
11+
open import Cubical.Foundations.Pointed
12+
open import Cubical.Foundations.Transport
13+
open import Cubical.Foundations.Univalence
14+
open import Cubical.Foundations.HLevels
15+
open import Cubical.Foundations.Function
16+
17+
open import Cubical.Data.Sigma
18+
open import Cubical.Data.Unit
19+
20+
open import Cubical.HITs.Susp
21+
open import Cubical.HITs.Susp.SuspProduct
22+
open import Cubical.HITs.Pushout
23+
open import Cubical.HITs.Pushout.Flattening
24+
open import Cubical.HITs.Wedge
25+
open import Cubical.HITs.SmashProduct
26+
27+
open import Cubical.Homotopy.Loopspace
28+
29+
module Cubical.HITs.James.Stable {ℓ} (X∙@(X , x₀) : Pointed ℓ) where
30+
31+
module ContrPushout where
32+
Code : Pushout (terminal X) (terminal X) → Type ℓ
33+
Code x = inl _ ≡ x
34+
35+
ΩΣX = Code (inl _)
36+
ΩΣX∙ : Pointed _
37+
ΩΣX∙ = ΩΣX , refl
38+
39+
α : X × ΩΣX → ΩΣX
40+
α (x , p) = (p ∙ push x) ∙ sym (push x₀)
41+
42+
open FlatteningLemma
43+
(terminal X) (terminal X)
44+
(Code ∘ inl) (Code ∘ inr)
45+
(pathToEquiv ∘ cong (inl tt ≡_) ∘ push)
46+
47+
pushoutEq : Pushout Σf Σg ≃ Pushout snd α
48+
pushoutEq = pushoutEquiv _ _ _ _
49+
(idEquiv (X × ΩΣX)) (ΣUnit _)
50+
(ΣUnit _ ∙ₑ compPathrEquiv (sym (push x₀)))
51+
refl (funExt λ (x , p)
52+
→ cong (_∙ sym (push x₀)) (substInPathsL (push x) p))
53+
54+
Code≡E : ∀ x → Code x ≡ E x
55+
Code≡E (inl _) = refl
56+
Code≡E (inr _) = refl
57+
Code≡E (push a i) j = uaη (cong Code (push a)) (~ j) i
58+
59+
isContrΣE : isContr (Σ _ E)
60+
isContrΣE = subst isContr (Σ-cong-snd Code≡E) (isContrSingl (inl tt))
61+
62+
isContrPushout : isContr (Pushout snd α)
63+
isContrPushout = isOfHLevelRespectEquiv _ (flatten ∙ₑ pushoutEq) isContrΣE
64+
65+
open ContrPushout
66+
67+
LoopSuspSquare : commSquare
68+
LoopSuspSquare = record
69+
{ sp = 3span snd α
70+
; P = Unit* {ℓ}
71+
; comm = refl }
72+
73+
LoopSuspPushoutSquare : PushoutSquare
74+
LoopSuspPushoutSquare = (LoopSuspSquare , isContr→≃Unit* isContrPushout .snd)
75+
76+
open PushoutPasteLeft LoopSuspPushoutSquare
77+
(λ _ → lift {j = ℓ} tt) _ _ (funExt merid)
78+
79+
cofib-snd-James : cofib (λ (r : X × ΩΣX) → snd r) ≃ Susp ΩΣX
80+
cofib-snd-James = pushoutSwitchEquiv
81+
∙ₑ pushoutEquiv snd _ snd _
82+
(idEquiv _) (idEquiv _) Unit≃Unit* refl refl
83+
∙ₑ (_ , isPushoutRightSquare→isPushoutTotSquare
84+
(SuspPushoutSquare _ _ ΩΣX))
85+
86+
StableJames : Susp ΩΣX ≃ Susp∙ X ⋁ Susp∙ (X∙ ⋀ ΩΣX∙)
87+
StableJames = invEquiv cofib-snd-James ∙ₑ cofib-snd X∙ (ΩΣX , refl)

‎Cubical/HITs/Join/Properties.agda‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,15 @@ private
3636
variable
3737
ℓ ℓ' : Level
3838

39+
-- the inclusion maps are null-homotopic
40+
join-inl-null : {X : Pointed ℓ} {Y : Pointed ℓ'} (x : typ X)
41+
→ Path (join (typ X) (typ Y)) (inl x) (inl (pt X))
42+
join-inl-null {X = X} {Y} x = push x (pt Y) ∙ sym (push (pt X) (pt Y))
43+
44+
join-inr-null : {X : Pointed ℓ} {Y : Type ℓ'} (y : Y)
45+
→ Path (join (typ X) Y) (inr y) (inl (pt X))
46+
join-inr-null {X = X} y = sym (push (pt X) y)
47+
3948
open Iso
4049

4150
-- Characterisation of function type join A B → C

‎Cubical/HITs/Pushout/Properties.agda‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,28 @@ pushoutSwitchEquiv = isoToEquiv (iso f inv leftInv rightInv)
7575
leftInv = λ {(inl x) → refl; (inr x) → refl; (push a i) → refl}
7676
rightInv = λ {(inl x) → refl; (inr x) → refl; (push a i) → refl}
7777

78+
79+
{-
80+
Direct proof that pushout along the identity gives an equivalence.
81+
-}
82+
pushoutIdfunEquiv : ∀ {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'} (f : X → Y)
83+
→ Y ≃ Pushout f (idfun X)
84+
pushoutIdfunEquiv f = isoToEquiv (iso inl inv leftInv λ _ → refl)
85+
where
86+
inv : Pushout f (idfun _) → _
87+
inv (inl y) = y
88+
inv (inr x) = f x
89+
inv (push x i) = f x
90+
91+
leftInv : section inl inv
92+
leftInv (inl y) = refl
93+
leftInv (inr x) = push x
94+
leftInv (push a i) j = push a (i ∧ j)
95+
96+
pushoutIdfunEquiv' : ∀ {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'} (f : X → Y)
97+
→ Y ≃ Pushout (idfun X) f
98+
pushoutIdfunEquiv' f = compEquiv (pushoutIdfunEquiv _) pushoutSwitchEquiv
99+
78100
{-
79101
Definition of pushout diagrams
80102
-}
@@ -809,6 +831,48 @@ module _ {ℓ₀ ℓ₂ ℓ₄ ℓP : Level} where
809831
PushoutSquare : Type (ℓ-suc ℓ*)
810832
PushoutSquare = Σ commSquare isPushoutSquare
811833

834+
module _ {ℓ₀ ℓ₂ ℓ₄ ℓP ℓP' : Level}
835+
{P' : Type ℓP'} where
836+
open commSquare
837+
extendCommSquare : (sk : commSquare {ℓ₀} {ℓ₂} {ℓ₄} {ℓP})
838+
→ (sk .P → P') → commSquare
839+
extendCommSquare sk f .sp = sk .sp
840+
extendCommSquare sk f .P = P'
841+
extendCommSquare sk f .inlP = f ∘ sk .inlP
842+
extendCommSquare sk f .inrP = f ∘ sk .inrP
843+
extendCommSquare sk f .comm = cong (f ∘_) (sk .comm)
844+
845+
846+
extendPushoutSquare : (sk : PushoutSquare {ℓ₀} {ℓ₂} {ℓ₄} {ℓP})
847+
→ (e : sk .fst .P ≃ P') → PushoutSquare
848+
extendPushoutSquare sk e = (extendCommSquare (sk .fst) (e .fst) ,
849+
subst isEquiv H (compEquiv (_ , sk .snd) e .snd))
850+
where
851+
H : e .fst ∘ _ ≡ _
852+
H = funExt λ
853+
{ (inl x) → refl
854+
; (inr x) → refl
855+
; (push a i) → refl }
856+
857+
-- Pushout itself fits into a pushout square
858+
pushoutToSquare : 3-span {ℓ} {ℓ'} {ℓ''} → PushoutSquare
859+
pushoutToSquare spn .fst = cSq
860+
where
861+
open commSquare
862+
cSq : commSquare
863+
cSq .sp = spn
864+
cSq .P = spanPushout spn
865+
cSq .inlP = inl
866+
cSq .inrP = inr
867+
cSq .comm = funExt push
868+
pushoutToSquare sp .snd =
869+
subst isEquiv (funExt H) (idIsEquiv _)
870+
where
871+
H : ∀ p → p ≡ Pushout→commSquare _ p
872+
H (inl x) = refl
873+
H (inr x) = refl
874+
H (push a i) = refl
875+
812876
-- Rotations of commutative squares and pushout squares
813877
module _ {ℓ₀ ℓ₂ ℓ₄ ℓP : Level} where
814878
open commSquare

‎Cubical/HITs/SmashProduct/Base.agda‎

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -67,13 +67,8 @@ commK (gluer b x) = refl
6767

6868
--- Alternative definition
6969

70-
i∧ : {A : Pointed ℓ} {B : Pointed ℓ'} → A ⋁ B → (typ A) × (typ B)
71-
i∧ {A = A , ptA} {B = B , ptB} (inl x) = x , ptB
72-
i∧ {A = A , ptA} {B = B , ptB} (inr x) = ptA , x
73-
i∧ {A = A , ptA} {B = B , ptB} (push tt i) = ptA , ptB
74-
7570
_⋀_ : Pointed ℓ → Pointed ℓ' → Type (ℓ-max ℓ ℓ')
76-
A ⋀ B = Pushout {A = (A ⋁ B)} (λ _ → tt) i∧
71+
A ⋀ B = Pushout {A = (A ⋁ B)} (λ _ → tt) ⋁↪
7772

7873
_⋀∙_ : Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
7974
A ⋀∙ B = (A ⋀ B) , (inl tt)

‎Cubical/HITs/Susp/Properties.agda‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,12 +10,15 @@ open import Cubical.Foundations.Pointed
1010
open import Cubical.Foundations.Pointed.Homogeneous
1111
open import Cubical.Foundations.GroupoidLaws
1212
open import Cubical.Foundations.Function
13+
open import Cubical.Foundations.Univalence
1314

1415
open import Cubical.Data.Bool
1516
open import Cubical.Data.Sigma
17+
open import Cubical.Data.Unit
1618

1719
open import Cubical.HITs.Join
1820
open import Cubical.HITs.Susp.Base
21+
open import Cubical.HITs.Pushout
1922
open import Cubical.Homotopy.Loopspace
2023

2124
private
@@ -73,6 +76,47 @@ Susp≃joinBool = isoToEquiv Susp-iso-joinBool
7376
Susp≡joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≡ join A Bool
7477
Susp≡joinBool = isoToPath Susp-iso-joinBool
7578

79+
-- Here Unit* types are more convenient for general A
80+
SuspSpan : ∀ {ℓ} ℓ' ℓ'' (A : Type ℓ) → 3-span {ℓ'} {ℓ} {ℓ''}
81+
SuspSpan ℓ' ℓ'' A = record { A2 = A ; A0 = Unit* {ℓ'} ; A4 = Unit* {ℓ''} }
82+
83+
SuspSquare : ∀ {ℓ} ℓ' ℓ'' (A : Type ℓ) → commSquare {ℓ'} {ℓ} {ℓ''}
84+
SuspSquare ℓ' ℓ'' A = cSq
85+
where
86+
open commSquare
87+
cSq : commSquare
88+
cSq .sp = SuspSpan ℓ' ℓ'' A
89+
cSq .P = Susp A
90+
cSq .inlP _ = north
91+
cSq .inrP _ = south
92+
cSq .comm = funExt merid
93+
94+
SuspPushoutSquare : ∀ {ℓ} ℓ' ℓ'' (A : Type ℓ)
95+
→ isPushoutSquare (SuspSquare ℓ' ℓ'' A)
96+
SuspPushoutSquare ℓ' ℓ'' A = isoToIsEquiv (iso _ inverse rInv lInv)
97+
where
98+
inverse : _
99+
inverse north = inl _
100+
inverse south = inr _
101+
inverse (merid a i) = push a i
102+
103+
rInv : _
104+
rInv north = refl
105+
rInv south = refl
106+
rInv (merid a i) = refl
107+
108+
lInv : _
109+
lInv (inl x) = refl
110+
lInv (inr x) = refl
111+
lInv (push a i) = refl
112+
113+
Susp≃PushoutSusp* : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} → Susp A ≃ spanPushout (SuspSpan ℓ' ℓ'' A)
114+
Susp≃PushoutSusp* {ℓ} {ℓ'} {ℓ''} {A} = invEquiv (_ , SuspPushoutSquare ℓ' ℓ'' A)
115+
116+
Susp≡PushoutSusp* : ∀ {ℓ ℓ' ℓ''} {A : Type _} → Susp A ≡ spanPushout (SuspSpan ℓ' ℓ'' A)
117+
Susp≡PushoutSusp* {ℓ} {ℓ'} {ℓ''} = ua
118+
(Susp≃PushoutSusp* {ℓ-max ℓ (ℓ-max ℓ' ℓ'')} {ℓ'} {ℓ''})
119+
76120
congSuspIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Iso A B → Iso (Susp A) (Susp B)
77121
fun (congSuspIso is) = suspFun (fun is)
78122
inv (congSuspIso is) = suspFun (inv is)

0 commit comments

Comments
 (0)