module Cat.Instances.Sets.Cocomplete where

# Sets is cocompleteπ

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.

Sets-has-coproducts : β {ΞΊ β} β has-indexed-coproducts (Sets (ΞΊ β β)) ΞΊ Sets-has-coproducts {ΞΊ} {β} {I = I} F = coprod where

The coproduct of the family
$F : I \to \mathbf{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.

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
$\mathbf{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.

sum : Type (ΞΊ β β) sum = Ξ£[ i β I ] β£ F i β£ open Indexed-coproduct open is-indexed-coproduct coprod : Indexed-coproduct (Sets _) F coprod .Ξ£F = el β₯ 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 above, we used the fact that $Y$ (the common codomain of all the $f_i$) is a set to eliminate from the truncation β 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 $\mathbf{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.

Sets-is-cocomplete : β {ΞΉ ΞΊ o} β is-cocomplete ΞΉ ΞΊ (Sets (ΞΉ β ΞΊ β o)) Sets-is-cocomplete {ΞΉ} {ΞΊ} {o} {D = D} F = to-colimit (to-is-colimit colim) where module D = Precategory D module F = Functor F open _=>_ open make-is-colimit 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 \xrightarrow{f} Y) \in \mathcal{D}$ such that $F(f)(x) = y$.

By the same truncation nonsense as above, we can apply Coeq-rec 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.

univ : β {A : Set (ΞΉ β ΞΊ β o)} β (eps : β j β β£ F.Fβ j β£ β β£ A β£) β (β {x y} (f : D.Hom x y) β β Fx β eps y (F.Fβ f Fx) β‘ eps x Fx) β sum / rel β β£ A β£ univ {A} eps p = Coeq-rec (A .is-tr) (Ξ» { (x , p) β eps x p }) (Ξ» { ((X , x) , (Y , y) , f , q) β sym (p f x) β ap (eps _) q}) colim : make-is-colimit F (el! (sum / rel)) colim .Ο x p = inc (x , p) colim .commutes f = funext Ξ» _ β sym (quot (f , refl)) colim .universal {A} eps p x = univ {A} eps (Ξ» f β happly (p f)) x colim .factors eps p = refl colim .unique {A} eps p other q = funext Ξ» x β Coeq-elim-prop (Ξ» x β A .is-tr (other x) (univ {A} eps (Ξ» f β happly (p f)) x)) (Ξ» x β happly (q (x .fst)) (x .snd)) x

# Coproducts are disjointπ

As a final lemma, we prove that coproducts in
$\mathbf{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.

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, the 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 \leftarrow F_j$.

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.

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 β hlevel!) (Ξ» 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$.

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))