<!--
```agda
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
```
-->

```agda
module Cat.Instances.Sets.Cocomplete where
```

# Sets is cocomplete

<!--
```agda
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.

[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]: Homotopy.Space.Circle.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 = 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`{.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 {ι} {κ} {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 $\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 \cD$ such
that $F(f)(x) = y$.

[quotient]: Data.Set.Coequaliser.html#quotients

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

<!--
```agda
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 $\ell$ admits them.

```agda
  Sets-initial : Initial (Sets ℓ)
  Sets-initial .bot = el! (Lift _ ⊥)
  Sets-initial .has⊥ _ .centre ()
  Sets-initial .has⊥ _ .paths _ = ext λ ()
```

Coproducts are given by disjoint sums:

```agda
  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.

```agda
  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$.

```agda
  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`{.Agda} is finitely cocomplete:

```agda
  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.

```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 .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 $\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 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 $\bot$ using the assumption that $i ≠ j$.

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