-
Notifications
You must be signed in to change notification settings - Fork 63
/
Cocomplete.lagda.md
200 lines (162 loc) · 7.19 KB
/
Cocomplete.lagda.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
```agda
open import Cat.Diagram.Coproduct.Indexed
open import Cat.Instances.Sets.Complete
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Initial
open import Cat.Prelude
module Cat.Instances.Sets.Cocomplete where
```
# Sets is cocomplete
<!--
```agda
open Cocone-hom
open Initial
open Cocone
```
-->
Before proving that the [category of sets] is [cocomplete], as a warm-up
exercise, we prove that the category of sets admits [indexed
coproducts], and furthermore, that these are [disjoint]: all of the
coproduct inclusions are monomorphisms, and distinct inclusions have
initial images. This will be illustrative of a minor sticking point that
will come up in the construction of arbitrary colimits.
[indexed coproducts]: Cat.Diagram.Coproduct.Indexed.html
[cocomplete]: Cat.Diagram.Colimit.Base.html#cocompleteness
[category of sets]: Cat.Instances.Sets.html
[disjoint]: Cat.Diagram.Coproduct.Indexed.html#disjoint-coproducts
```agda
Sets-has-coproducts : ∀ {κ ℓ} → has-indexed-coproducts (Sets (κ ⊔ ℓ)) κ
Sets-has-coproducts {κ} {ℓ} {I = I} F = coprod where
```
The coproduct of the family $F : I \to \sets$ is given by the type $\sum
F$. However, this type is in general _not a set_! Consider a family of
sets indexed by [the circle]. Its total space will, by necessity, be a
[groupoid] rather than a set.
[the circle]: 1Lab.HIT.S1.html
[groupoid]: 1Lab.HLevel.html#is-groupoid
However, we can always [truncate] the sum down to a set, and it turns
out that this truncation _does_ serve as a coproduct of the family _in
the category of sets_. The point here is that, since the objects of
$\sets$ are.. well, sets, they can't have any interesting paths, _by
definition_. A grim slogan: In the category of Sets, nobody can hear
your paths scream.
[truncate]: Data.Set.Truncation.html
```agda
sum : Type (κ ⊔ ℓ)
sum = Σ[ i ∈ I ] ∣ F i ∣
open Indexed-coproduct
open is-indexed-coproduct
coprod : Indexed-coproduct (Sets _) F
coprod .ΣF = ∥ sum ∥₀ , squash
coprod .ι i x = inc (i , x)
coprod .has-is-ic .match {Y = Y} f =
∥-∥₀-elim (λ _ → Y .is-tr) λ { (i , x) → f i x } {- 1 -}
coprod .has-is-ic .commute = refl
coprod .has-is-ic .unique {Y = Y} f p = funext
(∥-∥₀-elim (λ _ → is-prop→is-set (Y .is-tr _ _)) λ x → happly (p _) _)
```
Note that, in the construction of `match`{.Agda} above, we used the fact
that $Y$ (the common codomain of all the $f_i$) is a set to `eliminate
from the truncation`{.Agda ident=∥-∥₀-elim} --- by definition, $Y$ can't
tell that $\sum F$ might have had some extra paths we squashed away.
## Colimits
Perfectly dually to the construction of [limits in $\sets$], rather than
taking the equaliser of a product, we take the [coequaliser] of a sum. The
same considerations about truncation level that apply for arbitrary
coproducts apply to arbitrary colimits: fortunately, the construction of
set-coequalisers already includes a truncation.
[limits in $\sets$]: Cat.Instances.Sets.Complete.html
[coequaliser]: Data.Set.Coequaliser.html
```agda
Sets-is-cocomplete : ∀ {ι κ o} → is-cocomplete ι κ (Sets (ι ⊔ κ ⊔ o))
Sets-is-cocomplete {D = D} F = colim where
module D = Precategory D
module F = Functor F
sum : Type _
sum = Σ[ d ∈ D.Ob ] ∣ F.₀ d ∣
rel : sum → sum → Type _
rel (X , x) (Y , y) = Σ[ f ∈ D.Hom X Y ] (F.₁ f x ≡ y)
```
The precise coequaliser we take is the [quotient] of $\sum F$ by the
relation (generated by) identifying together all those points $(X, x)$
and $(Y, y)$ whenever there exists a map $(X \xto{f} Y) \in \ca{D}$ such
that $F(f)(x) = y$.
[quotient]: Data.Set.Coequaliser.html#quotients
```agda
apex : Cocone F
apex .coapex = (sum / rel) , squash
apex .ψ x p = inc (x , p)
apex .commutes f = funext (λ i → sym (quot (f , refl)))
```
By the same truncation nonsense as above, we can apply `Coeq-rec`{.Agda}
to eliminate from our quotient to the coapex of any other cocone over
$F$; The family of maps $\psi$ respects the quotient essentially by
definition.
```agda
colim : Initial _
colim .bot = apex
colim .has⊥ other = contr map unique where
map : Cocone-hom F apex other
map .hom = Coeq-rec (other .coapex .is-tr) (λ { (x , p) → other .ψ x p })
λ { ((X , x) , (Y , y) , f , p) →
sym (happly (other .commutes f) x) ∙ ap (other .ψ Y) p
}
map .commutes o = refl
unique : ∀ x → map ≡ x
unique hom′ = Cocone-hom-path _
(funext (Coeq-elim-prop (λ x → other .coapex .is-tr _ _)
λ y → sym (happly (hom′ .commutes _) _)))
```
# Coproducts are disjoint
As a final lemma, we prove that coproducts in $\sets$, as constructed
above, are disjoint. However, this does not apply to _arbitrary_
coproducts; To prove that the injections are monomorphisms, we require
that the indexing type be a set.
```agda
module _ {κ} {I : Set κ} {F : ∣ I ∣ → Set κ} where
private module coprod = Indexed-coproduct (Sets-has-coproducts {ℓ = κ} F)
Set-disjoint-coprods : is-disjoint-coproduct (Sets κ) {S = coprod.ΣF} F coprod.ι
Set-disjoint-coprods = coprod where
open is-disjoint-coproduct
open is-indexed-coproduct
```
We already know that the coproduct is a coproduct (who would have
guessed, honestly) --- so it remains to show that the `injections are
monic`{.Agda ident=injections-are-monic}, the `summands intersect`{.Agda
ident=summands-intersect}, and the intersections of different summands
are empty. The intersections are cheap: Sets is finitely complete, so
all pullbacks exist, in particular the pullback of $F_i \to \sum F \ot
F_j$.
```agda
coprod : is-disjoint-coproduct _ _ _
coprod .is-coproduct = coprod.has-is-ic
coprod .summands-intersect i j = Sets-pullbacks _ _
```
To prove that the injections are monic, we use our assumption that the
family $F$ was indexed by a set: The sum $\sum F$ then is also a set, so
we can get it out from under the truncation in the definition of
coproduct.
```agda
coprod .injections-are-monic _ g h path = funext go where abstract
path′ : Path (∀ c → Σ (λ x → ∣ F x ∣)) (λ c → _ , g c) (λ c → _ , h c)
path′ i c = ∥-∥₀-elim {B = λ _ → Σ (∣_∣ ⊙ F)}
(λ x → Σ-is-hlevel 2 (I .is-tr) (λ x → F x .is-tr))
(λ x → x) (path i c)
q : ∀ {c} → ap fst (happly path′ c) ≡ refl
q = I .is-tr _ _ _ _
go : ∀ c → g c ≡ h c
go c = subst (λ e → PathP (λ i → ∣ F (e i) ∣) (g c) (h c)) q
(ap snd (happly path′ c))
```
The same thing happens in proving that different injections have
disjoint images: We must project out a path $i = j$ from a path $\|
(i,-) = (j,-) \|$ --- using that they are in a set to eliminate from the
truncation --- to prove $\bot$ using the assumption that $i ≠ j$.
```agda
coprod .different-images-are-disjoint i j i≠j os = contr map uniq where
map : Σ[ i ∈ ∣ F i ∣ ] Σ (λ x → _) → ∣ os ∣
map (i , j , p) = absurd (i≠j (ap (∥-∥₀-elim (λ _ → I .is-tr) fst) p))
uniq : ∀ x → map ≡ x
uniq _ = funext λ where
(_ , _ , p) → absurd (i≠j (ap (∥-∥₀-elim (λ _ → I .is-tr) fst) p))
```