Dear John, Barr & Wells "Toposes, Triples and Theories", Section 4.4, give some examples of LE-sketches (= finite limit sketches) that includes sketches for the theories of finite limit categories and of elementary toposes. They don't include CCCs, but you should at least get the idea. The basic trick (corresponding to the logical one of Freyd's "essentially algebraic" theories) is to think of these theories as being given algebraically with some of the operators (e.g. composition, pairing) being partial and with domain of definition described by equations. You then introduce those domains of definitions as nodes in the sketch, with arrows, diagrams and cones constraining them to be finite limits in a way that corresponds to the equations. Incidentally, Palmgren and I recently came up with a new logical characterization of finite limit theories, using a logic of partial terms. It leads to a neat proof of the initial model theorem. However, I also believe there is a specific but non-obvious advantage of sketches over logical syntax in that sketches do not rely on having canonical finite limits. Suppose a sketch has two distinct nodes a and b, and manages to constrain them both to be finite limits of the same diagram. In a model, a and b can be interpreted as different objects (though, of course, they have to be isomorphic). Regards, Steve Vickers. John Baez wrote:
Dear Categorists -
Andrei Rodin pointed out this paper by Charles Wells:
http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf
I took a look. In section 4.1 it mentions that people have given a finite limits sketch for cartesian closed categories. I'm curious about how this works, Unfortunately the list of references given here is quite long. Can anyone help me find a reference on a sketch for CCC's?
Best, jb