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.
Colimitsπ
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} {D = 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.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 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.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 = Coeq-rec (A .is-tr) (Ξ» { (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 β Coeq-elim-prop (Ξ» x β A .is-tr (other x) (univ {A} eps (Ξ» f β happly (p f)) x)) (Ξ» x β happly (q (x .fst)) (x .snd)) x
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 _ 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 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 : Ξ£[ 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))