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

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:ISetsF : I \to \sets is given by the type F\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.

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\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 =  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 YY (the common codomain of all the fif_i) is a set to eliminate from the truncation — by definition, YY can’t tell that F\sum F might have had some extra paths we squashed away.


Perfectly dually to the construction of limits in Sets\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 {D = D} F = colim where
  module D = Precategory D
  module F = Functor F

  sum : Type _
  sum = Σ[ d  D.Ob ]  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\sum F by the relation (generated by) identifying together all those points (X,x)(X, x) and (Y,y)(Y, y) whenever there exists a map (XfY)D(X \xto{f} Y) \in \ca{D} such that F(f)(x)=yF(f)(x) = y.

  apex : Cocone F
  apex .coapex = (sum / rel) , squash
  apex .ψ x p = inc (x , p)
  apex .commutes f = funext  i  sym (quot (f , refl)))

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 FF; The family of maps ψ\psi respects the quotient essentially by definition.

  colim : Initial _
  colim .bot = apex
  colim .has⊥ other = contr map unique where
    map : Cocone-hom F apex other
    map .hom = Coeq-rec (other .coapex .is-tr)  { (x , p)  other .ψ x p })
                  λ { ((X , x) , (Y , y) , f , p) 
                      sym (happly (other .commutes f) x)  ap (other .ψ Y) p
    map .commutes o = refl

    unique :  x  map  x
    unique hom′ = Cocone-hom-path _
      (funext (Coeq-elim-prop  x  other .coapex .is-tr _ _)
                λ y  sym (happly (hom′ .commutes _) _)))

Coproducts are disjoint🔗

As a final lemma, we prove that coproducts in Sets\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 FiFFjF_i \to \sum F \ot 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 FF was indexed by a set: The sum F\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 _ g h path = funext go where abstract
      path′ : Path (∀ c  Σ  x   F x ))  c  _ , g c)  c  _ , h c)
      path′ i c = ∥-∥₀-elim {B = λ _  Σ (∣_∣  F)}
         x  Σ-is-hlevel 2 (I .is-tr)  x  F x .is-tr))
         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=ji = j from a path (i,)=(j,)\| (i,-) = (j,-) \| — using that they are in a set to eliminate from the truncation — to prove \bot using the assumption that iji ≠ j.

    coprod .different-images-are-disjoint i j i≠j os = contr map uniq where
      map : Σ[ i   F i  ] Σ  x  _)   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))