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)} β (eta : β j β F Κ» j β β£ A β£) β (β {x y} (f : D.Hom x y) β β Fx β eta y (F.Fβ f Fx) β‘ eta x Fx) β sum / rel β β£ A β£ univ {A} eta p = Coeq-rec (Ξ» { (x , p) β eta x p }) (Ξ» { ((X , x) , (Y , y) , f , q) β sym (p f x) β ap (eta _) 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} eta p x = univ {A} eta (Ξ» f β happly (p f)) x colim .factors eta p = refl colim .unique {A} eta p other q = funext Ξ» x β Coeq-elim-prop (Ξ» x β A .is-tr (other x) (univ {A} eta (Ξ» f β happly (p f)) x)) (Ξ» x β happly (q (x .fst)) (x .snd)) x

## Finite set-colimitsπ

module _ {β} where open Precategory (Sets β) private variable A B : Set β f g : β A β β β B β open Initial open is-coproduct open Coproduct open is-pushout open Pushout open is-coequaliser open Coequaliser

For expository reasons, we present the computation of the most famous
shapes of finite
colimit (initial
objects, coproducts, pushouts, and coequalisers) in
the category of sets. All the definitions below are redundant, since
finite colimits are always small, and thus the category of sets of
*any* level
$β$
admits them.

Sets-initial : Initial (Sets β) Sets-initial .bot = el! (Lift _ β₯) Sets-initial .hasβ₯ _ .centre () Sets-initial .hasβ₯ _ .paths _ = ext Ξ» ()

Coproducts are given by disjoint sums:

Sets-coproducts : (A B : Set β) β Coproduct (Sets β) A B Sets-coproducts A B .coapex = el! (β£ A β£ β β£ B β£) Sets-coproducts A B .ΞΉβ = inl Sets-coproducts A B .ΞΉβ = inr Sets-coproducts A B .has-is-coproduct .is-coproduct.[_,_] f g = Data.Sum.[ f , g ] Sets-coproducts A B .has-is-coproduct .[]βΞΉβ = refl Sets-coproducts A B .has-is-coproduct .[]βΞΉβ = refl Sets-coproducts A B .has-is-coproduct .unique p q = sym ([]-unique (sym p) (sym q))

Set coequalisers are described in their own module.

Sets-coequalisers : (f g : Hom A B) β Coequaliser (Sets β) {A = A} {B = B} f g Sets-coequalisers f g .coapex .β£_β£ = Coeq f g Sets-coequalisers f g .coapex .is-tr = hlevel 2 Sets-coequalisers f g .coeq = inc Sets-coequalisers f g .has-is-coeq .coequal = ext Ξ» x β glue _ Sets-coequalisers f g .has-is-coeq .universal {e' = e'} p = Coeq-rec e' (unext p) Sets-coequalisers f g .has-is-coeq .factors = refl Sets-coequalisers f g .has-is-coeq .unique q = reext! q

Pushouts are similar to coequalisers, but gluing together points of $A+B.$

Sets-pushouts : β {A B C} (f : Hom C A) (g : Hom C B) β Pushout (Sets β) {X = C} {Y = A} {Z = B} f g Sets-pushouts f g .coapex .β£_β£ = Coeq (inl β f) (inr β g) Sets-pushouts f g .coapex .is-tr = hlevel 2 Sets-pushouts f g .iβ a = inc (inl a) Sets-pushouts f g .iβ b = inc (inr b) Sets-pushouts f g .has-is-po .square = ext Ξ» x β glue _ Sets-pushouts f g .has-is-po .universal {iβ' = iβ'} {iβ'} p = Coeq-rec Data.Sum.[ iβ' , iβ' ] (unext p) Sets-pushouts f g .has-is-po .universalβiβ = refl Sets-pushouts f g .has-is-po .universalβiβ = refl Sets-pushouts f g .has-is-po .unique q r = ext (Equiv.from β-universal (unext q , unext r))

Hence, `Sets`

is finitely
cocomplete:

open Finitely-cocomplete Sets-finitely-cocomplete : Finitely-cocomplete (Sets β) Sets-finitely-cocomplete .initial = Sets-initial Sets-finitely-cocomplete .coproducts = Sets-coproducts Sets-finitely-cocomplete .coequalisers = Sets-coequalisers Sets-finitely-cocomplete .pushouts = Sets-pushouts

# 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 .has-is-ic = 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))