open import Cat.Functor.Kan.Pointwise
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Functor
open import Cat.Functor.Kan.Base
open import Cat.Functor.Hom
open import Cat.Prelude

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 $\mathcal{C}$ be a $\kappa \text{-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 \text{,}$ 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]\text{,}$ exhibiting an $n\text{-dimensional}$ simplex as a face in an $(n+1)\text{-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 \text{.}$

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

where ${\mathrm{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)