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 C\mathcal{C} be a κ\kappa-small precategory. It, broadly speaking, will not be cocomplete. Suppose that we’re interested in passing from C\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 C=Δ\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][n+1][n]\to[n+1], exhibiting an nn-dimensional simplex as a face in an (n+1)(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:CDF : \mathcal{C} \to \mathcal{D} into a cocomplete category D\mathcal{D} factors as

CPSh(C)LanFD, \mathcal{C} {\xrightarrow{{よ}}} {{\mathrm{PSh}}}(\mathcal{C}) {\xrightarrow{\operatorname{Lan}_{よ}F}} \mathcal{D}\text{,}

where LanF\operatorname{Lan}_{よ}F is the left Kan extension of FF 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)