That is carried out (rather sketchily :)) on page 48 of Graph Based Logic and Sketches by Bagchi and Wells, here: http://arxiv.org/PS_cache/arxiv/pdf/0809/0809.3023v1.pdf This post http://sixwingedseraph.wordpress.com/2009/05/08/turning-definitions-into-mat... is the first of a projected series to explain the Bagchi-Wells paper in a more how-to-think-about-it style. Charles Wells On Thu, May 21, 2009 at 2:43 PM, John Baez <john.c.baez@gmail.com> 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

I have not kept up with the field very well, but I can recommend these works: Peter Johnstone, *Sketches of an Elephant*, Vol. 2, OUP 2003: the chapter on sketches. (I am in rural Wisconsin at the moment asnd don't have access to the book. If OUP would make its pages available to look at on Amazon I could have told you the exact page.) Bagchi and Wells, *Graph Based Logic and Sketches*, here: http://arxiv.org/PS_cache/arxiv/pdf/0809/0809.3023v1.pdf Also Kinoshita, et al 1997, referred to in GBLS. There might be relevant papers since 1993 mentioned in the Elephant, too. Category people: If you can suggest other papers that should be included, let me know soon, and I will revise the sketches paper to include them (and the ones I mentioned above). Charles Wells On Wed, May 20, 2009 at 4:23 PM, <Andre.Rodin@ens.fr> wrote:

Dear Charles and others:

this

http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf

is your very useful overview of Sketch theory dated back to 1993. I wonder how much it omits today: are there significant research programmes in this field emerged during last 15 years? What should I look at first of all? Many thanks in advance.

Andrei

Dear Andrei, Speaking about research programmes, Makkai's generalized sketches should definitely be mentioned. An easy introduction can be found in A Diagrammatic Logic for Object-Oriented Visual Modeling Zinovy Diskin and Uwe Wolter DOI Bookmark: 10.1016/j.entcs.2008.10.041 It provides references to Makkai's papers and some other sources, and briefly describes some history and motivations. You may skip all sentiments about engineering applications, or do just the opposite -- pay attention to them -- at least, this is what granting agencies like. There are two distinctions from Makkai's sketches: a signature of diagram predicates is a category rather than a set, and semantics is given in terms of functors into sketches rather than from them. ZD 2009/5/20 Andre.Rodin <Andre.Rodin@ens.fr>:

Dear Charles and others:

this

http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf

is your very useful overview of Sketch theory dated back to 1993. I wonder how much it omits today: are there significant research programmes in this field emerged during last 15 years? What should I look at first of all? Many thanks in advance.

Andrei

Let me make a few clarifying remarks On Fri, May 22, 2009 at 8:44 PM, <Andre.Rodin@ens.fr> wrote:

I came across this recent paper by Diskin&Wolter

http://www.cs.toronto.edu/~zdiskin/Pubs/ACCAT-07.pdf

where the authors propose a version of sketch-based syntax for Computer Science purposes. The main idea here (as far as I understood the paper) is to use sketches as arities of predicates. I heard about similar ideas from Rene Guitart in private conversations (but Rene's approach is algebraic rather than logical).

our version of sketches is intended for use in software engineering, not only in computer science. The difference between them is like the difference between, say, electrical engineering and physics. Predicate arities may be objects of any a priori chosen good category, e.g., sketches built in a previous step, but this is not the main idea. Relation of Makkai's generalized sketches to classical sketches is, roughly, like relation of a general first-order theory a la Tarski to a particular family of theories like, e.g., lattice theory. The former provide a general framework, in which the user can define any theory she likes. The latter is a family of particular instantiations of the framework. The fact that this family is expressive enough to specify any structure is another story. A first-order signature contains operation and predicate symbols. Similarly, a generalized sketch signature may contain operation symbols too (whose arities are In-Out spans). Definitions and some details can be found in Report referenced as [6] in the paper above. ZD Looking at GBLS briefly I couldn't immediately grasp if your and

Atish Bagchi's approach to graph-based logic is based on similar ideas or your approach is quite different. I certainly should read GBLS more carefully for discussing it but I would grateful for a hint.

Andrei

Selon Charles Wells <charles@abstractmath.org>:

...

I have not kept up with the field very well, but I can recommend these works:

Peter Johnstone, *Sketches of an Elephant*, Vol. 2, OUP 2003: the chapter on sketches.  (I am in rural Wisconsin at the moment asnd don't have access to the book.  If OUP would make its pages available to look at on Amazon I could have told you the exact page.)

Bagchi and Wells, *Graph Based Logic and Sketches*, here:

http://arxiv.org/PS_cache/arxiv/pdf/0809/0809.3023v1.pdf

Also Kinoshita, et al 1997, referred to in GBLS.  There might be relevant papers since 1993 mentioned in the Elephant, too.

Category people:  If you can suggest other papers that should be included, let me know soon, and I will revise the sketches paper to include them (and the ones I mentioned above).

Charles Wells

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/ ]