Skip to content

Commit 7affe55

Browse files
ecavalloecavallo
authored
Merge pull request #529 from LuuBluum/sum
Sum type properties
2 parents 9b11e86 + 5ada3e4 commit 7affe55

File tree

3 files changed

+86
-37
lines changed

3 files changed

+86
-37
lines changed

‎Cubical/Data/Fin/LehmerCode.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ lehmerEquiv {suc n} =
157157
Fin (suc n)
158158
≃⟨ invEquiv projectionEquiv ⟩
159159
Unit ⊎ FinExcept fzero
160-
≃⟨ isoToEquiv (Sum.sumIso idIso (equivToIso f)) ⟩
160+
≃⟨ isoToEquiv (Sum.⊎Iso idIso (equivToIso f)) ⟩
161161
Unit ⊎ FinExcept k
162162
≃⟨ projectionEquiv ⟩
163163
Fin (suc n)

‎Cubical/Data/Fin/Recursive/Properties.agda

+4-4
Original file line numberDiff line numberDiff line change
@@ -231,22 +231,22 @@ module Isos where
231231
up : Fin m → Fin (m + n)
232232
up {m} = inject≤ (k≤k+n m)
233233

234-
resplit-identᵣ₀ : ∀ m (i : Fin n) → Sum.SumPath.Cover (split m (m ⊕ i)) (inr i)
234+
resplit-identᵣ₀ : ∀ m (i : Fin n) → Sum.⊎Path.Cover (split m (m ⊕ i)) (inr i)
235235
resplit-identᵣ₀ zero i = lift refl
236236
resplit-identᵣ₀ (suc m) i with split m (m ⊕ i) | resplit-identᵣ₀ m i
237237
... | inr j | p = p
238238

239239
resplit-identᵣ : ∀ m (i : Fin n) → split m (m ⊕ i) ≡ inr i
240-
resplit-identᵣ m i = Sum.SumPath.decode _ _ (resplit-identᵣ₀ m i)
240+
resplit-identᵣ m i = Sum.⊎Path.decode _ _ (resplit-identᵣ₀ m i)
241241

242-
resplit-identₗ₀ : ∀ m (i : Fin m) → Sum.SumPath.Cover (split {n} m (up i)) (inl i)
242+
resplit-identₗ₀ : ∀ m (i : Fin m) → Sum.⊎Path.Cover (split {n} m (up i)) (inl i)
243243
resplit-identₗ₀ (suc m) zero = lift refl
244244
resplit-identₗ₀ {n} (suc m) (suc i)
245245
with split {n} m (up i) | resplit-identₗ₀ {n} m i
246246
... | inl j | lift p = lift (cong suc p)
247247

248248
resplit-identₗ : ∀ m (i : Fin m) → split {n} m (up i) ≡ inl i
249-
resplit-identₗ m i = Sum.SumPath.decode _ _ (resplit-identₗ₀ m i)
249+
resplit-identₗ m i = Sum.⊎Path.decode _ _ (resplit-identₗ₀ m i)
250250

251251
desplit-ident : ∀ m → (i : Fin (m + n)) → Sum.rec up (m ⊕_) (split m i) ≡ i
252252
desplit-ident zero i = refl

‎Cubical/Data/Sum/Properties.agda

+81-32
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,20 @@ open import Cubical.Data.Nat
1212

1313
open import Cubical.Data.Sum.Base
1414

15+
open Iso
16+
17+
18+
private
19+
variable
20+
ℓa ℓb ℓc ℓd : Level
21+
A : Type ℓa
22+
B : Type ℓb
23+
C : Type ℓc
24+
D : Type ℓd
25+
26+
1527
-- Path space of sum type
16-
module SumPath {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
28+
module ⊎Path {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
1729

1830
Cover : A ⊎ B → A ⊎ B → Type (ℓ-max ℓ ℓ')
1931
Cover (inl a) (inl a') = Lift {j = ℓ-max ℓ ℓ'} (a ≡ a')
@@ -67,40 +79,77 @@ module SumPath {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
6779
isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥)
6880
isOfHLevelCover n p q (inr b) (inr b') = isOfHLevelLift (suc n) (q b b')
6981

70-
isEmbedding-inl : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → isEmbedding (inl {A = A} {B = B})
71-
isEmbedding-inl w z = snd (compEquiv LiftEquiv (SumPath.Cover≃Path (inl w) (inl z)))
82+
isEmbedding-inl : isEmbedding (inl {A = A} {B = B})
83+
isEmbedding-inl w z = snd (compEquiv LiftEquiv (⊎Path.Cover≃Path (inl w) (inl z)))
7284

73-
isEmbedding-inr : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → isEmbedding (inr {A = A} {B = B})
74-
isEmbedding-inr w z = snd (compEquiv LiftEquiv (SumPath.Cover≃Path (inr w) (inr z)))
85+
isEmbedding-inr : isEmbedding (inr {A = A} {B = B})
86+
isEmbedding-inr w z = snd (compEquiv LiftEquiv (⊎Path.Cover≃Path (inr w) (inr z)))
7587

76-
isOfHLevelSum : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} {B : Type ℓ'}
88+
isOfHLevel⊎ : (n : HLevel)
7789
→ isOfHLevel (suc (suc n)) A
7890
→ isOfHLevel (suc (suc n)) B
7991
→ isOfHLevel (suc (suc n)) (A ⊎ B)
80-
isOfHLevelSum n lA lB c c' =
92+
isOfHLevel⊎ n lA lB c c' =
8193
isOfHLevelRetract (suc n)
82-
(SumPath.encode c c')
83-
(SumPath.decode c c')
84-
(SumPath.decodeEncode c c')
85-
(SumPath.isOfHLevelCover n lA lB c c')
86-
87-
isSetSum : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → isSet A → isSet B → isSet (A ⊎ B)
88-
isSetSum = isOfHLevelSum 0
89-
90-
isGroupoidSum : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → isGroupoid A → isGroupoid B → isGroupoid (A ⊎ B)
91-
isGroupoidSum = isOfHLevelSum 1
92-
93-
is2GroupoidSum : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is2Groupoid A → is2Groupoid B → is2Groupoid (A ⊎ B)
94-
is2GroupoidSum = isOfHLevelSum 2
95-
96-
sumIso : ∀ {ℓa ℓb ℓc ℓd} {A : Type ℓa} {B : Type ℓb} {C : Type ℓc} {D : Type ℓd}
97-
→ Iso A C → Iso B D
98-
→ Iso (A ⊎ B) (C ⊎ D)
99-
Iso.fun (sumIso iac ibd) (inl x) = inl (iac .Iso.fun x)
100-
Iso.fun (sumIso iac ibd) (inr x) = inr (ibd .Iso.fun x)
101-
Iso.inv (sumIso iac ibd) (inl x) = inl (iac .Iso.inv x)
102-
Iso.inv (sumIso iac ibd) (inr x) = inr (ibd .Iso.inv x)
103-
Iso.rightInv (sumIso iac ibd) (inl x) = cong inl (iac .Iso.rightInv x)
104-
Iso.rightInv (sumIso iac ibd) (inr x) = cong inr (ibd .Iso.rightInv x)
105-
Iso.leftInv (sumIso iac ibd) (inl x) = cong inl (iac .Iso.leftInv x)
106-
Iso.leftInv (sumIso iac ibd) (inr x) = cong inr (ibd .Iso.leftInv x)
94+
(⊎Path.encode c c')
95+
(⊎Path.decode c c')
96+
(⊎Path.decodeEncode c c')
97+
(⊎Path.isOfHLevelCover n lA lB c c')
98+
99+
isSet⊎ : isSet A → isSet B → isSet (A ⊎ B)
100+
isSet⊎ = isOfHLevel⊎ 0
101+
102+
isGroupoid⊎ : isGroupoid A → isGroupoid B → isGroupoid (A ⊎ B)
103+
isGroupoid⊎ = isOfHLevel⊎ 1
104+
105+
is2Groupoid⊎ : is2Groupoid A → is2Groupoid B → is2Groupoid (A ⊎ B)
106+
is2Groupoid⊎ = isOfHLevel⊎ 2
107+
108+
⊎Iso : Iso A C → Iso B D → Iso (A ⊎ B) (C ⊎ D)
109+
fun (⊎Iso iac ibd) (inl x) = inl (iac .fun x)
110+
fun (⊎Iso iac ibd) (inr x) = inr (ibd .fun x)
111+
inv (⊎Iso iac ibd) (inl x) = inl (iac .inv x)
112+
inv (⊎Iso iac ibd) (inr x) = inr (ibd .inv x)
113+
rightInv (⊎Iso iac ibd) (inl x) = cong inl (iac .rightInv x)
114+
rightInv (⊎Iso iac ibd) (inr x) = cong inr (ibd .rightInv x)
115+
leftInv (⊎Iso iac ibd) (inl x) = cong inl (iac .leftInv x)
116+
leftInv (⊎Iso iac ibd) (inr x) = cong inr (ibd .leftInv x)
117+
118+
⊎-swap-Iso : Iso (A ⊎ B) (B ⊎ A)
119+
fun ⊎-swap-Iso (inl x) = inr x
120+
fun ⊎-swap-Iso (inr x) = inl x
121+
inv ⊎-swap-Iso (inl x) = inr x
122+
inv ⊎-swap-Iso (inr x) = inl x
123+
rightInv ⊎-swap-Iso (inl _) = refl
124+
rightInv ⊎-swap-Iso (inr _) = refl
125+
leftInv ⊎-swap-Iso (inl _) = refl
126+
leftInv ⊎-swap-Iso (inr _) = refl
127+
128+
⊎-swap-≃ : A ⊎ B ≃ B ⊎ A
129+
⊎-swap-≃ = isoToEquiv ⊎-swap-Iso
130+
131+
⊎-assoc-Iso : Iso ((A ⊎ B) ⊎ C) (A ⊎ (B ⊎ C))
132+
fun ⊎-assoc-Iso (inl (inl x)) = inl x
133+
fun ⊎-assoc-Iso (inl (inr x)) = inr (inl x)
134+
fun ⊎-assoc-Iso (inr x) = inr (inr x)
135+
inv ⊎-assoc-Iso (inl x) = inl (inl x)
136+
inv ⊎-assoc-Iso (inr (inl x)) = inl (inr x)
137+
inv ⊎-assoc-Iso (inr (inr x)) = inr x
138+
rightInv ⊎-assoc-Iso (inl _) = refl
139+
rightInv ⊎-assoc-Iso (inr (inl _)) = refl
140+
rightInv ⊎-assoc-Iso (inr (inr _)) = refl
141+
leftInv ⊎-assoc-Iso (inl (inl _)) = refl
142+
leftInv ⊎-assoc-Iso (inl (inr _)) = refl
143+
leftInv ⊎-assoc-Iso (inr _) = refl
144+
145+
⊎-assoc-≃ : (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
146+
⊎-assoc-≃ = isoToEquiv ⊎-assoc-Iso
147+
148+
⊎-⊥-Iso : Iso (A ⊎ ⊥) A
149+
fun ⊎-⊥-Iso (inl x) = x
150+
inv ⊎-⊥-Iso x = inl x
151+
rightInv ⊎-⊥-Iso x = refl
152+
leftInv ⊎-⊥-Iso (inl x) = refl
153+
154+
⊎-⊥-≃ : A ⊎ ⊥ ≃ A
155+
⊎-⊥-≃ = isoToEquiv ⊎-⊥-Iso

0 commit comments

Comments
 (0)