An Introduction to Forms
9 May 2014
Charles (at) abstractmath.org
Introduction
A form is a kind of generalized sketch that I introduced in [GenSk]. The most detailed description of forms is in [GBLS]. Reading this introduction might help you work your way through that paper.
A sketch (invented fifty years ago by Charles Ehresmann) is a mathematical structure designed for specifying a type of mathematical structure. Sketches are described briefly here and in detail in references [CTCS] and [TTT]. A form is an abstraction of the concept of sketch. Forms also specify kinds of mathematical structures, and they can specify more kinds of structures than sketches can [LimSk]. In a sense, a form is a kind of sketch of a sketch.
I will sneak up on the idea of sketch using the specification of directed graphs as an example.
Directed
graphs
This picture shows a directed graph. A graph theorist might call it a directed multigraph with loops.
What makes it a directed graph is that it has some nodes (x, y, z and w in this case), some arrows (a, b, c, d, e, u), and each arrow has a source and a target; for example, the source of c is z and its target is x. That information completely determines the structure of a directed graph.
The picture has lots of extraneous information irrelevant to the structure, for example the placement of the nodes. This extraneous data may make it easier to see the structure but is not part of the structure of the directed graph itself.
You can denote the set of positive divisors of 7 by {1,7} or by {7,1}; in either case it is the set whose elements are exactly 1 and 7 and nothing else. Whether the 1 or the 7 comes first inside the braces is not relevant. It is interesting that most notation systems for mathematical object has properties that are irrelevant to the structure denoted -- even the notation for a two-element set. This introduces noise in the required pattern recognition process.
The statement in blue above is an informal definition of "directed graph" written in mathematical English. This definition determines a type of mathematical structure. You could go on and say that a morphism of directed graphs must take nodes to nodes, arrows to arrows, and preserve source and target. For example, a morphism f from the directed graph in the picture to some other directed graph must satisfy the requirements that the source of f(c) must be f(z) and the target must be f(x). Thus the two statements in blue define a category of directed graphs.
There are other ways to define morphism of directed graphs; for example, you can allow an arrow to go to a node. That category of directed graphs can also be sketched. So can undirected graphs. [GMG] gives a survey of these concepts.
About definitions
The definitions in blue require experience in reading mathematical prose and fairly sophisticated pattern-recognition to determine that they are definitions and to determine just what requirements they impose for an object to be a directed graph. This is discussed in detail in abstractmath.org.
Both the definitions in blue could be made more formal. They could be clearly marked as definitions and the example remarks could be segregated into another paragraph. For example:
Definition. A directed graph consists of two
sets A, whose elements are called arrows, and N, whose
elements are called nodes, and two functions 
This formal definition is still a piece of mathematical English. It still requires pattern recognition to extract the mathematical content. But what is the mathematical content of a definition? Both mathematical logic and sketch theory provide (different) answers to this question: Both provide a mathematical object that determines a type of structure.
First-order theories
A first-order theory is a mathematical structure that specifies a type of mathematical structure. It provides a mathematically defined system of symbols, expressions and formulas that determine a type of structure, along with a set of rules that determine which sets-with-structure are of the desired type, in other words are models. The expressions and formulas are strings of symbols defined recursively and subject to axioms.
As an example, the theory for directed graphs could contain two types (node, arrow), a set of variables of each type, two unary function symbols s and t, and some production rules such as: "If a is of type arrow, then s(a) is a well formed term of type node." (You could also use a single-sorted theory, with predicates that say whether an object is a node or an arrow.) A model of this theory (in the category of sets) must consist of two sets and two functions between them.
This theory is a mathematical object. The fact that first-order theories and their models are math objects allows you to prove theorems such as the Löwenheim-Skolem Theorem (every finitary first order theory that has an infinitary model has non-isomorphic models, which is where you get non-standard integers).
The
details about first order theories are spelled out in the Stanford encyclopedia entry. Wikipedia has a
list of first order theories of common structures such as
groups and (undirected) graphs.
A first order theory could be described as a mathematical object consisting of strings of symbols subject to certain axioms, along with rules describing what models must be. Thus it takes a formal definition in Mathematical English, such as the definition of directed graph given above, and models it as strings, in the same way we might model the flight of a cannonball as a parabola. (This is a different use of the word "model" from the meaning of model of a first order theory. Abstractmath.org has a discussion about the various uses of the word "model".)
Because of this, it makes sense to say that a first order theory is a string-based specification of a type of math structure.
Sketches
A sketch
is a graph-based specification of a type of mathematical
structure. The sketch for directed graphs is shown at the right. It
is itself a graph, which is confusing. Get used to it.
A model M of this sketch in a category 
Thus a model in the category of sets is both of these things:
· A particular directed graph.
· A functor from the sketch to the category of sets.
A functor from a directed graph into a category is defined in the same way as a functor from a category into a category, except that there are no composites or identities to preserve.
A morphism of models of this sketch from 
If you chase these diagrams you will discover that they say both these things:
That is a start on understanding sketches: Models are functors and morphisms between models are natural transformations.
Specifying more kinds of structure
Groups, small categories, fields and many other structures
are models of sketches. To show how that happens, I have to say
how to sketch binary operations (to define groups), how to impose
equations (to state the associative law), how to define equalizers (so I
can say how to define composition when the domain of one morphism equals the
codomain of another) , "not equals" (so I can say 
We can go further and sketch special kinds of categories (cartesian closed, toposes, and others) which we will need to do to create forms with more power than sketches.
The sketch for an endofunction
Let 
be the graph above. It has one node c and
one arrow s, whose source and target are (necessarily) c. A model
of this sketch is a set C and a function from C to itself. Any
such function determines a cyclic semigroup of transformations of C.
One particular model is the one in which in which C is the set of
natural numbers and s is the successor function: this is the free semigroup on
one letter.
You may want to experiment with other graphs as sketches. Any graph produces a category of models in sets. Each such category is a category of presheaves, hence is a topos ([TTT], p. 67, Theorem 2.4).
Imposing equations
We need to expand the idea of sketch to be able to define
more kinds of structure. Let’s start with equations.
Suppose we take the sketch for an endofunction and want to modify it so that 
in every model in Set.
This means we must require that the diagram (in the category of sets) below
commute for every model M.
To say that this diagram is commutative (or commutes)
requires that 
.
· This use of the word "commutative" is distinct from the meaning of the word in algebra.
· Saying exactly what “this diagram is commutative” means for any particular diagram requires fussiness. Chapter 2 of [GBLS] goes into excruciating detail about this.
The obvious way to do this is to say that we require a model
to be a functor from the graph to the category of sets that has the property
that the image of the diagram
under M is a commutative diagram in the category of sets. We say that this diagram is formally commutative. In general, in sketch theory, something is formally P if in every model of the sketch its image is required to be P.
To say that the diagram itself is commutative is meaningless. It is a diagram in a graph, which has no notion of composition of arrows.
This gives us a more general notion of sketch
which allows the specification of equations, although so far only between unary
operations. Formally, a linear sketch 
consists of a graph G
together with a set 
of zero or more
formally commutative diagrams. It should be apparent that an linear sketch can
specify anything that a universal algebra signature with only unary operations
can specify.
Models in arbitrary categories
A model in Set of a linear sketch 
is a graph morphism 
with the property that
M takes every diagram in D to a
commutative diagram in Set.
This definition would still
be meaningful if we replaced 
by any category
whatever. So now we can talk about a model of 
in any category C.
For example, a model in the category of groups of the endofunction sketch above
that requires the cube to be the identity function is simply a group with a
specified automorphism of order 1 or 3. Indeed, in any category of structures
of a certain type, a model is a structure of that type with a specified
automorphism of order 1 or 3.
The more elaborate sketches we construct later will still allow models in any category. For example, a model of the sketch for groups (see [TTT] starting on page 126) in the category of Hausdorff spaces is precisely a Hausdorff topological group.
Ancient cute theorem: A model of the sketch for groups in the category of groups is an Abelian group. That’s because the group operations must be homomorphisms!
Clones and theories
Sketches as I have described them so far can now describe some kinds of universal algebras, namely those with unary operations and equations. n-ary operations and more elaborate constructions will come later.
The first big construction in universal algebra is that of the clone of a type of algebra (commonly called a signature): a specific set of n-ary operations for various n and specific equations involving those operations. The clone is essentially all the expressions you can create from the operations, requiring two expressions to be equivalent if you can prove they are equivalent given the equations of the algebra.
For example, in the clone for groups, x(y(xy)) is equivalent to (xy)(xy). On the other hand, xy is not equivalent to yx because there are noncommutative groups, so xy = yx can’t possibly follow from the equations.
The Lawvere theory of the algebra is a different construction which essentially expresses the clone as a special kind of category, with models of the theory being product-preserving functors.
In model theory a first-order theory is an extension of the concept of clone that allows relations other than equality, as well as the use of negation and quantifiers. First order theories are constructed in a different way from clones and Lawvere theories but they capture the same general idea in the bigger context.
The cattheory of a sketch
For a sketch, the idea equivalent to the clones and theories just described is that of a cattheory. (This is a new coinage. See Terminology below.)
Suppose we have a linear sketch 
where G is a graph
and D is a set of formally
commutative diagrams. The cattheory of the linear sketch,
denoted by 
, is the free
category generated by G with the condition imposed that the
diagrams in D must become commutative. The graph morphism 
that takes the nodes
and arrows in G to the corresponding objects and arrows of the free
category is by definition a model of the sketch 
. G is called the generic model of the sketch.
A model of the cattheory in a category 
is simply a functor 
. We don’t have to impose properties on the functor
because functors automatically preserve commutative diagrams. When we get
into more complicated structures we will have to add preservation requirements
on the model functor.
The category of models of the linear sketch in a category is denoted by 
. The category of models of the cattheory in is denoted by 
. By definition of
"free", any model 
induces a unique model
for which 
.
I defined a model of in as a graph morphism 
, but in the previous paragraph I referred to a model . This is the standard
abuse of notation
used everywhere in math: Deliberately not distinguishing a structure from its
underlying set. (See "abuse of
notation" in Wikipedia
and in [Hbk].)
The cattheory has this universal property:
Theorem The map 
is an equivalence of categories.
This theorem forces the cattheory to be determined up to natural equivalence of categories that commutes with the generic model. For all practical purposes, a model of the sketch is thus the same thing as a model of its cattheory. This will remain true as we go up the hierarchy of new constructions (n-ary operations, limits and colimits, and other things) and is the defining property of the cattheory. Clones, Lawvere theories and first order theories are all cattheories up to equivalence.
How to think about cattheories
may be thought
of as the minimal category that contains a model of , the model being the generic model G. Every model
M of in any category must induce a unique
(up to natural isomorphism) model of in , simply because everything in must be there because
any category containing a model of must have everything in .
For example, consider the sketch for endofunctions above.
Because s is in the graph of the sketch, every power of M(s)
must be in any category containing a model M
of the sketch. This forces by induction a unique functor M' from the cattheory of the sketch to 
(Usually the induced functor is unique only up to natural
isomorphism, but this time it is rilly rilly unique.)
Terminology
The remarks in this section apply in general to all kinds of sketches, not just the restricted version we are considering here.
The situation in the literature is confusing.
- In [TTT] and in the other books and articles by Michael Barr and/or me, we call the cattheory the theory.
- In [GBLS], Atish Bagchi and I refer to the cattheory of a finite limit sketch as a theory or as a categorial theory in an attempt to distinguish it from some version or other of logical theory. We said “categorial theory” instead of “categorical theory” because the latter phrase means something different to logicians. Unfortunately, “categorial” means something different to linguists!
- In [SkEl], Johnstone calls the cattheory of a sketch the syntactic category.
- In [GBLS], page 33, we refer to SynCat[ f ], where f is a form (generalized sketch). Now f has a cattheory, but it is not SynCat[ f ], which is the cattheory correspond to the doctrine that f belongs to (the type of categories it can have models in.)
I am using “cattheory” so that I will have a neologism that doesn’t mean anything different to anybody. Personally, I think we should keep using “theory”, because the theory (syntactic category in the sense of Johnstone) is ultimately the same thing (satisfies the same universal property) as the corresponding logical theory; the difference is only in the construction.
Products
A (binary) product diagram in a category is a cone to {a,b}, in other words a diagram that looks like this
(1)
with this specific universal property:
For any other cone to {a,b}, 
(2)
there is a unique fill-in arrow fi such that this diagram commutes:
(3)
This diagram has been called a sawhorse. But like most metaphors in math, this name is misleading.
How to think about the sawhorse
- The sawhorse is not symmetrical with respect to its two pairs of legs. The black (right) legs form a product cone but the blue (left) legs need not be a product diagram. It could be called a directed sawhorse.
- The construction of the
fill-in arrow is like an algebraic operation whose domain is the set of
diagrams of the form (2) for a fixed product diagram (1) and whose
output is the fill-in arrow. Now ordinary algebraic operations
have domain some cartesian product of sets with output in a set. For
example scalar multiplication of a real vector space is an operation
. The fill-in arrow is an operation on a set of tuples of arrows, but the domain
is not the cartesian products of arrow sets; instead it is an equationally
defined subset of a cartesian product of arrow sets (the equation says
that the source of one must match the product of the other). - The colors in the sawhorse correspond to the quantifiers in the definition of the diagram: Given a cone from x to {a, b}, then for any other cone from any object y to {a,b}, there is a unique fill-in arrow fi from a to b such that the sawhorse commutes.
- By making the blue cone also a product diagram you get an instant proof that the resulting fi is an isomorphism, in fact the only isomorphism making the sawhorse commute. Thus "products in a category are determined up to a unique isomorphism".
Chapter 5 of [CTCS] gives a detailed explanation of products in categories at a rather elementary level.
Finite products
Finite products 
A category has finite products if there is a product diagram for any finite set of objects.
FP sketches
An FP sketch is a graph together with some
specified formally commutative diagrams and some specified formal product
diagrams. A model of an FP sketch in a category is a functor from the graph to that takes the specified formally
commutative diagrams to commutative diagrams and the specified formal product
diagrams to product diagrams.
The category of all algebras for any specified type of universal algebra (with finitary operations) is equivalant to the category of models of an FP sketch. Chapter 4 of [TTT] describes an FP sketch for the category of groups starting on page 126.
On the nose
The homomorphisms in the category of models of an FP sketch
must preserve the designated product diagrams on the nose. For example, the sketch for groups just
mentioned has three designated formal product cones, for the terminal object,
for 
and for 
. The formal binary operation is an arrow 
. "On the
nose" means that in a model the binary operation must have domain the exact copy of 
that is the value of
the model at . This is just a technicality, although some mathematicians make a big deal
out of it. In fact when mathematicians talk about the “category of
groups” they never say which product
cone they mean by and .
Finite Limits
Review: a cone
to a set 
of objects of a category consists of an
object v of the category and one arrow from v to each object in 
.
A finite-product diagram is a cone to such a (finite) set with the unique fill-in property.
Now suppose we have a finite diagram 
in a category. I am specifically
not assuming it is commutative. A commutative cone to is an object v, an arrow(called
a projection) from v to each node of ,
with the additional property that each triangle formed by two projections and
an arrow of the diagram must commute. The diagram is called the base diagram of
the cone.
Example
Here is an example of a base diagram:
(a)
A commutative cone over this base will look like the left diagram below. The three arrows with source P are the projections.
Since the triangles involving two projections have to commute, the diagonal
projection is determined by the other two. For this reason, this
particular example is almost always drawn as on the right. It is called a pullback diagram.
Two other examples
In each case all the projections are shown on the left and only the necessary ones on the right.
(b)
(c)
Limit cones
A limit cone over a diagram is a commutative cone over the diagram with the same unique-fill-in property that product cones have. For example if this is a limit cone over diagram (a) above
(d)
and the blue arrows on the left below also form a
commutative cone over the same base, then there must be a unique fill-in arrow making everything commute in the
diagram on the right.
This particular shape (d) of limit cone is called a pullback diagram. A limit cone in the shape of (b) is an equalizer diagram. It turns out that if you assume that if all pullbacks and equalizers exist, then you have limit cones over every finite diagram for free. Limit cones of shape (c) don’t have a common name but they will be referred to later.
Since a finite set of objects is just a finite diagram with no arrows, product diagrams are a special case of limit diagrams. The commutativity requirement is then vacuous.
A category has all finite limits is called an FL-category. From the remark in the previous paragraph,
an FP-category is automatically an FL-category; the
diagrams in have nodes but no arrows.
An older name, which is deprecated, is left exact category.
FL-Sketches
An FL sketch (finite-limit sketch) is a finite graph 
with a finite set 
of finite formally
commutative diagrams and a finite set of formal limit cones over
finite diagrams (which are not usually among the formally commutative
diagrams.)
A model of an FL sketch in an FL category is a graph map into
the (underlying graph of) the FL category that take the diagrams in to commutative cones
and the cones in 
to limit cones.
The category of models of the FL sketch in an FL category is denoted by 
.
FL cattheories
The FL cattheory of a linear sketch is a category 
together with a model 
with the the property
that for any model 
of in a category , there is a unique model M' of in such that
commutes. G is the generic model of .
The category of models of the cattheory in is denoted by 
.
The cattheory has this universal property:
Theorem The map 
is an equivalence of categories.
(Compare the corresponding theorem for linear categories.)
This theorem forces the cattheory to be determined up to natural equivalence of categories that commutes with the generic model. For all practical purposes, a model of the sketch is thus the same thing as a model of its cattheory.
FL-sketches and forms
The first key to understanding forms is that all sorts of
interesting kinds of categories (cartesian closed, toposes, symmetric monoidal)
are models of FL-sketches. Indeed, I expect (but haven't proved) that
every kind of n-category that anyone ever defined is a model of an
FL-sketch
Constructing FL cattheories
The linear cattheory of a linear sketch is just the free category generated by the graph of the sketch, with the formally commutative diagrams forced to be commutative. It is more complicated to prove the existence of the FL cattheory of an FL sketch. Once you do show it exists, it follows easily from the definition that it is uniquely determined up to equivalence of categories.
There are two approaches to showing the existence of the FL cattheory.
As a fixed point
Introduce an operator on categories that adjoins diagrams
that in effect add limit cones to finite diagrams that don’t already have
limits. This is done in lots of detail in sections 4.2 and 4.3 of [GLBS]. Starting with an FL-sketch , the cattheory is the minimum fixpoint of this operator.
This is the computer-sciencey way of doing it. Each arrow and commutative diagram in the theory is constructed explicitly. When [GLBS] constructs proofs, this step-by-step construction corresponds to the inductive construction of formulas and rules of inference in classical string-based logic.
Embedded in a functor category
Given an FL sketch , the category 
of models of in the category of sets turns out to be
a full reflective subcategory of the presheaf
category 
.
Let’s spell out what this means: the models are
finite-limit-preserving functors and the presheaf category contains all
functors. The reflectivity means that the embedding has a left adjoint,
which implies that a limit of a diagram in the model category is also the limit
of the diagram in the presheaf category. The fullness means that every
natural transformation between models is a morphism of models. Using these
facts you can get an embedding of 
in ; is then the full FL subcategory generated by the image of the
embedding.
This is worked out in detail for the FP case in [TTT], Chapter 4.3. The construction is then carefully described for the FL case in Chapter 4.4, but the proof is omitted. It is quite analogous to the FP case.
I have been focusing here on the FL case because that is the foundation of the construction of forms in [GBLS].
FP Sketches
An FP sketch and its FP
cattheory
are defined in
the same way, except that the finite diagrams that the cones are over have to
be discrete, and it has properties analogous to those for FL sketches given
above. Note that any FP sketch or linear sketch will also have an
FL cattheory.
The sketch for categories
FL sketches (finite-limit sketches) makes it possible to construct a sketch for categories. To do this you need some nodes:
, which in a model will become the set of objects -- so
in our "formal" terminology is the formal set of objects.
(This terminology, by the way, is due to John W. Gray.)
, the formal set of arrows.
, the formal set of composable pairs of arrows.
, the formal set of composable triples of arrows, needed to
state the associative law.
It needs many arrows, some of which are:
that formally picks
the identity arrow of an object
that formally pick the
source and target of an arrow.
that formally picks
out the composite of a pair of arrows.
...as well as many structural arrows that, for example, pick
out the first arrow in a composable chain, or that picks out the pair of arrows
given a composable
triple.
Cones and diagrams
Of course, you can’t just say that is the formal set of composable pairs
of arrows. What you must do is produce a cone that forces it to be
that formal set, in other words forces it to be the set of composable arrows in
a model. And here it is:
(The blue arrows are the projections, the black objects and arrows form the base diagram. Note that the middle blue arrow is superfluous. If you drop it, you may recognize this as an ordinary pullback diagram.)
You need an analogous cone for 
and diagrams for
associativity and to make the identity arrows behave right. The details
are in [GLBS], chapter 7.
In a model M, the elements of 
are diagrams that look
like this:
This green diagram is in the model (semantics), and the cone above is a diagram in the syntax. You have to make the distinction constantly in this subject. This is remarkably annoying. To help, I am systematically putting objects of the category-that-is-the-model in green, and cone projections in blue. Black and blue means syntax, green means semantics.
Remarks
is the domain of the composition arrow 
. So defining categories requires more subtlety that
defining an ordinary algebra, where the domains of the ops are always cartesian
products: this domain is an equalizer.
To sketch categories requires the full power of finite limits, not just
finite products. Of course, that last sentence does not follow
from anything I have said, since there might be a rascally way to use only
finite products. But there isn’t: the category of small categories is not
regular (Exercise 6, page 278, of [TTT]) but any
category of multisorted universal algebras (which are the same thing as models
of FP theories) does have that property: see [TTT], section
8.4.
Nevertheless, the category of models of an FL sketch always has all sortwise limits and all sortwise filtered colimits. in particular initial algebras.
Constructing a particular kind of limit or colimit sortwise means that it is
constructed sort by sort. For example, if always 
, then the category of models has sortwise products. In
most of the references the name “pointwise” is used.
Categories with structure
Many categories with particular properties can also be sketched with FL sketches. These include
- Categories with finite limits
- Cartesian closed categories
- Toposes
- Symmetric monoidal categories
- Abelian categories
Sketch for categories with finite products
A category has finite products (is an FP category) if it has terminal objects and binary products. GBLS describes the construction of the FL sketch for categories with finite products in section 7.3, which spells out how you sketch the set of terminal objects and the set of binary product cones. I will give a more detailed discussion of how to do binary product cones here and introduce the annotation notation we use.
Syntax and semantics
We must distinguish between two things:
- The FL sketch for FP categories
- The models of the FL sketch for FP categories, which are FP categories.
A diagram in the FL sketch will be in black (the color for syntax) and a diagram in a category with finite products will be green (the color for semantics). In both syntax and semantics, projection arrows may be blue and arrows that exist uniquely (fill-in arrows) may be red.
Product diagrams
A product diagram in an FP category looks like this:
(Diagram
)
But a diagram can look like that without being a product diagram. You have to say that it is a product diagram. This means that for any cone to the same pair of objects
(Diagram
)
there is a unique arrow h making this diagram commute:
(Diagram
F)
FL sketch for FP categories
To get the FL sketch for FP categories, you start with the sketch for categories and add some objects and arrows. The ones listed below are the objects and arrows needed for sketching the set of binary cones and finite-product cones. Others are needed for the terminal object (much easier and not done here).
Objects
, the formal set of cones of the form .
, the formal set of fill-in diagrams (diagrams of the form of
F above).
Arrows
, that picks out the product cone over a pair of objects.
, that picks out the source cone of a fill-in arrow.
, that picks out the target cone of a fill-in arrow.
, that takes a cone to the unique fill-in diagram that has
the cone as source cone.
that formally picks
out the fill-in arrow in a fill-in diagram.
Specification for the formal set of cones
The FL sketch for FP categories contains this limit cone, which requires that the two arrows in a cone have the same source. Note that I have named the projections lproj and rproj.
(Diagram
ConeSpec)
Annotations
This cone is annotated according to a
system that is spelled out precisely in [GBLS]. The
annotation of this diagram refers to cone above. Some perspectives on this
situation:
- The
annotations allow you to chase the diagram. For example, if is a member of
the set of cones of a model, then
and 
. In the
preceding sentence, I use abuse of notation: The sentence should say that 
and that 
. 
is being used as
the shape graph (see [GBLS], 2.3) for ConeSpec. - The annotation is a section of the model thought of as a sheaf.
Specification for the formal set of fill-in diagrams
This much more complicated annotated limit cone defines :
I completed the annotation compared to the version in GBLS, whose partial annotation generates the rest. The three projection arrows shown generate all the others, not shown to avoid clutter.
Some notes and examples:
- It is worthwhile checking through the conditions to see that this limit cone really does specify fid. If you do, you will see the sketch needs a couple of commutative diagrams, found in GBLS, 7.3.2.
- The whole diagram is commutative because of the diagrams just mentioned and the commutative diagrams of the FL sketch for categories mentioned above (and described completely in GBLS 7.2).
- This diagram is symmetrical in spirit, with one exception: The arrow prod breaks the symmetry because there is no corresponding arrow going upward. This reflects the fact that a fill-in diagram is not symmetrical: The right hand cone is a limit cone but the left hand cone is not.
- I suspect that the diagram could be drawn in a way that is really symmetrical (geometrically) in three dimensions (or four?), except for the break mentioned in (3).
Cartesian closed categories
A Cartesian closed category is a category with the following structure:
- has binary products.
- For
each pair of objects A and B of , there is an object
and an arrow 
. is an exponential
object. - For
each triple of objects A, B
and C of , there is a map
such that for every arrow 
, the diagram below commutes:
(lameval)
- For
any arrow
, 
.
It follows that 
is a natural isomorphism of homsets.
Currying
Going from to 
is called currying or
partial application. You can curry a multivariable function all the way
down to a constant. The inverse process is usually called uncurrying.
It constitutes getting rid of entries in the codomain of a function that
are function spaces by adding variables to the function. I suggest using
blanding instead of “uncurrying”.
The FL sketch for cartesian closed categories
The FL sketch for CCC’s (which I will call CCCSk) is spelled out in detail in [GBLS]. I will mention some of the constructions here. I will use many of them in the next section to give an example of a form.
Objects and arrows
The complete list is spelled out in Sections 7.2 and 7.6 of [GBLS]. Here I mention
that formally picks
out the identity arrow of an object.
, the formal set of functions of two variables, in other
words arrows of the form .
that picks out the
arrow 
itself.
that picks out the
source 
of a two-variable
function .
, the formal set of curried functions from 
.
and 
that pick out the
source and target of a curried function .
that picks out the
function space of two objects 
and 
.
, the formal set of composable pairs of arrows in the FL
sketch for categories, defined by this pullback diagram:
(Ar2Def)
For the purposes of the example below, I need 
as defined by this
diagram:
(Bsource)
In an object-oriented program built on this work, this would be a derived method..
One of the limit cones in CCCSk defines and in particular
gives 
the properties it needs:
(Curry)
The formally commutative diagram below should have been included in the FL sketch for categories in Section 7.2 of [GLBS]. It gives the composite of a composable pair the right source and target.
(Compreq)
Representing reflexive function spaces
An object of a cartesian closed category is reflexive
if there are arrows 
and 
such that
(ret)
commutes. That means 
is a retract of
. is called a reflexive
function space. Reflexive function
spaces are the theoretical basis for programming languages which have functions as first
class objects.
So a sketch for RFS’s would be defined by a limit cone over the diagram below. I have always shown the cones in blue before, but GBLS does not show cones at all, and it isn’t necessary to show them.
(ReflFSConeBase)
To specify a reflexive function space you would have to
give an object and two arrows 
that satisfies Diagram
(lameval) above, so the mandatory projections would be to 
, 
and 
. The projection to 
is induced by Diagram
(Curry) above, the projection to 
by Diagram (Ar2Def),
and the projection to 
follows from the fact
that it is the vertex of the product cone shown. The other projections exist by composition.
Let's call the vertex of this cone rfs for "reflexive function space". Note that all the objects and arrows in this diagram exist in the FL sketch for cartesian closed categories.
Now you can check (or forget all the constructions above and
just Put Your Hands On The Monitor And Believe) that in a model of the FL sketch for CCC’s, 
would be the set of reflexive function spaces
together with specified inclusion and retraction .
Non-surprise: In any model of the FL sketch for CCC’s
in the category of sets, will be the empty set. It is well known that for any
set the function space has cardinality properly bigger that
the cardinality of , so there can be no inclusion of into .
Nevertheless, is a perfectly well
defined set. It just turns out to be empty.
Forms
Forms are defined formally in [GBLS]. Here I will provide a form for reflexive function spaces as an example. In such a way that you get an informal definition of form.
Some terminology:
Constructor space
The sketch CCCSk for cartesian closed categories is a constructor
space. A constructor space must be an FL-sketch that “contains” and is
“generated” (see [GBLS],
Chapter 6.1) by the FL sketch for categories, and indeed CCCSk is built from
the FL sketch for categories by adjoining some objects and arrows, cones and
commutative diagrams that all exist already in the FL
Cattheory for categories. So a constructor space 
has models we can call C-categories.
In particular a model for CCCSk in sets is a cartesian closed category.
We can identify the constructor space as a doctrine. For example, the doctrine of equational
theories (FP sketches) is the constructor space for categories with finite products, and the
doctrine of cartesian closed categories is CCCSk. (I believe, without having thought about it enough, that this definition of
doctrine is spiritually the same as Beck's definition of
doctrine.)
Form
For any constructor space , take an object 
in the FL Cattheory of and adjoin a new arrow 
where 1 is the terminal object. is what we call a C-form and with as a freely adjoined arrow is called 
.
A "model of a -form in a C-category 
“ means that contains a model of 
. This means that in , 
is nonempty.
The CCC-form for reflexive function spaces is then a global element of the node 
of CCCSk as constructed above for
some CCC. There are no models in the category of sets, but there are many
toposes (and many other CCC’s) that do have models, as in domain theory.
More about a model of a form
Sketches are forms, in this sense: If you have a sketch in some doctrine (for example, a
finite-limit sketch), the sketch consists of a graph with some diagrams,
cones and cocones. There is a node S in the FL-Cattheory of finite-limit categories
each of whose elements in a model of S (in other words in an FL -category) will
be such a sketch.
Example: The FP sketch for magmas
A magma is a set with a binary operation defined on it. It does not have to be associative or commutative or anything.
In the FP doctrine, the sketch for magmas consists of objects
and 
, arrows 
and one cone
(Cone1)
and nothing else. The FP-Cattheory for this sketch is (equivalent to) the Lawvere theory of magmas.
The FL-Cattheory FPSk for FP categories contains a node whose inhabitants in any model of FPSk (in other words in any FP-category) are all such sketches (objects, arrows and the cone). This means that the FP sketch for magmas corresponds to an FP-form. In this way you can see that all sketches in Ehresmann’s sense are forms in my sense.
This node can be constructed as the limit of a cone over a diagram in FPSk. You have to make the diagram become
a description of the objects, arrows and cone above, using the arrows in
the constructor space FPSk. For example 
, 
, and others, and
including formally commutative diagrams that say for example that Cone1′s
projections go to the same object (using 
and 
}. Adjoining a global element to this limit node
will result in an FL-category 
which contains FPSk along with that
global element.
So a model of the form for magmas in an FP category 
is a model of for which the model of the underlying
cattheory FPSk is ; in other words it is the category with a
distinguished element f of the node . That distinguished element is a particular diagram
and cone like the ones shown above for a particular object (because the projections onto include a particular projection to 
That object with the arrows corresponding to 
, 
and 
is a particular
magma, a model of the sketch for magmas given above.
The paper [LimSk] contains two other examples of forms, the form whose models are categories with subterminal objects, and the category of groups with morphisms restricted to those that preserve centers. Neither of these categories can be sketched. They both use a "Universal Quantifier Constructor", and so have models in toposes.
Acknowledgments
Thanks to Toby Bartels for corrections and suggestions.
References
[GBLS] Atish Bagchi and Charles Wells, Graph-Based Logic and Sketches, draft, September 2008, on ArXiv.
[MSk] Michael Barr, Models of sketches (1986). Cahiers de Topologie et Géométrie Différentielle Catégorique, 27:93-107.
[LimSk] Michael Barr and Charles Wells. On the limitations of sketches (1992). Canadian Mathematical Bulletin, 35:287-294.
[CTCS] Michael Barr and Charles Wells, Category Theory for Computing Science (1999). Les Publications CRM, Montreal (publication PM023).
[TTT] Michael Barr and Charles Wells, Toposes, Triples and Theories (2005). Reprints in Theory and Applications of Categories 1.
[GMG] R. Brown, I. Morris, J. Shrimpton and C. D. Wensley. Graphs of morphisms of graphs, 2008.
[Mgm] M. Hazewinkel (2001), “Magma“, in Hazewinkel, Michiel, Encyclopaedia of Mathematics, Kluwer Academic Publishers, ISBN 978-1556080104
[SkEl] Peter T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Volume 2 (2002). Oxford Logic Guides 44, Oxford University Press, ISBN 978-0198524960.
[KPT] Yoshiki Kinoshita, John Power, and Makoto Takeyama. Sketches (1997). In Mathematical Foundations of Programming Semantics, Thirteenth Annual Conference, Stephen Brookes and Michael W. Mislove, editors. Elsevier.
[nLEquiv] n-Labs, Equivalence of categories.
[PHLCC] Palmgren, E and Vickers, Steven (2006) Partial Horn logic and cartesian categories. Annals of Pure and Applied Logic, 143 (3). pp. 314-353. ISSN 0168-0072
[FEAS] A.J. Power and Charles Wells. A formalism for the specfication of essentially algebraic structures in 2-categories (1992) Mathematical Structures in Computer Science, 2:1-28.
[FDDT] Charles Wells and Michael Barr, The formal description of data types using sketches, in Mathematical Foundations of Programming Language Semantics, M Main, A Melton, M Mislove, and D Schmidt, editors. Lecture Notes in Computer Science 298 (1988).
[GenSk] Charles Wells. A generalization of the concept of sketch (1990). Theoretical Computer Science, 70:159-178.
[Hbk] Charles Wells, A Handbook of Mathematical Discourse (2003).
[SkOut] Charles Wells, Sketches: Outline with references. (2009).
Charles (at) abstractmath.org