Don MacInnes has

recently been trying to understand the notion of "the" free category with X over a given category. Here X is supposed to be something like "finite limits" or "natural number object" or "cartesian closed structure" or combinations of similar properties.

One way of presenting such things is by means of 2-monads, and I expect that there will be an Australian response on these lines. Another is to use syntax. Given that most of the practical examples are categorical versions of syntax, this seems to me to be a perfectly natural way to proceed. I'm not going to write another long reply, but once again I would like to point you to my book, which seeks to make FLUENT translations between syntax and category theory. In particular, the so called "classifying category" of a type theory, which I call the "category of contexts and substitutions" by analogy with the names of familiar categories in pure mathematics, is constructed via an elementary sketch. This separates the recursive generation of the language from the associative composition, which as functional programmers know very well don't go very well together. The more difficult question is how to start off from a category, and build structure syntactically on top of it. Section 7.6 shows how to contruct the language from the category. Paul