show/hide this revision's text 2 LaTeXiFiCaTiOn

There are general results about how to freely add limits or colimits to a category. They are formally dual, but people normally state the colimit variety because they involve the category of presheaves.

To freely add some class of colimits to a given category C, $C$, you form the closure of the representables in the presheaf category [C^op,Set] $[C^{op},\mathsf{Set}]$ under the given type of colimit.

If you want to do this in such a way that certain existing colimits are preserved, then you form the closure not in the presheaf category, but in the full subcategory of those presheaves which send the existing colimits in C into limits in Set.

So to freely complete a category C $C$ with finite products to a category with finite limits, you should look at the Yoneda embedding of C $C$ into the opposite FP(C,Set)^op $FP(C,Set)^{op}$ of the category FP(C,Set) $FP(C,\mathsf{Set})$ of finite-product-preserving functors from C $C$ to Set. $\mathsf{Set}$. Now take the closure of the representables under finite limits. That is, finite limits in FP(C,Set)^op, $FP(C,\mathsf{Set})^{op}$, or finite colimits in FP(C,Set). $FP(C,\mathsf{Set})$. This then gives the value at C $C$ of a left biadjoint to the forgetful 2-functor from the 2-category LEX of categories with finite limits to the 2-category FP of categories with finite products.

There is an explicit, syntactic description, due to Andy Pitts. It can be found, for example, in the paper

M. Bunge and A. Carboni, The symmetric topos, Journal of Pure and Applied Algebra, 1995.

An object is a pair of maps f,f':X-->X' $f,f':X \to X'$ equipped with a common retraction r. $r$. A morphism from such a pair to g,g':Y-->Y',s $g,g':Y \to Y',s$ consists of an equivalence class, under a suitably defined equivalence relation, of pairs (a,a') $(a,a')$ where a:X-->Y$a:X \to Y$, a':X'-->Y'$a':X'\to Y'$, and the evident diagrams commute.

show/hide this revision's text 1

There are general results about how to freely add limits or colimits to a category. They are formally dual, but people normally state the colimit variety because they involve the category of presheaves.

To freely add some class of colimits to a given category C, you form the closure of the representables in the presheaf category [C^op,Set] under the given type of colimit.

If you want to do this in such a way that certain existing colimits are preserved, then you form the closure not in the presheaf category, but in the full subcategory of those presheaves which send the existing colimits in C into limits in Set.

So to freely complete a category C with finite products to a category with finite limits, you should look at the Yoneda embedding of C into the opposite FP(C,Set)^op of the category FP(C,Set) of finite-product-preserving functors from C to Set. Now take the closure of the representables under finite limits. That is, finite limits in FP(C,Set)^op, or finite colimits in FP(C,Set). This then gives the value at C of a left biadjoint to the forgetful 2-functor from the 2-category LEX of categories with finite limits to the 2-category FP of categories with finite products.

There is an explicit, syntactic description, due to Andy Pitts. It can be found, for example, in the paper

M. Bunge and A. Carboni, The symmetric topos, Journal of Pure and Applied Algebra, 1995.

An object is a pair of maps f,f':X-->X' equipped with a common retraction r. A morphism from such a pair to g,g':Y-->Y',s consists of an equivalence class, under a suitably defined equivalence relation, of pairs (a,a') where a:X-->Y, a':X'-->Y', and the evident diagrams commute.