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

private module C = Cat.Reasoning C module D = Cat.Reasoning D open import Cat.Morphism Cat[ C , D ] using (_≅_) open Func open _=>_

# Free cocompletions🔗

Let $\mathcal{C}$ be a $\kappa$-small precategory. It, broadly speaking, will not be cocomplete. Suppose that we’re interested in passing from $\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
$\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]\to[n+1]$,
exhibiting an
$n$-dimensional
simplex as a face in an
$(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 : \mathcal{C} \to \mathcal{D}$
into a cocomplete category
$\mathcal{D}$
factors as

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

where
$\operatorname{Lan}_よ F$
is the left Kan extension of
$F$
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)