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

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

# Free cocompletions🔗

Let $C$ be a $κ-small$ precategory. It, broadly speaking, will not be cocomplete. Suppose that we’re interested in passing from $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=Δ,$
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],$
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
$Δ.$

Universally embedding
$Δ$
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→D$
into a cocomplete category
$D$
factors as

where
$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)