Dear Alexandru, I would recommend the paper "Partial Horn logic and cartesian categories" that I wrote with Eric Palmgren (Annals of Pure and Applied Logic 145 (3) (2007), pp. 314 - 353; doi:10.1016/j.apal.2006.10.001). Free categories of various kinds usually do exist, an idea that comes out well in Higgins's 1971 "Notes on categories and groupoids" (now reissued as a TAC reprint). The underlying machinery, again recognized for a long time, relies on the notion of left exact theories, alias finite limit theories, cartesian theories or essentially algebraic theories. In the formulation as an essentially algebraic theory, the operators may be partial but their domains of definition can be expressed in terms of equations using operators defined "earlier" (i.e. there is an ordering on the operators). For categories, the core example is composition, which is partial and defined when an equation holds between the domain of one morphism and the codomain of the other. But the same phenomenon arises, for example, when adding morphisms in an Abelian enriched category or composing 2-cells in a 2-category. The fundamental result for left exact theories is that a forgetful functor, from a category of algebras for one theory to that for another with fewer operators (or fewer equations, for that matter), has a left adjoint. I believe the result is covered in chapter 4 Barr and Wells' "Toposes, Triples and Theories", or at least is inferrable from Kennison's Theorem as stated there. Palmgren and I proved the fundamental freeness result (our Theorem 29, Free Partial Model Theorem) in a way that makes much clearer the connection with the well known result for algebraic theories. (For algebraic theories, with all operators total, you just take a term model and factor out a congruence.) We used a logic, minimally adapted from the standard account of categorical logic as in the Elephant, in which terms are only partially defined. We also described a simple "quasi-equational" mode of theory presentation equivalent to left exact theories. The proof is then very similar to the algebraic case, taking a partial term model and factoring out a partial congruence. It is also more elementary than that in TTT. I hope this will answer your question in most cases. Strictness is an issue, as you mention. Our treatment is very syntactic in nature, and expects strictness of homomorphisms. However, we do have techniques that allow this to be relaxed - see our Theorem 56. We also give various examples from category theory, as well as discussing some of the history of the result. Regards, Steve Vickers. Michael Barr wrote:
From: Alexandru Chirvasitu <chirvasitua@gmail.com>
Dear Prof. Barr,
... Unfortunately, I couldn't find any results stating clearly (clearly for someone who is perhaps not *too* familiar with the higher categorical machinery) that such free categories always exist. Of course, the few constructions I needed can easily be done by hand, but what I had in mind was some kind of higher categorical analogue of the fact that the forgetful functor from a variety of algebras to another variety of algebras with "fewer operations" has a left adjoint.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]