open import Cat.Diagram.Coproduct.Indexed
open import Cat.Instances.Sets.Complete
open import Cat.Diagram.Colimit.Finite
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Initial
open import Cat.Diagram.Pushout
open import Cat.Prelude

open import Data.Sum

module Cat.Instances.Sets.Cocomplete where


# Sets is cocompleteπ

open Initial


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 is given by the type 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 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 (the common codomain of all the is a set to eliminate from the truncation β by definition, canβt tell that might have had some extra paths we squashed away.

## Colimitsπ

Perfectly dually to the construction of limits in , 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 by the relation (generated by) identifying together all those points and whenever there exists a map such that

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

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

    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 was indexed by a set: The sum 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 from a path β using that they are in a set to eliminate from the truncation β to prove using the assumption that

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