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)