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 $F:I\to \mathbf{Sets}$ is given by the type $\sum F\text{.}$ 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\text{)}$ 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} {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\stackrel{f}{\to }Y)\in \mathcal{D}$ such that $F(f)(x)=y\text{.}$

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\text{;}$ The family of maps $\psi$ 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 $\ell$ 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 
  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\text{.}$

  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 
  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 $\mathbf{Sets}\text{,}$ 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\text{.}$

    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.

    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 )
        (λ 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 $\Vert (i,-)=(j,-)\Vert$ — using that they are in a set to eliminate from the truncation — to prove $\perp$ using the assumption that $i\ne j\text{.}$

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