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 be a -small precategory. It, broadly speaking, will not be cocomplete. Suppose that we’re interested in passing from 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 , 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 , exhibiting an -dimensional simplex as a face in an -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 into a cocomplete category factors as
where is the left Kan extension of 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)