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βSets$
is given by the type
$β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
$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
$β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.

Sets-is-cocomplete : β {ΞΉ ΞΊ o} β is-cocomplete ΞΉ ΞΊ (Sets (ΞΉ β ΞΊ β o)) Sets-is-cocomplete {ΞΉ} {ΞΊ} {o} {J = 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 ] 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 $βF$ by the relation (generated by) identifying together all those points $(X,x)$ and $(Y,y)$ whenever there exists a map $(XfβY)β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
$Ο$
respects the quotient essentially by definition.

univ : β {A : Set (ΞΉ β ΞΊ β o)} β (eps : β j β 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 (Ξ» { (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
$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}ββFβ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 $β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 ix g h path = funext go where abstract path' : Path (β c β Ξ£[ i β I ] (F Κ» i)) (Ξ» c β _ , g c) (Ξ» c β _ , h c) path' i c = β₯-β₯β-elim {B = Ξ» _ β Ξ£ _ (β£_β£ β F)} (Ξ» x β hlevel 2) (Ξ» 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 $β₯$ using the assumption that $iξ=j.$

coprod .different-images-are-disjoint i j iβ j os = contr map uniq where map : Ξ£[ x β F i ] Ξ£[ y β F j ] (coprod.ΞΉ i x β‘ coprod.ΞΉ j y) β β£ 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))