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 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 simplex as a face in an 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.
よ-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)