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


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)}
       β†’ (eps : βˆ€ j β†’ F Κ» j β†’ ∣ A ∣)
       β†’ (βˆ€ {x y} (f : D.Hom x y) β†’ βˆ€ Fx β†’ eps y (F.F₁ f Fx) ≑ eps x Fx)
       β†’ sum / rel
       β†’ ∣ A ∣
  univ {A} eps p =
      (Ξ» { (x , p) β†’ eps x p })
      (Ξ» { ((X , x) , (Y , y) , f , q) β†’ sym (p f x) βˆ™ ap (eps _) 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} eps p x = univ {A} eps (Ξ» f β†’ happly (p f)) x
  colim .factors eps p = refl
  colim .unique {A} eps p other q = funext Ξ» x β†’
      (Ξ» x β†’  A .is-tr (other x) (univ {A} eps (Ξ» f β†’ happly (p f)) x))
      (Ξ» x β†’ happly (q (x .fst)) (x .snd))

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