On 25/05/09 3:03 PM, "John Baez" <john.c.baez@gmail.com> wrote:
Steve Lack writes:
You ask about a sketch for cartesian closed categories. Have a look at
at the paper "A presentation of topoi as algebraic relative to categories or graphs (Dubuc-Kelly, J. Alg. 81: 420-433, 1983). This describes something even tighter: the category of cartesian closed categories is monadic over the category of graphs.
Thanks!
And thanks to everyone else for their helpful comments. I'm behind on answering my emails.
In this approach, does each pair of objects in a ccc come with a chosen product and exponential? Are the morphisms of ccc's are required to preserve these on the nose?
Yes, that's right on both counts, but see below.
At first I was a bit shocked to hear of a sketch for ccc's, because the internal hom is contravariant in one variable. But I guess that as long as we treat ccc's purely 1-categorically that's no problem. But then I guess we pay the price of "undue strictness". Right?
As you say, if you work 1-categorically, you are stuck with undue strictness. And as you imply, there is an impediment to a fully 2-categorical approach because of the contravariance of the internal hom. But there is a way around this. You work 2-categorically, but not over the 2-category Cat, but over the 2-category of categories, functors, and natural _isomorphisms_. (Kelly & co call this 2-category Cat_g, with g presumably standing for groupoidal, since this is not just enriched in Cat but in groupoids.) Then the internal hom does indeed become a 2-functor Cat^2_g-->Cat_g. Having these invertible 2-cells now allows you to consider pseudomorphisms of algebras, which preserve structure up to isomorphism, thus alleviating the problem of undue strictness. It doesn't completely solve it - since we only have invertible 2-cells, we don't have a notion of lax morphism; or, more precisely, the notion of lax morphism we get is just that of pseudomorphism. Similarly, some constructions might not give what we hoped for. For example, the cotensor C^2 in Cat_g is not the category of arrows in C, it's the category of invertible arrows in C. All the best, Steve. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]