module
  Cat.Functor.Hom.Cocompletion
    {κ o} (C : Precategory κ κ) (D : Precategory o κ)
    (colim : is-cocomplete κ κ D)
    where

Free cocompletions🔗

Let C\mathcal{C} be a κ\kappa-small precategory. It, broadly speaking, will not be cocomplete. Suppose that we’re interested in passing from C\mathcal{C} to a cocomplete category; How might we go about this in a universal way?

To substantiate this problem, it helps to picture a geometric case. We’ll take C=Δ\mathcal{C} = \Delta, the category of non-empty finite ordinals and monotonic functions. The objects and maps in this category satisfy equations which let us, broadly speaking, think of its objects as “abstract (higher-dimensional) triangles”, or simplices. For instance, there are (families) of maps [n]→[n+1][n]\to[n+1], exhibiting an nn-dimensional simplex as a face in an (n+1)(n+1)-dimensional simplex.

Now, this category does not have all colimits. For example, we should be able to the red and blue triangles in the diagram below to obtain a “square”, but you’ll find no such object in Δ\Delta.

Universally embedding Δ\Delta in a cocomplete category should then result in a “category of shapes built by gluing simplices”; Formally, these are called simplicial sets. It turns out that the Yoneda embedding satisfies the property we’re looking for: Any functor F:C→DF : \mathcal{C} \to \mathcal{D} into a cocomplete category D\mathcal{D} factors as

C→よPSh(C)→Lan⁡よFD, \mathcal{C} \xrightarrow{よ} \mathrm{PSh}(\mathcal{C}) \xrightarrow{\operatorname{Lan}_よ F} \mathcal{D}\text{,}

where Lan⁡よF\operatorname{Lan}_よ F is the left Kan extension of FF along the Yoneda embedding, and furthermore this extension preserves colimits. While this may sound like a lot to prove, it turns out that the tide has already risen above it: Everything claimed above follows from the general theory of Kan extensions.

よ-extension : (F : Functor C D) → Lan (よ C) F
よ-extension F = cocomplete→lan (よ C) F colim

extend-factors : (F : Functor C D) → (よ-extension F .Lan.Ext F∘ よ C) ≅ F
extend-factors F = ff→cocomplete-lan-ext (よ C) F colim (よ-is-fully-faithful C)