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

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

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)