An Introduction to Forms

**9 May 2014**

Charles (at) abstractmath.org

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.

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.

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

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. *

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.

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:

is a morphism of directed graphs. is a *natural transformation*fromto .

That is a start on understanding sketches: *Models are functors and morphisms between
models are natural transformations.*

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.

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).

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.

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!

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

For example, in the clone for groups, *x*(*y(xy*)) is
equivalent to (*xy*)(*x*y*)*. 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.

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.

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.)

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.

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.

- The sawhorse is
with respect to its two pairs of legs. The black (right) legs form a product cone but the*not symmetrical**blue**(left)*It could be called a**legs need not be a product diagram.****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 anof a cartesian product of arrow sets (the equation says that the source of one must match the product of the other).*equationally defined subset* - 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

A category **has finite products **if there is a product
diagram for any finite set of objects.

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.

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

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

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**.

In each case all the projections are shown on the left and only the necessary ones on the right.

(b)

(c)

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.**

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 .

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.*

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 *doesn’t *require anything that might
be called “*n*-sketches”. However, they will have the same problem
as ordinary categories in that in the category of models the structure has to
be preserved on the nose. In the case of
FL-sketches for different kinds of 1-categories, the sketch’s model category is
equivalent (but not isomorphic because of the nose problem) to the usual way we
define categories of that kind of category. What “equivalence” means for
“every kind of *n*-category” is referred to in [nLEquiv].

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.

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.

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

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.

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.

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.*

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.

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

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.

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.**

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**)

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).

, the formal set of cones of the form .

, the formal set of fill-in diagrams (diagrams of the form of
**F** above).

, 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.

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**)

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

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).

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.

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 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.

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)

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 a*ll 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 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:

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.)

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.

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.

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

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.

Thanks to Toby Bartels for corrections and suggestions.

[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, T*he 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