open import Cat.Diagram.Initial open import Cat.Prelude import Cat.Functor.Reasoning as Func import Cat.Morphism module Cat.Diagram.Colimit.Base where

# Ideaπ

Colimits are dual to limits limit; much like their cousins, they generalize constructions in several settings to arbitrary categories. A colimit (if it exists), is the βbest solutionβ to an βidentification problemβ. This is in contrast to the limit, which acts as a solution to an βequational problemβ.

# Constructionπ

Every concrete colimit (coproducts, coequalisers, initial objects) we have seen so far consists of roughly the same data. We begin with some collection of objects and morphisms, and then state that the colimit of that collection is some object with a universal property relating all of those objects and morphisms.

It would be convienent to be able to talk about *all* of these
situations at once, as opposed to on a case-by-case basis. To do this,
we need to introduce a bit of categorical machinery: the Cocone.

The first step is to generalize the βcollection of objects and morphismsβ involved. Luckily, this step involves no new ideas, just a change in perspective. We already have a way of describing a collection of objects and morphisms: itβs a category! As an example, the starting data of a coproduct is a pair of objects, which can be thought of as a very simple category, with only identity morphisms.

The next step also involves nothing more than a change in
perspective. Letβs denote our βdiagramβ category from earlier as
$J$.
Then, a means of picking out a
$J$
shaped figure in
$C$
isβ¦ a functor
$F : J \to C$!
Going back to the coproduct example, a functor from our 2 object
category into
$C$
selects 2 (not necessarily distinct!) objects in
$C$.
We this pair of category and functor a *diagram* in
$C$.

module _ {J : Precategory o β} {C : Precategory oβ² ββ²} (F : Functor J C) where private import Cat.Reasoning J as J import Cat.Reasoning C as C module F = Functor F record Cocone : Type (o β β β oβ² β ββ²) where no-eta-equality constructor cocone

Now, for the actual machinery! If we want to capture the essence of
all of our concrete examples of colimits, we a notion of an object
equipped with maps *from* every object in our diagram. We call
this designated object the βcoapexβ of the cocone.

field coapex : C.Ob Ο : (x : J.Ob) β C.Hom (F.β x) coapex

If our diagram consisted of only objects, we would be done! However, some diagrams contan non-identity morphisms, so we need to take those into account as well. This bit is best understood through the lens of the coequaliser: in order to describe the commuting condition there, we want every injection map from the codomain of a morphism to factor through that morphism.

commutes : β {x y} (f : J.Hom x y) β Ο y C.β F.β f β‘ Ο x

As per usual, we define a helper lemma charaterizing the path space of cones:

open Cocone Cocone-path : {x y : Cocone} β (p : coapex x β‘ coapex y) β (β o β PathP (Ξ» i β C.Hom (F.β o) (p i)) (Ο x o) (Ο y o)) β x β‘ y Cocone-path p q i .coapex = p i Cocone-path p q i .Ο o = q o i Cocone-path {x = x} {y = y} p q i .commutes {x = a} {y = b} f = is-propβpathp (Ξ» i β C.Hom-set _ _ (q b i C.β F.β f) (q a i)) (x .commutes f) (y .commutes f) i

## Cocone Mapsπ

Now that weβve defined cocones, we need a way to figure out how to express universal properties. Like most things categorical, we begin by considering a βcocone morphismβ, which will give us a category that we can work within. The idea here is that a morphism of cocones is a morphism in $C$ between the coapicies, such that all of the injection maps commute.

record Cocone-hom (x y : Cocone) : Type (o β ββ²) where no-eta-equality constructor cocone-hom field hom : C.Hom (x .coapex) (y .coapex) commutes : β o β hom C.β x .Ο o β‘ y .Ο o

We define yet another helper lemma that describes the path space of cocone morphisms.

open Cocone-hom Cocone-hom-path : β {x y} {f g : Cocone-hom x y} β f .hom β‘ g .hom β f β‘ g Cocone-hom-path p i .hom = p i Cocone-hom-path {x = x} {y = y} {f = f} {g = g} p i .commutes o j = is-setβsquarep (Ξ» i j β C.Hom-set _ _) (Ξ» j β p j C.β x .Ο o) (f .commutes o) (g .commutes o) refl i j

Now, we can define the category of cocones over a given diagram:

Cocones : Precategory _ _ Cocones = cat where open Precategory compose : β {x y z} β Cocone-hom y z β Cocone-hom x y β Cocone-hom x z compose K L .hom = K .hom C.β L .hom compose {x = x} {y = y} {z = z} K L .commutes o = (K .hom C.β L .hom) C.β x .Ο o β‘β¨ C.pullr (L .commutes o) β©β‘ K .hom C.β y .Ο o β‘β¨ K .commutes o β©β‘ z .Ο o β cat : Precategory _ _ cat .Ob = Cocone cat .Hom = Cocone-hom cat .id = cocone-hom C.id (Ξ» _ β C.idl _) cat ._β_ = compose cat .idr f = Cocone-hom-path (C.idr (f .hom)) cat .idl f = Cocone-hom-path (C.idl (f .hom)) cat .assoc f g h = Cocone-hom-path (C.assoc (f .hom) (g .hom) (h .hom))

## Colimitsπ

We now have all of the machinery in place! What remains is the universal property, which expresses that a*particular*cocone is universal, in the sense that it has a

*unique*map to any other cocone. However, we already have something that captures this idea, itβs the initial object! This leads to the following terse definition: A colimit over a diagram is an initial object in the category of cocones over that diagram.

is-colimit : Cocone β Type _ is-colimit K = is-initial Cocones K Colimit : Type _ Colimit = Initial Cocones Colimit-apex : Colimit β C.Ob Colimit-apex x = coapex (Initial.bot x)

# Preservation of Colimitsπ

Because a cocone is a commutative diagram, any given functor $F : \ca{C} \to \ca{D}$ takes cocones in $\ca{C}$ to cocones in $\ca{D}$, as functors preserve commutative diagrams.

F-map-cocone : Cocone Dia β Cocone (F Fβ Dia) F-map-cocone x .Cocone.coapex = F.β (Cocone.coapex x) F-map-cocone x .Cocone.Ο f = F.β (Cocone.Ο x f) F-map-cocone x .Cocone.commutes {y = y} f = F.β (Cocone.Ο x y) D.β F .Fβ _ β‘β¨ F.collapse (Cocone.commutes x _) β©β‘ F.β (Cocone.Ο x _) β

Though functors must take cocones to cocones, they may not
necessarily take colimiting cocones to colimiting cocones! When a
functor does, we say that it *preserves* colimits.

Preserves-colimit : Cocone Dia β Type _ Preserves-colimit K = is-colimit Dia K β is-colimit (F Fβ Dia) (F-map-cocone K)

## Cocompletenessπ

A category is **cocomplete** if admits for limits of
arbitrary shape. However, in the presence of excluded middle, if a
category admits coproducts indexed by its class of morphisms, then it is
automatically [thin]. Since excluded middle is independent of type
theory, we can not prove that any non-thin categories have arbitrary
colimits.

Instead, categories are cocomplete *with respect to* a pair of
universes: A category is
**$(o, \ell)$-cocomplete**
if it has colimits for any diagram indexed by a precategory with objects
in
$\ty\ o$
and morphisms in
$\ty\ \ell$.

is-cocomplete : β {oc βc} o β β Precategory oc βc β Type _ is-cocomplete o β C = β {D : Precategory o β} (F : Functor D C) β Colimit F