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 be a 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 simplex category. 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 simplex as a face in an simplex.
Now, this category does not have all colimits. For example, we should be able to glue 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.
よ-extension : (F : Functor C D) → Lan (よ C) F よ-extension F = cocomplete→lan (よ C) F colim よ-extension-cocontinuous : ∀ {o' κ' F} → is-cocontinuous o' κ' (よ-extension F .Lan.Ext) よ-extension-cocontinuous = left-adjoint-is-cocontinuous (Realisation⊣Nerve _ colim) よ-extension-extends : (F : Functor C D) → よ-extension F .Lan.Ext F∘ よ C ≅ F よ-extension-extends F = ff→cocomplete-lan-ext (よ C) F colim (よ-is-fully-faithful C)