open import Cat.Functor.Adjoint.Continuous open import Cat.Diagram.Colimit.Base open import Cat.Functor.Kan.Nerve open import Cat.Instances.Functor open import Cat.Functor.Hom open import Cat.Functor.Kan open import Cat.Prelude module Cat.Functor.Hom.Cocompletion {κ o} (C : Precategory κ κ) (D : Precategory o κ) (colim : is-cocomplete κ κ D) where

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

extend : Functor C D → Functor (PSh κ C) D extend F = Realisation colim F extend-cocontinuous : ∀ {od ℓd} {J : Precategory od ℓd} {Dg : Functor J (PSh κ C)} (F : Functor C D) → Colimit Dg → Colimit (extend F F∘ Dg) extend-cocontinuous F = left-adjoint-colimit (Realisation⊣Nerve colim F) extend-factors : (F : Functor C D) → (extend F F∘ よ C) ≅ F extend-factors F = ff-lan-ext colim (よ C) F (よ-is-fully-faithful C)