From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
Subject: Re: Topos theory for mere mortals (?)
Organization: Computer Science Department,  Stanford University.
Date: Wed, 30 Sep 1992 07:36:58 GMT

In article <1a9ufaINNhgd@usenet.INS.CWRU.Edu> cxm7@po.CWRU.Edu (Colin Mclarty) writes:
>	The higher powered approach is naturally "metatheoretic".
>If you want to look at some category from outside you can use this,
>and you can do it using comma categories in the category of all 
>categories.  There is a more subtle approach that is quite useful 
>when it applies, using "enriched categories" which now that I 
>think of it I am not going to explain here.  

I'm more of a fan of enriched categories than toposes myself, so since
I have a nice quiet afternoon let me have a bash at it.  Toposes are
great for foundations, which isn't really my cup of tea.  Enriched
categories on the other hand are just as nice for us setaholics as for
toposophers.  What's nice about them is that they give you a way of
thinking of posets, metric spaces, categories, 2-categories, and many
other familiar and not-so-familiar structures, all as instances of the
same basic idea of a *reflexive transitive graph*.  The price for the
generality is some hard work, but it's well worth it.

A category is just a graph with identity edges and a composition law.
But a category theorist's "graph" is a queer little creature with too
many edges: the rest of the world uses directed graphs having at most
one edge from x to y.  If this difference has ever worried you, then
with enriched categories your worries are over.  We're going to think
of an ordinary category as simply an ordinary directed graph with the
single edge from x to y labeled with a set.  Any set can be used as a
label, in particular the same set could label edges (x,y) and (y,x).
We don't think of the elements of a label as arrows until we know which
edge (x,y) is being labeled, at which time the elements of the set can
be construed as arrows with source x and target y.

A V-category is one with labels of type V.  Typical label types are
sets, truth values, integers, reals, categories, n-categories, and
posets.  Sets as labels yield ordinary categories, with Hom(x,y) being
a homset as usual.  Truth values yield partially ordered sets less
antisymmetry, i.e. *preordered* sets; Hom(x,y) becomes the proposition
"x <= y" which may be true or false.  Reals, thought of as either
distances or cost of travel, yield metric spaces less symmetry
(d(x,y)=d(y,x)) and "d(x,y)=0 => x=y", i.e.  *generalized* metric
spaces.  Categories yield 2-categories:  Hom(x,y) is now a category
whose objects are maps (the 1-cells) from x to y (0-cells) and whose
maps are 2-cells between maps from x to y.  More generally n-categories
yield (n+1)-categories:  Hom(x,y) of an (n+1)-category C is an
n-category whose i-cells are those (i+1)-cells of C having 0-source x
and 0-target y (the 0-cells of C).

For V = Poset (partially ordered sets) Hom(x,y) is a poset.  This
situation arises naturally for example with partial functions in Dana
Scott's approach to the semantics of partial recursive functions, where
functions are ordered by f<g when dom(f) subset dom(g) and g agrees
with f on the latter's domain.  Mitch Wand developed this perspective
on "Scottery" in terms of order-enriched categories in the late
1970's.  (We think of "enriching" the homsets with additional
structure, which makes sense for homobjects that have underlying sets,
the case for the original motivating examples, see "History" below.)

Set itself is enriched in the singleton category 1 having one object 0
and one map.  (A category enriched in 1 might look more like a clique
than a set.  However we typically imagine V as having an initial object
0, certainly the case for 1, with "missing" edges in a V-category
really being edges with label 0.  Thus a category enriched in 1 has all
edges missing in this sense, making it merely a set.)

Well, that's the basic idea behind enrichment, and perhaps all you
really want to know about enrichment.  But just in case you're a
glutton for punishment, here's the formal definitions of V-category,
V-functor, and V-natural transformation, and what's more, arranged so
that we can apply the method recursively to form (V-Cat)-Cat, e.g. to
get from the one-object category 1 to Set thence to Cat then 2-Cat by
repeated "-Cat"ing.

Before diving into the definitions it will help to look at one example
in more detail, namely generalized metric spaces.  A GMS is a category
enriched in the category R of nonnegative reals, with homobjects
Hom(x,y) now being real-valued distances d(x,y) satisfying

		     0 >= d(x,x)    ("0 >=" is the same as "0 =" here)

	 d(x,y)+d(y,z) >= d(x,z).

We have supposed the reals to be ordered by >= rather than its converse
<=,  i.e. the reals form a category with a map from  x  to  y  just
when x >= y.  For general V these inequalities will be given as
specific maps of R, from 0 to d(x,x) etc.  But in the case at hand, V=R
is a poset, hence having at most one map between any two objects of R.
So to specify a map from x to y says no more than to assert that a map
exists there, thus giving these specifications merely propositional
content.

An R-functor F:S->T between GSM's S,T then becomes a function from the
points of space S to those of space T, subject to the constraint
d_S(x,y) >= d_T(F(x),F(y)), making it just a contraction, a natural
notion of map of metric spaces.  Again this constraint is a specific
map, but as before it has only propositional content because V is just
a poset.


With that example we are now ready to get into details.  To keep sane
we will define the ordinary notions of category, functor, and natural
transformation, but using only those properties of Set that we have
assumed for our arbitrary V.  This makes it easy to verify that our
definition specializes to the usual one for V=Set, while still giving
it in full generality.  In particular we cannot assume that the objects
of V have underlying sets, since we have no sensible notion of the
underlying set of a truth value or a real.

Objects.  A category has first of all a set of objects; this remains
unchanged for general V and has nothing to do with whether V = Set or
not.

Homobjects.  The *homset* Hom(x,y) or C(x,y) of an ordinary category C
is an object of Set.  In a V-category C, the *homobject* Hom(x,y) or
C(x,y) is an object of V (what we were calling a label).

Identities.  For each object x of an ordinary category we must
distinguish some element of Hom(x,x) as the identity 1_x at x.  By
"element of X" in Set we shall mean a function from some fixed
singleton {*} to X, whence to specify an identity map in a category is
to give a function 1_x: {*} -> Hom(x,x), i.e. 1_x is a map of Set.  So
for general V, we need an object of V serving as a "singleton", call it
I.  Then in a V-category the identity 1_x at object x is a map
1_x: I -> Hom(x,x), a map of V.  Although {*} is final in Set we do not
require that I be final in V.

Composition.  For V=Set, ordinary composition is, for each triple X,Y,Z
of sets, a function m_{XYZ}: Hom(X,Y) x Hom(Y,Z) -> Hom(X,Z).  (I
should really write Hom(Y,Z) x Hom(X,Y) but when V-categories can be
posets or metric spaces this gets not only pointless but confusing.)

Tensor Product.  To generalize composition m_{xyz} to any V-category we
need something to play the role of Cartesian product in the domain of
m_{xyz}.  To this end we require that V be equipped with a binary
associative operation, written @ (\oplus) and called *tensor product*.
Hence composition in a V-category is, for each triple x,y,z of objects
of C, a map m_{xyz}: Hom(x,y) @ Hom(y,z) -> Hom(x,z) of V.  This is the
messiest part of the whole business, and will keep us occupied for the
next six paragraphs (which you might therefore want to skip on a first
reading).

Ordinary (aka direct, categorical, cartesian, <unqualified>) product is
automatically associative (up to an isomorphism) and hence a tensor
product.  V can have many tensor products but (up to isomorphism) only
one ordinary product.  We do not require that @ be ordinary product.
If we think of I as zeroary @ then this corresponds to not requiring I
to be final, the final objects being exactly the zeroary products.

Laxness.  Cartesian product, as Set's @, is only associative up to an
isomorphism, i.e. (XxY)xZ is isomorphic to but not equal to Xx(YxZ),
whence requiring *strict* associativity (XxY)xZ = Xx(YxZ), "on the
nose" as they say, is too strong.  We need a more "lax" definition of
"associative" as a natural isomorphism from the functor
(XxY)xZ:Set^3->Set to the functor  Xx(YxZ):Set^3->Set.  Not just any
natural isomorphism however but the "standard" one, a, which for each
object  (X,Y,Z)  of Set^3 is the function a_{XYZ}:(XxY)xZ -> Xx(YxZ)
mapping the element <<x,y>,z> of (XxY)xZ to the element <x,<y,z>> of
Xx(YxZ).

For general @ we require lax associativity, that is, associativity up
to a *specified* or "standard" natural isomorphism
a_{xyz}:(x@y)@z->x@(y@z), a family of maps of V indexed by objects of
V^3, i.e. a natural transformation from the functor (x@y)@z:V^3->V to
the functor x@(y@z):V^3->V.

Going back yet again to V=Set, we notice a certain important
"coherence" property of associativity of product in Set.  One can get
from ((WxX)xY)xZ to Wx(Xx(YxZ)) along various paths, of which the two
principal ones are in two steps via (WxX)x(YxZ), and in three steps via
(Wx(XxY))xZ and Wx((XxY)xZ).  Each path defines a composite natural
isomorphism f_{WXYZ}: ((WxX)xY)xZ -> Wx(Xx(YxZ)): on the 2-step path it
takes two applications of a, on the 3-step one it goes ax1 (that is, do
a:Wx(XxY)->(WxX)xY in parallel with 1:Z->Z), then a, then 1xa.  These
two composites turn out to be the same function (a bijection), namely
a'_{WXYZ}(<<<w,x>,y>,z>) = <w,<x,<y,z>>>.  In general we require of V
that these two paths compose to give the same natural isomorphism
a'_{wxyz} from ((w@x)@y)@z to w@(x@(y@z)); this requirement is called a
*coherence* condition.  It can be shown that this condition is
complete, in the sense that it is enough to ensure the corresponding
notion of coherence for natural isomorphisms between the expressions
built using @ from any fixed list of n distinct variables.  (There are
as many such expressions as binary trees with n leaves, given by the
n-th *Catalan number*.)

In addition to associativity we want to say that I is the unit for @,
namely x@I ~ x ~ I@x.  Call these two natural isomorphisms (between
These three functors from V to V) respectively r and l for right and
left identity laws.  With similar motivation to that for associativity
we require that the single step from (x@I)@y via r@1 to x@y equal the
two-step path via a to x@(I@y) thence via 1@l to x@y.

Monoidal.  We have now given all the conditions for V to be a *monoidal
category*.  V must be a category equipped with a specified object I, a
specified functor @:V^2->V, and specific natural isomorphisms a,l,r
satisfying the above two coherence conditions.

Associativity.  Having returned from the strenuous task of defining @
for V (the previous 7 paragraphs), we return to the description of the
identities and composition of a V-category.  Recall that these are
given by natural transformations

			      1_x: I -> Hom(x,x)
	m_{xyz}: Hom(x,y) @ Hom(y,z) -> Hom(x,z)

We now want to say that composition is associative and the identities
are left and right identities for compostion.

But what is an "equation" here?  For an ordinary category associativity
is an equality between composites f(gh) and (fg)h.  But here we cannot
refer explicitly to maps as elements of homobjects, which might be sets
(fine) or might be reals (what is an element of a real?).

We overcome this hurdle this with "variable-free programming", as in
combinatory logic or John Backus' programming language FP.  We want to
say that "ternary" composition can be defined as a map from
(Hom(w,x)@Hom(x,y))@Hom(y,z) to Hom(w,z), or from
Hom(w,x)@(Hom(x,y)@Hom(y,z)) to Hom(w,z).  In the first case it is two
applications of binary composition, more exactly the composite
(m_{wxy}@1)m_{wyz}.  In the second it is (1@m_{xyz})m_{wxz}.  We can't
require that these maps be equal since they have different sources, but
we get around this by prefixing a to the second map to yield
a(1@m_{xyz})m_{wxz}, which now has the same source and target as the
first map; these are what we require to be equal.  The equations for
the left and right identities follow the same general lines
(exercise).

That does it for V-categories.

V-functors.  In Cat, a functor F:C->D is a graph homomorphism (in the
intuitive sense of an incidence-preserving map of graphs) which in
addition for each edge (x,y) of C specifies a function
F_{xy}:C(x,y)->D(x,y) (the map portion of the functor), such that
F_{xx}(1_x) = 1_{F(x)} (F preserves identities) and F_{xz}(fg) =
F_{xy}(f) F_{yz}(g) (F preserves composition).  Exercise: generalize
this to V-functor by stating this using only the allowed properties of
V, with the same general idea we used for associativity. In particular
each F_{xy} becomes a map of V, which we can think of as stretching
from edge (x,y) to edge (F(x),F(y)).  For metric spaces this is just an
inequality preventing distances from increasing and so making an
R-functor a contraction.

V-natural transformations.  If @ was the hardest part, this is the
second hardest.  For V=Set, a natural transformation t:F->G of functors
F,G:C->D can be thought of as t sweeping F across to G:  t sweeps each
object x of C along a "path" t_x in D(F(x),G(x)) (i.e. a map of D), and
(the naturality condition) sweeps each map f:x->y of C(x,y) across a
commuting square (the only possible 2-cell since D has no nontrivial
2-cells, being an ordinary category).  That is, the following square
commutes:

              t_x
	F(x) -----> G(x)
	 |           |
	 |           |
	 |F(f)       |G(f)
	 |           |
	 |           |
	 V    t_y    V
	F(y) -----> G(y)

i.e. t_x G(f) = F(f) t_y.

To express the top-and-right composite, we produce a pair (t_x,G(f))
which we feed to composition (in D).  We can produce this pair by
applying the "element" t_x to * (the element of the singleton) and, in
parallel, G to f, call this the map t_x @ G.  And to get (*,f) from f
we use the inverse of the isomorphism l_{C(x,y)}:{*}@C(x,y)->C(x,y).
Putting these three maps together yields
(l_{C(x,y)}^{-1})(t_x@G)m_{F(x)G(x)G(y)} from C(x,y) to D(F(x),G(y)).
Going around the other way yields by similar reasoning the map
(r_{C(x,y)}^{-1})(F@t_y)m_{F(x)F(y)G(y)}: C(x,y) -> D(F(x),G(y)).
Naturality is then expressed by requiring that these two maps are
equal.  (As a commuting diagram this is a hexagon, which I don't have
the patience to type.)  But, after changing {*} to I, this is now all
expressed completely in the language of V, with no remaining non-V-ish
dependence on Set, so we are done.

Recursion.  If we obtain 2-categories as Cat-categories, where Cat was
obtained by taking categories to be Set-categories, then we clearly
need V-categories to be monoidal categories.  We take I in V-Cat to be
the category with one object * and with Hom(*,*)=I in V.  We take C@D
in V-Cat to be the V-category with object set the cartesian product of
the object sets of C and D, with (C@D)((x,y),(x',y')) =
C(x,x')@D(y,y'), and with the identities, composition law, and a,l,r
left for you to work out (lazy me---abstract from your understanding of
Cat as Set-Cat).  To show that this defines a monoidal category we need
V to have another property, symmetry, defined as follows.

Symmetry.  In Set, not only is product associative with left and right
identities, it is also *symmetric*, a natural isomorphism from
XxY:Set^2->Set to YxX:Set^2->Set, the standard one being
f(<x,y>)=<y,x>.  (So symmetry is also lax.)  For general V the symmetry
of V takes the form of a specific natural isomorphism s_{xy}:x@y->y@x.
The coherence axioms associated with symmetry are a triangle from x@y
to x@y (l = ss) and a hexagon from (x@y)@z to y@(z@x)
(asa=(s@1)a(1@s)).  This axiomatizes the notion of a *symmetric*
monoidal category.

A second use for symmetry (besides showing that V-Cat is a monoidal
category) is that we can now define the opposite of a V-category:
replace Hom(x,y) by Hom(y,x) and use symmetry to construct a new
composition law.

V is a V-category.  Set of course is a Set-category.  Cat is a
Cat-category because it has natural transformations.  Poset is a
Poset-category: the monotone functions in Hom(X,Y) form a poset under
their pointwise ordering.  The chain {0<1} is obviously a
{0<1}-category because these are just preordered sets, which includes
posets like {0<1}.  This is no coincidence.  Theorem: If V is closed
then V "is" a V-category, in the sense that there exists a V-category
whose objects are those of V and whose homobject Hom(x,y) is the object
x->y of V.  With this motivation we define:

Closed.  There is one last property of Set that we wish to generalize
to other V's.  We can fix one argument of a binary operation f:XxY->Z
to form a unary operation f_x:Y->Z (lambda-calculus and functional
programming language people call this Currying, recursion theorists
call it the s-m-n theorem).  Here f_x is the value of f':X->(Y->Z) at
some x in X.  There is a natural bijection between the set (XxY)->Z (of
functions from the set XxY to the set Z] and the set X->(Y->Z) [of
functions from X to the set Y->Z [of functions from Y to Z]], defined
by f(x,y)=f'(x)(y).  We encapsulate this property of Set by saying that
Set is *closed.* (Noting that the product used here was not any old
tensor product but ordinary or cartesian product, we say that Set is
*Cartesian* closed.) The general notion of "closed" for symmetric
monoidal V is that for each x in V, the functor F_x:V->V defined by
F_x(y) = x@y has a right adjoint G_x:V->V defined by G_x(z) = x->z,
also written z^x.  That is, the homset V(x@y,z) is naturally isomorphic
(in Set) to the homset V(x,y->z).  We call x->y the *internal hom* of
V, since it gives Hom(x,y) as an object of V rather than as some
external object such as a set.

Besides the theorem "V is a V-category", another use for closedness is
that the Yoneda lemma becomes available, in both its covariant and
contravariant forms.

A closed category for which @ is an ordinary product and I is final is
called *cartesian closed*.  A cartesian closed poset with finite sums
(coproducts) is a Heyting algebra (the generic model of intuitionistic
logic).  In lattice theory a closed poset (not necessarily cartesian
closed) is called a residuated poset.

Various Side Issues

Monoid objects.  When V is a discrete category (every map an identity
map), i.e. a set, this becomes exactly the notion of a monoid, since
functors on V become functions and natural isomorphisms become
equations, with naturality and coherence being satisfied vacuously.  A
nice way to say this is that an ordinary monoid is a monoid object in
Set, that is, an object X of Set (i.e. a set) together with arrows
I:{*}->X, @:X^2->X of Set (i.e.  functions) satisfying the
associativity and identity laws.  A monoidal category is a monoid
object V in Cat (i.e. a category) together with arrows I:1->V, @:V^2->V
(i.e. functors) and specific natural isomorphisms expressing
associativity and identity and satisfying the coherence laws.)

Category objects.  At the heart of the enriched category idea is the
notion of an edge-labeled graph of the graph theoretic kind, with at
most one edge from x to y.  This is one way to define "category"
abstractly in order to generalize the notion.  Another (the other?) way
is via the notion of a category object c in a category C (assumed to
have all limits), which is really a pair O,M of objects of C denoting
respectively the objects of c and the maps of c, along with maps
s,t:M->O, 1:O->M and m:M^2->M of C (2 being *ordinal* 2, making M^2
pairs of *consecutive* edges; with cardinal 2 it becomes any pairs of
edges) giving respectively the source, target, and identity map
functions, and the partial binary or "path-ary" (domain = length-2
paths) operation of composition.  An ordinary category is a category
object in Set.  A category object in Poset consists of a poset of
objects, a poset of maps, and s,t,1,m must all be monotone.  In Cat
s,t,1,m must all be functors.  (This is the obvious place to start when
defining categories in terms of themselves when bypassing set theory.)
And so on.

n-categories.  A map in a category can be thought of as a trajectory of
a point, and a 2-cell the trajectory of a 1-cell with fixed endpoints.
An (n+1)-cell runs between two n-cells x,y with common source s and
target t ((n-1)-cells), and can be visualized as the (n+1)-dimensional
volume obtained by sweeping a "floating" n-cell from x to y holding
fixed its endpoints at s and t.  So n-categories are really just
n-dimensional geometric objects that unlike ordinary space are not
required to offer travelers a way to back up.)

History.   Although the idea for enriched categories can be traced to
Mac Lane in the 1950's, the details were first worked out by Eilenberg
and Kelly (who taught me category theory) and presented at the 1966
conference in La Jolla.  This was first seen as the gneralized abstract
nonsense underlying abstract nonsense.  But then in 1974 Bill Lawvere
gave more concrete applications such as V = {0,1}, the reals, etc. to
show that the idea was really a very natural extension of the idea of
category including very simple examples like posets and metric spaces.
In 1982 Kelly produced "Basic Concepts of Enriched Category Theory"
(Camb. U. Press), from which I learnt most of the above.

My work.  My own applications of enriched categories have been to the
modeling of time as a closed category V, and behavior as a V-category
whose objects represent events and whose homobjects represent temporal
distances between events.  This abstraction covers a wide variety of
kinds of time: ordered time, real time (upper-bound, lower-bound,
exact-bound, etc.), causal time (a 3-element V distinguishing causal
from accidental precedence), strict time (the other 3-element V,
distinguishing necessarily nonzero delay from delay with possible
simultaneity), and so on.  This is written up as "Temporal Structures"
by Casley, Crew, Meseguer, Pratt, and appears in the new journal
Mathematical Structures in Computer Science, 1:2, 179-214, July 1991
(Cambridge U. Press).  I also make implicit use of enrichment in a
paper on quantum logic and linear logic to be presented at the Physics
of Computation Workshop in Dallas this weekend (retrievable from
boole.stanford.edu as qlll.tex, see the README).

-- 
=================================================== In short, I am floundering
Vaughan Pratt   pratt@cs.Stanford.EDU  415-494-2545 around and don't take what
=================================================== I say seriously.
Newsgroups: sci.math