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

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.

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$) 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 $\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 $\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 \ca{D}$ such that $F(f)(x) = y$.

apex : Cocone F apex .coapex = el (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 $F$; 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$,
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 \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 $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 _ 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 → 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 $\| (i,-) = (j,-) \|$ — using that they are in a set to eliminate from the truncation — to prove $\bot$ using the assumption that $i ≠ 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))