single set {*} and every arrow to the identity on this set.

Given two natural transformations h: F®H and t: G®H , their pullback is defined objectwise:

for every c in ObC let (p 1,c : Xc ® F(c), p 2,c : Xc ® G(c) ) be the pullback in Set of h c :

F(c)®H(c) and tc: G(c)®H(c) . Then define a functor X: Cop®Set where X(c) = Xc , and

for every f:c®d, X(f) is the only arrow that makes the following diagram commute:

In the same way we define two natural transformations p1: X®F, p2: X®F, where for every c in

ObC, p1(c) = p1,c and p2(c) = p2,c. Then it is easily verified that ( p1: X®F, p2: X®F ) is the

pullback of h: F®H and t: G®H.

60

3. Functors and Natural Transformations

As always, the pullback of two functors F and G on the terminal T gives the product F´G. It

is easy to verify that F´G(c) = F(c)´G(c) and F´G(f) = F(f)´G(f).

Exponents are defined by using the Yoneda lemma.

If GF is the exponent of F and G, we must have an isomorphism Nat[H´F,G] @ Nat[H,GF]

for every H. In particular, if H is C[_,c], and since by the Yoneda lemma, Nat[C[_,c],K] @ K(c)

for every K, we have: Nat[C[_,c]´F,G] @ Nat[C[_,c],GF ] @ G F (c). Thus, we define GF (c) =

Nat[C[_,c]´F,G].

Given an arrow f: c®d, we must now define GF(f): Nat[C[_,d]´F,G]®Nat[C[_,c]´F,G].

Let s be a natural transformation from C[_,d]´F to G; then GF (f)(s) must be a natural

transformation from C[_,c]´F to G. We define GF(f)(s) = s ° C[_,f]´idF (see example 3.2.2 for

the definition of the natural transformation C[_,f] : C[_,c]®C[_,d] ).

GF is a functor, indeed GF(id)(s) = s. Moreover :

GF(f ° g)(s) = s ° C[_, f ° g]´idF

= s ° C[_,f]´idF ° C[_,g]´idF

= GF(g)(s ° C[_,f]´idF )

= GF(g)(GF(f)(s)).

Let us define the natural transformation of evaluation e F,G : GF ´F®G. For every d in ObC ,

eF,G(d): Nat[C[_,d]´F,G]´F(d)®G(d) is defined by eF,G(d)(s,n) = s(d)(idd,n).

We prove now that for any H: Cop®Set we have an isomorphism Q: Nat[H´F,G] @ Nat[H,GF].

Let t: H´F®G be a natural transformation. For any c in ObC, Q(t)(c) ought to be a function

from H(c) to GF(c) = Nat[C[_,c]´F,G]. By the Yoneda lemma, we have for every c in ObC an

isomorphism gc: Nat[C[_,c],H] @ H(c); thus, if mÎH(c),

gc-1(m)ÎNat[C[_,c],H]

t ° (g-1(m)´idF) ÎNat[C[_,c]´F,G].

Define then Q(t)(c) = lm. t ° ( gc-1(m)´idF): H(c)®GF(c) = Nat[C[_,c]´F,G].

We must prove that, for every t: H´F®G, m: H®GF,

1. eF,G ° (Q(t)´idF) = t

2. Q(eF,G ° (s´idF)) = s

For (1) we have, for every dÎObC, mÎH(d), nÎF(d), the following:

(eF,G(d) ° (Q(t)´idF)(d))(m,n) =

= eF,G(d) (Q(t)(d)(m),n)

= eF,G(d) ( t ° (gd-1(m)´idF),n) by def. of Q

= (t ° (gd-1(m)´idF))(d)(idd,n) by def. of eF,G

as (gd-1(m))(d)(idd) = m

= t (d)(m,n)

For (2) we have, for every dÎObC, mÎH(d), cÎObC, hÎC[c,d], nÎF(d), the following:

(Q(eF,G ° (m´idF))(d)(m)(c)(h,n) =

= (eF,G ° (m´idF) ° (gd-1(m)´idF))(c)(h,n) by def. of Q

61

3. Functors and Natural Transformations

= eF,G(c) ( (m´idF)(c)( gd-1(m)(c)(h), n ) )

by def of gd-1

= eF,G(c) ( (m´idF)(c)( H(h)(m), n )

= eF,G(c) (m(c)(H(h)(m)), n)

= m(c)(H(h)(m))(c) (idc,n) by def. of eF,G(c)

= GF(h)(m(d)(m))(c) (idc,n) by naturality of m

by def. of GF(h)

= (m(d)(m) ° C[_,h]´idF) (c)(idc,n)

= (m(d)(m)(c) ((C[c,h]´idF(c))(idc,n))

= (m(d)(m)(c)(h,n). ¨

References We only give some references for the examples we mentioned, as they are not

usually presented in other books and are mostly endebted to the theory of computing. Partial

equivalence relations as a model for higher type computations were given in Kreisel (1959) and later

applied to the semantics of higher order intuitionistic logic in Girard (1972) and Troelstra (1973c).

They recently came again to the limelight as relevant structures for the semantics of polymorphism in

functional languages (see chapter 12). Limit spaces and their closure properties can be found in

Kuratowski (1952). With our perspective, filter spaces are used in Hyland (1979).

For (pre)sheaves and related notions, the reader should consult the previous references for Topos

Theory (as well as Fourman (1977) and Lambek and Scott (1986), among others). See also Scott

(1980) for an application of Yoneda•s embedding of arbitrary CCC•s (and their reflexive objects, if

any) into topoi of presheaves.

62

4. Categories Derived from Functors and Natural Transformations

Chapter 4

CATEGORIES DERIVED FROM FUNCTORS AND

NATURAL TRANSFORMATIONS

This chapter has two main motivations. One derives from the use of algebraic methods in computer

science, the other from recent developments in (applied) Proof Theory. The two research directions

are brought together nicely by the underlying categorical structures, which tidily generalize two

constructions crucial form the perspective of this book namely, products and exponents. Here, they

will be discussed in the context of monoidal and monoidal closed categories.

As already mentioned, geometry and algebra provided the background and motivations for the

early developments of Category Theory. In these areas, Category Theory often suggested both a

unified language and effective tools for an abstract description or specification of mathematical

structures. This method, which is typical of the categorical approach, has been widely explored in

computer science, in connection with ideas from universal algebra. The point is that, before

performing a complicated task, a programmer needs a clear specification of it. This may be given, for

example, by a set of equations, or by a logical system, or also by declarations of types (or sorts) and

operations on them. Inference rules may specify a theory.

This abstract approach, in computer science as well as in mathematics, is meant to simplify the

work for a concrete implementation, since only the essential or desired aspects of a task, a problem,

or a mathematical structure are focused on and dealt with. Unstructured lists of goals or properties are

hard to understand, are prone to errors, and may hide the core of the issue.

As we shall recall in section 4.1, algebras are usually described as sets with operations. Now

(binary) operations need some kind of ’product“ on the carrier sets to be specified or typed, e.g., a

group operation ’.“ is .: G´G®G. However, ’´“ does not need to be the familar Cartesian

product, as several relevant examples may be given by using (binary) functors that do not need to

possess projections. One may then ask whether these functors may relate to suitable exponents, in a

way that is similar for CCC•s. This further step will take us to the natural (and fruitful) generalization

of CCC•s as monoidal closed categories and will relate the algebraic perspective to the ’functional“

one, which permeates this book.

4.1 Algebras Derived from Functors

An algebra is a set, or carrier, together with a family of functions, or operations, on the carrier.

One may define categories of algebras by taking, as morphisms, well-behaved functions, the

homomorphisms, between algebras of the same kind.

63

4. Categories Derived from Functors and Natural Transformations

More precisely, let W be a set of operator symbols indexed by their arities. Wn , say, is the set

operators of arity n .

4.1.1 Definition The category Alg W , of W -algebras, has as objects pairs (A,a), where A is a

carrier set and, for each n and each operator symbol rn ÎWn, a yields a function ar : An®A.

An morphism f from (A,a) to (A',a') is a function f: A®A such that

f(a r(a1, . . . ,an)) = a'r(f(a1, . . . ,f(an))

for all n, rnÎWn and a1, . . . ,anÎA .

For example, any monoid (A,.) is an W-algebra, with a binary operation on a carrier set A. As an

instance of this, take Kleene's (PR,°), i.e., the monoid of the partial recursive functions, is an W-

algebra over PR, as carrier, with the binary operation of composition, as operation.

Remark (Commutative) monoids provide the basic instances of linear and multilinear algebra. In

particular, there is a tensor product A„B of commutative monoids that can be characterized by a

universal bilinear map m: A´B®A„B such that for each bilinear f: A´B®C, there is a unique

monoid homomorphism g: A„B®C such that f = g ° m . This idea, as well as the generality of

monoids, provide the basic mathematical intuition for the categorical notions developed in this

chapter.

One may specify more, though. For example, over (PR,° ) one may require the existence of

distinguished functions, such as constants for the identity, the successor and everywhere constant

functions. The behavior of these elements is specified by a set of well-known equations.

In general, this technique defines a class of W-algebras, called a variety. Varieties form full

subcategories of the intended category AlgW.

A well-known generalization of W-algebras is given by the many sorted, or heterogeneous, case.

That is, the operators are specified over more than one carrier. The applications of these notions are

nowadays a broadly construed area in computer science. However, until now, they have been more

indebted to universal algebra and Abstract Model Theory than to Category Theory (see the

References).

Example A stack is made out of finite words over a set el of elements A È {error} . Let {tt, ff}

be the boolean values and A* the finite words on A . The following signature specifies a stack as a

many sorted algebra with sorts el, stack, bool, and operators:

push : stack el ® stack;

pop : stack ® stack;

top : stack ® el;

64

4. Categories Derived from Functors and Natural Transformations

iserrel : el ® bool;

iserrstack : stack ® bool;

For variables x: stack and e: el, one has to set the following:

empty = l

push(x,a) = ’if xÎA and aÎA* then xa else error “

pop( xa ) = ’if xÎA and aÎA* then a else error “

top( xa ) = ’if xÎA and aÎA* then x else error “

iserrel(error) = tt

iserrstack(error) = tt

A few more equations specify the behavior of ’iserr . . . “ on elements and the stack, in the obvious

way.

Observe now that a set W of operators determines a functor T: Set®Set defined by

T(A) = {r(a1, . . . ,an) | nÎw, rÎWn, a1, . . . ,anÎA}.

Then an w-algebra (A,a) determines a set-theoretic function f : F(A)®A by

f(r(a1 , . . . ,an )) = a r (a1 , . . . ,an ).

This informal remark suggests another generalization of the notion of W-algebra. W-algebras are

based on carriers as sets; we may obtain a more category-theoretic description of the general concept

of algebra by taking endofunctors over arbitrary categories, instead of T: Set®Set .

4.1.2 Definition Let C be a category and T: C®C be an endofunctor. The category T-alg of

T-algebras is defined as follows: the objects of T-alg are the pairs (c,a) with cÎOb C and

aÎC[T(c),c]; the arrows between two objects (c,a) and (c',a') are all the arrows hÎC[c,c'] such

that a'° T(h) = h ° a . Graphically,

Identities and composition are both inherited from C.

Thus W-algebras are T-algebras for T: Set®Set, but T-algebras, in general, are defined over

categories of structured data, not just sets. One may take, for example, a collection of data types

which form a category C and include the type p of programs, over those data types, as object. Then

65

4. Categories Derived from Functors and Natural Transformations

T: C®C and a:T(c)®c, given by T(c) = p´c and a(i,x) = ’apply program i to input x “ give a

T-algebra (c,a) , for each object c (see example 1, after definition 4.2.3).

Consider now a preorder (P,£) as a category. A functor T: P®P is a monotone function. In

this setting, a T-algebra is a prefixed point for the functor T as the mere existence of a:T(e)®e

corresponds to T(e) £ e, which means exactly that e is a prefixed point for T. Recall also that the

least prefixed point of a monotonic function, if it exists, is always the least fixed point as well. This

property has the following correspondent in Category Theory:

4.1.3 Proposition Let C be a category and T: C®C. If (c,a) is an initial T-algebra, then a is

an isomorphism from T(c) to c in C.

Proof Consider the following commutative diagram

(T(c),T(a)) is a T-algebra, and aÎT-alg[(T(c),T(a)),(c,a)]. Let hÎT-alg[(c,a),(T(c),T(a))] be

the unique morphism given by initiality. Then a°h and idc are both morphisms in T-alg[(c,a),(c,a)]

and by initiality they must be equal. Moreover,

h ° a = T(a) ° T(h) as hÎT-alg[(c,a), (T(c),T(a))]

= T(a ° h) since T is a functor

= T(idc)

= idc since T is a functor. ¨

We can now go a step further and extend T-algebras to a more general notion, based on functors that

share only the target category, instead of endofunctors. This further step may be understood in a very

abstract way. Look at the diagrams for definition 4.1.2 and generalize them by using, in the lower

line, new objects d, d', say, instead of c, c', and a different functor instead of the (implicit) identity

functor. This gives comma categories, which we denote by (F’¯G) instead of the frequently used

(F’,G).

4.1.4 Definition Let F: C® A, G: D® A be functors. The comma category (F’¯G) is

defined as follows: the objects of (F’¯G) are the triples (c,f,d) with cÎOb C , dÎOb D ,

fÎA[F(c),G(d)]; the arrows between two objects (c,f,d) and (c',f',d') are all the pairs (h: c®c',k:

d®d') such that f' ° F(h) = G(k) ° f . Graphically,

66

4. Categories Derived from Functors and Natural Transformations

The identity of (c,f,d) is (idc, idd); composition is defined componentwise, that is, (h',k') ° (h,k) =

(h'° h, k'° k).

Observe that by this further abstraction, we hit upun a notion examined in another context. Indeed, if

a is an object of C, and Ka: C®C is the constant functor taking every object to a, and every

morphism to ida, then (Ka¯idC) is just the category of objects over a, or slice category, mentioned

in definition 1.3.4.

4.1.5 Example A (possibly finite) graph G is a triple (T,¶,V), where T is a set of arcs (or

edges), V a set of nodes, and ¶: T®V´V a function that gives the source and target of each arc. A

morphism h from G to G' is a pair of functions <f,g >, f: T®T' and g: V®V' such that

g ° p0 ° ¶ = p0 ° ¶'° f and

g ° p1 ° ¶ = p1 ° ¶' ° f ,

where p0 and p1 are the projections.

This, with the obvious componentwise composition of morphisms, defines the category Graph.

Graph is a comma category (Id¯D) defined by the identity and the diagonal functors Id, D:

(Fin)Set®(Fin)Set.

Exercises

1. Prove that Graph is cartesian.

2. Observe that a category is a graph with some extra structure: identities for each object (node) and

composition for morphisms (arcs) of the due types. Give a (forgetful) functor from Cat, the category

of small categories, to Graph. Is this functor full?

4.2 From monoids to monads

Consider again a monoid (A,.,e), i.e., a carrier A, a binary associative operation and a (specified) left

and right identity for ’.“.

The monoid may be described as the set A together with two functions m: A´A®A and

h:1®A, where 1 is the singleton set (or terminal object in Set). The idea is that m describes the

67

4. Categories Derived from Functors and Natural Transformations

internal operation ’.“ and h picks up the identity in A. Associativity of the application and the

properties of the identity are given by the following commutative diagrams:

idxm hxid idxh

A3 A2 A2

1xA Ax1

m

mxid iso iso

m

A2 A

A

The abstract specification of monoids above can be generalized in several ways. We consider here the

case where functors are used as carriers, instead of sets. To this purpose, recall that each endofunctor

T: C ® C has composition Tn+1 = T n ° T : C ® C . Moreover, if m: T 2 ®T is a natural

transformation, whose components are mc: T2c®Tc for every cÎObC, then Tm: T3®T2 and

mT: T3®T2 are the natural transformations obtained by horizontal compositions, as in section 3.2.

Their components are (Tm)c = T(mc): T3c ® T2c and (mT)c = mTc: T3c ® T2c , respectively.

The idea is that an endofunctor of a category forms a monoid when the product of sets above is

interpreted as a composition of functors.

4.2.1 Definition A monad over a category C is a triple (T, m, h), where T: C®C is a functor,

m: T2®T and h: Idc®T are natural transformations, and the following diagrams commute:

mT

Th

3 hT

T2 T2

T T T

m

Tm idT id T

m

T2 T T

m

As in the case of monoids over a set, h and m give the identity and the internal operation. The

diagrams describe the behaviour of the (left and right) identity and associativity.

Remark Many other names have also been used in literature in place of ’monad“: the most common

is ’triple,“ but sometimes, you will find ’triad“ or ’standard construction.“ See Barr and Wells

(1985) for an interesting account of the history of this name.

Examples

1. Let M be a monoid and define T: Set®Set by T(A)=M´A, T(f)=idM´f. Let hA: A®M´A

and mA: M´M´A®M´A be, respectively, the functions that take a to (1M ,a) and (m,n,a) to

(mn,a). Then the associative and unarity identities follows from those of M .

68

4. Categories Derived from Functors and Natural Transformations

2. Let T be the covariant power-set functor, i.e., T: Set®Set as given by T(A) = P(A), the

powerset of A , and T(f)(B) = {f(a) | aÎB Í A} as the image of B along f . Then h A is the

singleton map hA(a) ={a} and mA is the union map mA(B) = ÈB. As for the next example, it is an

easy exercise to show that (T, m, h) is a monad.

3. As mentioned below definition 4.1.2, a preorder (P,£) yields a category where endofunctors are

monotone functions. If one has also a monad (T, m, h), the natural transformations h and m give

that, for any aÎP, a £ Ta and T(Ta) £ Ta, since h a : a®Ta, and m a : T(Ta)®Ta. By putting

together these inequalities with the monotonicity of T, one has Ta £ T(Ta) £ Ta. Therefore, a monad

in a partial order is a closure operator, since, in this case, T(Ta) = Ta.

4.2.2 Definition A comonad over a category C is a triple (T, d, e), where T: C® C is a

functor, and d: T®T2 and e: T®idC are natural transformations, such that the following diagrams

commute:

In definition 4.1.2, we defined the notion of T-algebra over a generic endofunctor T: C®C. Thus,

one may have T-algebras, if any, over a monad (T, h, m ). In this case, though, it is sound to

impose some extra conditions and ask that the monad•s operation and identity, given by m and h,

commute with the operation of T-algebra. That is, a T-algebra (c, a) is given by a monad (T, h,

m ) over a category C if it also satisfies the following commutative diagrams:

Th hc

T 2c Tc c Tc

h

h 1

mc

c.

h

Tc c

Or, equivalently, h ° T(h) = h ° mc ;

h ° hc = idc .

69

4. Categories Derived from Functors and Natural Transformations

When T is the functor of a monad (T, h, m ), we shall simply say T-algebras with the intended

meaning to be derived by the monad. This collection of T-algebras can be organized in a category by

adopting the same notion of morphism as in definition 4.1.2.

2.3 Definition Let (T, h, m ) be a monad over a category C . The Eilenberg-Moore

Category CT associated with the monad has T-algebras for objects, and for morphisms from (c,

a) to (c',a') all the arrows hÎC[c,c'] such that a'° T(h) = h ° a.

Examples

1. Consider the monad (T, h, m ) associated with a monoid M as in example 1 above. Then a T-

algebra is a pair (A, a) where a: T(A) = M´A®A. Let us write m*a in place of a(m,a); then, for

every aÎA and m,nÎM, the equations of a T-algebra read:

1*a = a ;

(m n)*a = m*(n*a) .

In other words, an algebra for the monad associated with a monoid M is just what is usually called an

M-set. Moreover the equation for a morphism h of T-algebras gives, for every aÎA and mÎM,

h(ma) = m h(a), that is the usual notion of homomorphism of M-sets.

2. In connection with example 3 above, observe that if the category C is a preorder, then c £ T(c),

by hc, and T(c) £ c, by a of the T-algebra. Thus, if C also happens to be a partial order, any T-

algebra given by a monad is a fixed point in the p.o.set.

Let (T, h, m ) be a monad over a category C. Then, for every cÎObC, (T(c), mc) is a T-algebra.

Indeed,

mc ° T(mc) = mc ° mT(c) by the associative law of (T, h, m )

mc ° hT(c) = idc by the unity law of (T, h, m )

The algebra (T(c), mc) is called the free algebra generated by c (with respect to T).

The computational significance of monads has been stressed recently in suggestions that they may

help in understanding programs ’as functions from values to computations.“ The approach we sketch

here, and which seems very promising, still belongs to a denotational view in program semantics;

however, it suggests an alternative to the conceptual gap between the intensional (operational) and the

extensional (denotational) approach to the semantics of programming languages. The idea, roughly,

is to give a denotational semantics to computations. The intuition we have been mostly referring to, in

the examples and in the presentation so far, is that objects are data types and morphisms are functions

or programs in extenso. However, one may need a better display of the intensional aspects of

computing and distinguish between values and computations. From this point of view, we can try to

look at programs not as transformations from values to values, but as transformations from values (or

70

4. Categories Derived from Functors and Natural Transformations

programs) to programs. This should be done by stressing the effectiveness and the intensional nature

of actual computations, without losing the insight and the elegance of the intended extensional

approach. That is one should preserve the conceptual unity of the mathematical view (e.g., by

categories and related structures), and without getting lost in the taxonomy and details of the

operational descriptions.

The idea of a monad (T, h, m ) as a model for computations is that, for each set of values of type

A, T(A) is the object of computations of ’type A.“ Then one may understand that hA : A®TA

maps values to computations, and mA: T2A®TA flattens a computation of a computation into a

computation. If one also requires that hA is a mono for every AÎC, then values form a ’subset“

of computations (see section 1.5, for subobjects).

Examples

1. The above example of the power-set functor as a monad may give a description of nondeterministic

computations by looking at nondeterministic computations as sets of values. hA picks up a specific

computation, as h A (a)={a}, and mA says that a nondeterministic computation over non-

deterministic computations, yields a nondeterministic computation, as mA(B) = ÈBÎP(A).

2. Even more expressively, computations with side effects may be described by the functor T(A) =

(A´S) S , where S is a set of stores. Intuitively a computation takes a store and returns a value

together with the modified store. Then a monad is obtained by setting, for each type (or object) A,

hA(a) = ls:S.(a, s) and mA(f) = ls:S.eval(fs)) .

The meaning of hA should be clear; while for each fÎ(A´S)S, mA(f) is the computation that, given

a store s, first computes the pair (computation,store) given by (f',s') = fs; then evaluates f'

applied to s' and returns a new pair (value,store).

In the application of monads the idea is to go from objects, or types, to the image by a functor of an

object. More specifically, in the examples, programs take values in A, say, to computations in TB .

Kleisli categories provide the right setting to describe this approach.

4.2.4 Definition Given a monad (T, m, h) over C, the Kleisli category CT , is the category

whose objects are those of C ; the set CT[A,B] of morphisms from A to B in CT is C[A,TB];

the identity in C T [A,A] is h :A®TA . Moreover, the composition of fÎC T [A,B] and gÎ

CT[B,C] in CT is g° f = mC ° Tg° f : A ®TB ® T2C®TC .

Exercises

1. Use the lifting functor (_)» after proposition 3.2.3 and observe that the Kleisli category is the

category of ’total maps“ over a given category of partial morphisms.

2. Give the notion of co-Kleisli category (see section 5.5).

71

4. Categories Derived from Functors and Natural Transformations

Eilenberg-Moore and Kleisli categories will be used in the next chapter when discussing adjunctions

and monads, and they will be applied in the semantics of linear logic.

4.3 Monoidal and monoidal closed categories

In section 4.2 we began by describing, with a diagram, the familiar notion of monoid. This motivated

the definition of monads, when Cartesian products in Set are substituted with composition of

functors, as in definition 4.2.1.

In both cases, we worked essentially ’up to isomorphisms“. As for monoids, we identified

(A´A)´A with A´(A´A), in the upper left vertex of the first diagram in section 4.2, and called both

A3. Similarly for T3, which is short for T»(T»T) and (T»T)»T, we followed a similar procedure in

definition 4.2.1. This is perfectly sound as both Cartesian product and composition are associative.

The next step now is the explicit formalization of these (implicit) properties, including the behavior of

the terminal object 1, as a left and right unit, since they are needed in all categories where it may be

possible to define monoids and derived notions.

4.3.1 Definition A monoidal category is a category C with a bifunctor „ :CxC ® C, a (left

and right) identity eÎObC and natural isomorphisms, for each a, b , cÎObC,

aa,b,c : a„(b„c)®(a„b)„c ;

la : e„a®a ;

ra : a„e®a ;

such that the following diagrams commute:

a

a „ (b „ (c „ d)) (( a „ b) „ c) „ d

a

(a „ b ) „ (c „ d)

1„a a„ 1

(a „ (b „ c)) „ d

a „ ((b „ c ) „ d) a

a „ (e „ c ) (a „ e) „ c

a

id „ l r „ id

a„ c

Indexes for the natural transformations a, l, and r will usually be skipped, when they are clear

from the context.

72

4. Categories Derived from Functors and Natural Transformations

Remarks 1 - The ’tensor product“ „ in a monoidal category does not need to be unique, in

contrast with the Cartesian product (see the example below in the category Stab and Lin). Observe

also that the dual of a tensor product is, formally, just (another) tensor product, since isomorphisms

define the monoidal structure and the reverse of an isomorphism is still an isomorphism.

2 - The motivation for the two diagrams in definition 4.3.1 originate from a relevant fact, whose

treatment goes beyond our limited aims. In short, it may be shown that in momoidal categories, as

defined above, any two (natural) isomorphisms built out of a, l, r and id, by using „ and

composition, actually coincide (’coherence theorem“). For example, a„(b„c)„(a'„b') and

(a„b)„(c„a'„b') are isomorphic in just one way.

4.3.2 Definition A symmetric monoidal category (C, „, e, a, l, r) is a monoidal category

such that for all objects a,b there is a natural isomorphism ga,b: a„b®b„a and

ga,b ° gb,a = idb,a

rb = lb ° gb,e : b„e®b

and moreover the following diagram commutes:

The diagram in 4.3.2 is motivated by an extension of the coherence theorem mentioned in the remark

above.

Example Every Cartesian category is a symmetric monoidal category, with respect to the categorical

product, and the obvious choice for the isomorphisms. Roughly, the tensor product, in the sense of

monoidal categories, differs from the Cartesian product in that it has no projections and pairing

functions.

Exercise Let C be a category with a coproduct for every pair of objects (i.e., C is co-Cartesian).

Prove that C is a symmetric monoidal category.

Example In section 2.4.2, we introduced the category Stab of coherent domains and stable

functions. Any coherent domain X is obtained from a set |X| of points and a binary relation - ,

73

4. Categories Derived from Functors and Natural Transformations

coherence, on |X|. Stable maps are continuous functions which also preserve intersection of coherent

arguments. Stab is a CCC.

In the same example, we noticed that one could also consider the linear maps between coherent

domains. They are stable ones which also commute with respect to arbitrary unions (see exercise 4

below definition 2.4.2.6). Lin is the category of coherent domains and linear functions. Products in

Lin are defined as for Stab, as the projections happen to be linear maps; thus, Lin is also Cartesian.

However, there is another relevant functor from Lin´Lin to Lin. Given coherent domains X

and Y, let (|X|´|Y|,-´) be given by (x,y)-´(x',y') iff x-x' and y-y'. Let X„Y be the coherent

domain obtained from (|X|´|Y|,-´). This is not a product in Lin, but the reader may easily check that

it turns Lin into a symmetric monoidal category.

We will mention again the categories Lin and Stab, and their interesting interplay, in section 4.4,

since they inspired Linear Logic.

Exercise Let S… be the free commutative monoid generated by a set S. Prove then that, for

S … „S'… = (S´S')… , the freely generated commutative monoids form a symmetric monoidal

category.

Example Our next example is borrowed from recent investigations of parallelism and concurrency,

based on a categorical description of well-known structures for those aspects of computations,

namely, Petri nets.

The category of graphs was defined in the example 4.1.5. For readability we write ¶0 = p0 ° ¶

and ¶1 = p1 ° ¶ and set (¶0,¶1: T®V) for the graph G = (T, ¶, V). Now, every graph G may

be turned into a category. Call C(G) the category whose objects are the nodes V of G, whose

arrows are generated from the arcs T of G by adding the identity arc for each node and closing

freely w.r.t. composition ’»“. Clearly, C is a functor from the category Graph in the example 4.1.5

to Cat (this method will be discussed when presenting adjunctions, see example 2 in section 5.3).

A (transition/place) Petri net is a graph N = (¶ 0 ,¶ 1 : T® S … ), where the arcs are called

transitions and whose nodes are the elements of the free commutative monoid S…, generated by a

(possibly finite) set S of labels, the places. Similarly for graphs, we may perform the free

construction of a category C(N), on top of a Petri net N. However, N has an extra structure: namely

the monoid structure of S…. Thus we may obtain a monoidal category as follows. Let C„(N) be the

category whose objects are the nodes of N, with u„v = uÈv in S…, and whose arrows are freely

generated from the transitions T of N with respect to composition ’»“ and the monoidal operation

„ as well. In short, for each pair f: u®u' and g: v®v' one also has f„g: u„v®u'„v' in

C„(N). The functoriality of „: C„(N)®C„(N) is expressed by

(1) (f„g) »(f'„g') = (f»f')„(g »g') .

74

4. Categories Derived from Functors and Natural Transformations

The intended meaning of the monoidal operation -„- is the parallel composition of arrows, while ’»“

is the sequential composition. Thus, net computations are understood as the closure of the transitions

with respect to the parallel and the sequential composition. (Exercise: discuss the meaning of (1)

above).

Monoidal categories provide the right setting for a generalization of the notion of ’monoid“.

4.3.3 Definition Let (C, „, e, a, l, r) a monoidal category. A monoid in C is an object c

together with two arrows m: c„c®c and h: e®c such that the following diagrams commute:

A morphism between two monoids (c, m, h) and (c', m', h') is an arrow f: c®c' in C such that

f ° m = m' ° (f„f) : c„c®c'

f ° h = h' : e®c'.

It is easy to prove that with the previous definition of morphisms, monoids over a monoidal category

C form a category MonC.

Examples

1. Set, with a Cartesian product, is monoidal and the monoids in it are exactly the ordinary monoids.

2. Given an arbitrary category C, consider the category of endofunctors C C , with natural

transformations as morphisms. Then composition ’°“ of functors is a bifunctor from CC´CC to CC

which turns CC into a monoidal category. The reader may easily check for exercise that the monoids

in this category are exactly the monads in definition 4.2.1 and thus understand the elegant conceptual

frame provided by the categorical developments of the notion of monoid.

75

4. Categories Derived from Functors and Natural Transformations

Dually, we have the concept of ’comonoid.“

4.3.4 Definition Let (C, „, e, a, l, r) be a monoidal category. A comonoid in C is an object

c together with two arrows d: c® c„c, e: c®e such that the following diagrams commute:

A morphism between two comonoids (c, d, e) and (c', d', e') is an arrow f: c®c' in C such that

f° d' = (f„f) ° d : c® c'„c'

e' ° f = e : c®e' .

As we have pointed out, monoidal categories are given by an abstract notion of ’product,“ described

only in terms of (natural) isomorphisms or, equivalently, in terms of collections of isomorphisms

between objects with no further properties (cartesian products also have projections).

Observe that, in the special case that C is Cartesian, each object is a comonoid: just set d =

<id,id>, i.e.,

Similarly to the construction of cartesian closed categories from cartesian ones, one may extend the

abstract or ’equational“ approach for monoidal categories and give a notion of monoidal closed

categories.

76

4. Categories Derived from Functors and Natural Transformations

4.3.5 Definition Let C be a symmetric monoidal category, with respect to the bifunctor „. Then

C is monoidal closed if there is also a bifunctor Þ: C´C®C such that, for every object b, there

exists an isomorphism L : C[a„b,c] @ C[a,bÞc] that is natural in a and c.

Clearly, any CCC is monoidal closed.

3.6 Exercise

1. (Important for the purposes of sections 4.4 and 5.5) Lin, with „ as in the example below

definition 4.3.2, is symmetric monoidal closed (hint: see section 2.4.2 and use the coherent domain

of traces of linear maps as ’Þ“; note that this is not an exponent for the Cartesian product in Lin).

2. Consider the tensor product „ of monoids given in the remark below definition 4.1.1. There is a

natural isomorphism A„B @ B„A, and the monoid homomorphisms between two commutative

monoids A and B form a commutative monoid [A®B]. Prove then that there is a natural isomorphism

[(A„B)®C] @ [A®[B®C]], making the category cMon, of commutative monoids, a symmetric

monoidal closed category.

3. Let e be the identity of a monoidal closed category. Prove then that eÞa @ a for any object a.

(Hint: use the diagram

in your proof.)

Example We already defined Petri nets and turned each individual net into a (monoidal) category.

We could thus view the relation between parallelism and sequentiality as a functorial notion (see the

example below definition 4.3.2). We consider now the collection of Petri nets as a category. The

category Petri, of (transition/place) Petri nets, has Petri nets (¶0,¶1: T®S… ) as objects, where

S… is the free commutative monoid generated by S. Morphisms are pairs <f,g >, f: T®T' and g:

S … ® S' … as for graphs (see the example 4.1.5), with the extra condition that g is monoid

homomorphism. (Exercise: describe Petri as a comma category). As the careful reader should

have checked, given two graphs G = (¶0,¶1: T®V) and G' = (¶'0, ¶'1: T'®V'), their cartesian

product is the graph G´G' = (¶ 0 ´¶'0 ,¶ 1 ´¶'1 : T´T'®V´V'). When considering Petri nets N =

(¶0,¶1: T®S…) and N' = (¶'0,¶'1: T'®S'…), their product as graphs, that is

N´N' = (¶ 0 ´¶'0 ,¶ 1 ´¶'1 : T´T'®S … ´S'… ),

77

4. Categories Derived from Functors and Natural Transformations

is also a Petri net, since S… ´S'… @ (S+S')… , i.e., the product of two free commutative monoids

S… and S'… coincides with the monoid freely generated by (S+S'). The Petri net N´N' is called

the synchronous product of the nets N and N'. Intuitively, the sychronous product of two Petri nets

is the results of a composition operation with synchronization: the places of the result are the union of

the places of the factors, while the transition in the synchronous product are pairs (i.e.,

synchronization) of the given transitions. Since S……S'… @ (S+S')… is valid as well, the category

Petri has also coproducts, namely,

N…N' = ([¶ 0 ,¶'0 ],[ ¶ 1 ,¶'1 ] : T+T '®(S+S') … ),

where [¶i,¶'i] denotes the function induced on the coproduct T+T' by the functions ¶i and ¶'i.

Intuitively, the coproduct of two Petri nets is the result of a composition operation without

synchronization: the two nets laid aside without interaction. The choice is nondeterministic because of

the freedom of choosing an arbitrary initial state.

The initial net has no transition and no places, while the final net has one transition and no places.

As the reader has proved for exercise, the tensor product of free commutative monoids satisfies

S… „S'… = (S´S')… . Thus, one may define - „ - : Petri2®Petri, the tensor product N„N' of

two Petri nets N and N', by taking as transitions the Cartesian product of their transitions, as places

the cartesian product of their places, and using the equation S…„S'… = (S´S')… to define nodes

from places. The unit object I is the Petri net (¶0,¶1: [1]®[1]…), with ¶0 = ¶1 the inclusion of

[1] in [1]…. In conclusion Petri is cartesian, cocartesian and is a monoidal category with a tensor

product derived from that operation on monoids.

The next step is to discuss the monoidal closed structure. This is easy when considering finite

Petri nets since, whenever S = {a1, ..., an} is finite, we have

n n

n

@ ( S' + . . . + ' ).

[S @ S'

® S' x . . . x S' S

@ S' S'

]

...

Define then the ’Þ“ functor, on finite Petri nets, as follows. Given Petri nets N and N', NÞN'

has as arrows the set of triples

{(h: T®T', g: S… ®S'… , g': S… ®S'… ) / g,g' are monoid homomorphisms, ¶'0 ° h = g ° ¶'0

and ¶'1 ° h = g' ° ¶1 }.

For S = {a1, ..., an} the monoid of nodes is the free commutative monoid (S'+ ... +S')… , n

times, and ¶0 and ¶1 are the second and third projection. It is then clear that (finite) Petri is a

symmetric monoidal closed category.

Monoidal closed categories generalize Cartesian closed ones in that they also possess exponent

objects aÞb, or ba, which ’internalize“ the hom-sets. One may then ask if there is a way to

describe ’internally“ the behavior of funtors on morphisms. That is, given a monoidal closed

category C and a functor F: C®C, consider, say, fÎC[a,b]. Then F(f)ÎC[F(a),F(b)]. Since ba

78

4. Categories Derived from Functors and Natural Transformations

and F(b)F(a) represent C[a,b] and C[F(a),F(b)] in C, one may study the conditions under which

F is ’represented“ by a morphism in C[ba, F(b)F(a)], for each a and b.

4.3.7 Definition Let C be a monoidal closed category. A functor F: C®C is closed if, for

each a and b in C, there exists fabÎC[ba, F(b)F(a)] such that, for all gÎC[a,b],

fab» L(g»la) =L(F(g)»lF(a))

where L : C[e„a,b] @ C[e,ba] and la: e„a®a are as in 4.3.1.

The notion of a closed functor soundly formalizes our aim above, in view of proposition.4.3.8

below. This essentially says that, internally, fab takes the identity to the identity and behaves

correctly w.r.t. to composition. We will call fab the action of F on ba.

4.3.8 Proposition Let C be monoidal closed category and F: C®C a closed functor. Then the

collection {fab | a,bÎOb C } of its actions is natural in a and b. Moreover, let compabc :

ab„bc®ac be the natural transformation which internalizes composition, and IDa: e®aa be the

natural transformation which ’picks up“ the identity in aa, i.e., IDa = L(la). Then the following

equations hold:

i. faa » IDa = IDF(a)

ii. "g: b®a, "h: c®b, fac » comp » L(g»lb)„L(h»lc) = comp » fab„fbc » L(g»lb)„L(h»lc)

Proof Exercise. ¨

4.3.9 Remark By similar techniques for monoidal categories, one may define other classes of

categories. In particular, this can be done in order to study very weak frames dealing with a notion of

exponent object. Consider for example a category C, not necessarily monoidal, but with an

’exponent“ functor which realizes the following natural isomorphism, C[a,cb] @ C[b,ca] satisfying

suitable identities. C is called symmetric closed. Clearly any symmetric monoidal closed category

is symmetric closed. This description of categories by (natural) isomorphisms may remind the reader

of remark 3.3.3, where we described the set of isomorphisms which hold in all CCC's. Those

equations do not characterize CCC's, as cartesian closure requires further structural properties, i.e.

projections. They may be used instead to define the larger class of symmetric monoidal closed

categories with a terminal object. (The reader may try to complete, as an exercise, the

definition of the classes of categories in this remark.)

4.4. Monoidal Categories and Linear Logic

The perspective of this book is to introduce and use Category Theory mainly in order to understand

’types as objects“ of (Cartesian Closed) Categories. Indeed, this will be the focus of the chapters in

79

4. Categories Derived from Functors and Natural Transformations

Part II. In the literature, so far, the categorical semantics of types has been mostly applied to the

functional notion of type, in connection with proof theoretic investigations. The link to functional

languages is described by the motto ’propositions as types,“ which proved successful both in the

mathematical investigation and in concrete applications as the design of new functional languages with

powerful type systems. It seems promising to explore similar analogies for other approaches to

computing, where nonfunctional constructs, e.g., parallel features, are considered. These motivations

and the properties of relevant categories, namely Stab and Lin, the categories of stable and linear

maps widely discussed in section 2.3 and in the previous section, have suggested a new formal

system, linear logic.

The crucial difference between the old and new paradigms may be informally summarized as

follows. When looking at ’propositions as objects“ one understands ’proofs as functions“, while one

of the possible perspectives suggested by linear logic is the description of ’proofs as actions“. An

action is roughly an operation which modifies its premises, by a sort of ’physical reaction.“ In short,

a step of logical inference modifies the state of the premises: for example, when deducing B from

A, some resource in A is consumed. This is in contrast with classical and intuitionistic logic, which

deal with static situations: if A implies B and A holds, then we deduce B, but A holds as before,

also after the deductive process. Observe that, when ignoring the reaction, one obtains ’proofs as

functions“ again, and thus the new approach may be considered a refinement of the ’propositions as

objects“ analogy.

The proof theoretic description of this difference is based on a rewriting of the structural rules of

deduction. We present next the core of linear logic and refer the reader to references for further

readings or comparisons with other systems in Proof Theory.

Linear Logic is formally a Gentzen-like logic. The calculus of sequences of Gentzen seems a very

suitable formalism for the study of proofs as dynamic actions; indeed the relevance of the structural

rules, which instead play a quite obscure role in natural deduction, for example, allows a better

formalization of the handling of formulas during the inference process, if one wants to focus on its

dynamic aspects. The main difference between linear logic and Gentzen calculus of sequences is just

in these structural rules. In particular, linear logic drops weakening and contraction rules, i.e.,

G |- D G,A,A |- D

__________

and

G, A |- D G,A |- D

Intuitively, formulas can be thought of as resources, and the interpretation of a sequent of the form

A 1 , . . . , An |- B is that of a process (action) which consumes the resourses A1 , . . . , An and

produces B. Thus, resources cannot be freely duplicated or erased; at most, they can be reordered.

Moreover, this lack of structural rules suggests a duplication of the binary connectives of conjunction

and disjunction. Namely, ™ and Ú will be described as „ and È in the ’multiplicative“ case and

80

4. Categories Derived from Functors and Natural Transformations

as Ç and … in the ’additive“ case below. The reason for this is clearly understood, say, in the

introduction and elimination rules for ™ : in the presence of contraction and weakening, Gentzen

calculus does not distinguish between („, r) and (Ç, r), nor between („, l ) and (Ç, l, 1) plus

(Ç, l, 2). Similarly for Ú , which is also described by two connectives, È and … .

In this section, we define and give categorical meaning to the core of ’classical“ linear logic by

suggesting the basic structural properties of suitable categories where the reader may carry on the

details of the interpretation. Other connectives or modalities, essentially the exponential connective

’!“ (of course), will be discussed in section 5.5.

4.4.1 Alphabet

1. atomic propositions, ranged over by A, B, C, . . .

2. logical symbol:

2.1. multiplicative symbols:

constants: 1 (mult. true), ^ (mult. false)

unary connective: ( )^ (linear negation)

bynary connectives: „ (mult. and), È (mult. or), __o (mult. or linear implication).

2.2. additive symbols:

constants: T (add. true), 0 (add. false)

bynary connectives: Ç (add. and), … (add. or).

The well-formed formulae are defined in the obvious way.

Greek capital letters G, D, . . . denote finite (possibly empty) sequences of formulas separated by

commas. The expression G |- D is called sequent.

4.4.2 Axioms and rules

Each set of (nonstructural) axioms and rules below begins with axioms and rules which deal with the

identities relative to the specified connective: 1 for „ , ^ for È , T for Ç , 0 for …. The other

rules are introduction rules.

1. structural rules

(id) A |- A

G |- D

(exc, r) where G', D' are permutations of G, D.

G' |- D'

81

4. Categories Derived from Functors and Natural Transformations

G1|- A, D A, G 2 |- D'

___________________

(cut)

G1, G2 |- D, D'

2. multiplicative rules

G |- D

_______

(1, r) |- 1 (1, l)

G, 1 |- D

G |- D

________

(^, l) (^, l) ^ |-

G |- ^, D

G1|- A, D G2 |- B, D' G, A, B |- D

___________

(„, r) („, l)

G 1, G 2 |- A„B, D, D' G, A„B |- D

G |- A, B, D G1, A |- D G2, B |- D'

___________ ___________________

(È, r) (È, l )

G |- AÈB, D G1, G2, AÈB |- D, D'

G, A |- B, D G1 |- A, D G2, B |- D'

___________ ___________________

( o, r) ( o, l )

G |- A__oB, D G1, G2, A__oB |- D, D'

3. additive rules

(T, r) G |- T, D (0, l) G, 0 |- D

G |- A, D G |- B, D G, A |- D

_________________ (Ç, l, 1) __________

(Ç, r)

G |- AÇB, D G, AÇB |- D

G, B |- D

(Ç, l, 2) _________

G, AÇB |- D

82

4. Categories Derived from Functors and Natural Transformations

G |- A, D

__________

(…,r,1)

G |- A…B, D

G |- B, D G, A |- D G, B |- D

________________

(…,r,2) (…, l)

G |- A…B, D G, A…B |- D

3. linear negation

G,A |- D G |- A, D

_________ ________

(^,r) (^,l)

G |- A^,D G, A^ |- D

As suggested by the rule („, l), the comma in the left hand side of a sequent has the same logical

meaning as „, while the commas in the right hand side correspond to the tensor sum È, the

disjunction which is dual to „.

Observe that the rules (^, r) and (^, l) are equivalent to

G,A |- B,D

____________

(contrap)

G, B^ |- A^,D

1 |- ^^ 1^ |- ^

(^, 1) and (^, 2)

(Hint: 1,^ |- ^ gives both ^ |- 1^ and 1 |- ^^ , while 1 |- 1,^ gives both ^^ |- 1 and 1^ |- ^;

the rest is obvious).

From the rules one may easily derive the following sequents:

(mAB) A,B |- A„B by („, r)

(evalAB) A, A__oB |- B by (__o, l )

In a few steps, one also obtains

(a-1ABC) A„(B„C) |- (A„B)„C .

(aABC) (A„B)„C |- A„(B„C)

83

4. Categories Derived from Functors and Natural Transformations

Exercise Show the logical equivalence of (A„B)__oC and A__o(B__oC). Derive also that A |-

(A^)^ and (A^)^ |- A, i.e. ( )^ is ’dualizing“.

This may be enough to suggest that the categorical meaning of linear logic may be found in particular

symmetric monoidal closed categories, where „ and __o are interpreted by the tensorial product

and the bifunctor Þ given in definition 4.3.5, respectively. Observe that the cartesian product is

needed too, so to provide an interpretation for Ç and its identity T (see later). Negation and all dual

constructions are taken care of by a ’dualizing“ endofunctor (-)*, which is closed in the sense of

4.3.7. Indeed, theorem 4.4.6 below shows that this functor, given „ and Ç , immediately yields

their duals.

4.4.4 Definition A * -autonomous category K is a symmetric monoidal closed category and a

contravariant closed functor (-)*: K ® K such that:

- there exists a natural isomorphism d : Id @ (-)**

- the following diagram commutes (where (-)* is the action of the functor on exponents)

(-)*

A ÞB B*Þ A*

d» _ » d-1 (-)*

A** Þ B**

A *-autonomous category is linear if it is also cartesian.

In other words, a linear category has both a monoidal and a Cartesian structure, „ and Ç , plus a

dualizing functor (-)*.

4.4.5 Proposition Both the vertical and the horizontal arrows in the diagram in definition 4.4.4

are isomorphisms. Moreover,

i. A* @ B* iff A @ B;

ii. A* @ AÞ1*.

Proof By definition, the following diagram commutes and d » _ » d-1 is an isomorphism,

f**

B**

A**

d-1 d

A B

f

84

4. Categories Derived from Functors and Natural Transformations

Then the horizontal (-)*, in the diagram in definition 4.4.4, is a split mono (see section 1.4) and the

vertical one is a split epi. Since the latter is an instance of the former, they are both split monos and

split epis as well and, thus, isomorphisms. In conclusion, AÞB @ B*ÞA*. Finally, A* @ B*

implies A @ A** @ B** @ B and, by exercise 4.3.6.3, A* @ 1ÞA*. Thus, A* @ B* iff A @ B

and, moreover, A* @ A Þ 1*. ¨

4.4.6 Theorem Let K be a linear category. Define

AÈB = (A*„B*)*

A…B = (A*ÇB*)*.

Then È is a dual to the tensor product and … is the coproduct in K. Their identies are ^ = 1* and

0 = T*, respectively.

Proof È is a well-defined dual to „: just compare with definition 4.3.1 (and the remark

afterwards) and note that

- AÈ^ = (A*„1)* @ A** @ A (similarly for the identity to the left),

- (A*„B*)„C* @ A*„(B*„C*) implies (AÈB)*„C* @ A*„(BÈC)* implies

((AÈB)*„C*)* @ (A*„(BÈC)*)* implies (AÈB)ÈC @ AÈ(BÈC) .

As for the Cartesian coproduct, note that, if pA* and pB* are the projections for A*ÇB*, then

their images (pA*)* and (pB*)* via the (-)* functor are the injections for A…B. Finally, AÈ^ =

(A*„1)* @ A and A…0 = (A*ÇT)* @ A. ¨

The results in proposition 4.4.5 and theorem 4.4.6 prove the ’dualizing“ role of the (-)* functor and

of ^ = 1*. In particular, theorem 4.4.6 is a version of De Morgan rules in the semantic structures for

linear logic, when described in categorical terms. Note also that

A*ÈB @ (A„B*)*

@ (A„B*)Þ^

@ AÞ(B*Þ^)

@ AÞ(1ÞB)

@ AÞB

which gives the ’classic“ flavor of this fragment of Linear Logic.

The meaning of linear logic as a deductive system is then given by interpreting each entailment A

|- B as a morphism between the interpretation of the formulas. Linear categories yield such an

interpretation, which we sketch here, by induction on rules. Here are some of the basic cases. Some

crucial ones are simply the properties corresponding to (mAB), (evalAB), (aABC) and (a-1ABC),

given before definition 4.4.4, in monoidal closed categories. As for the others,

the rules are interpreted by the fact that

85

4. Categories Derived from Functors and Natural Transformations

for 1 and ^ 1 and ^ are (the unique) identies for „ and È, which

are expressed by commas, on the left or right, respectively,

of |-.

(„,r) and (È,l) „ and È are bifunctors

(Ç,r) and (…,l) Ç and … have pairing and sum of morphisms

(Ç,l,1) and (Ç,l,2) there exist projections for Ç

(…,r,1) and (…,r,2) there exist injections for …

(contrap) (-)* is so defined in linear categories

(^,^) ^ = 1* and, thus, ^* @ 1 .

(By the argument before 4.4.4, (contrap) and (^,^) are equivalent to (^,r) and (^,l) .)

Example The category Lin of coherent domains and linear maps, in 2.4.2, not only provides an

example of linear category, but it has even been the source of inspiration for linear logic, since linear

functions depend on inputs ’additively“ as deductions from assumptions in this logic. (There is more

than that analogy, though, as this example and section 5.5 should clarify.)

We noticed that Lin is Cartesian in 2.3.7(II). Lin is also co-Cartesian. Indeed, let (|X|,-) and

(|Y|,-) be coherent structures. Define then the coproduct X…Y as the coherent domain associated

with the coherent structure ({(0,z) | zÎ|X|}È {(1,z) | zÎ|Y|},-…), where (a,x)-…(a',y) iff a = a'

and x-y . (Note the difference with the product: the support is the same, but the coherence relation

changes. Give the embedding linear maps for exercise.)

The singleton coherent domain T = 0 = {Æ} , associated with the empty coherent structure, is

both terminal and initial in the category. Indeed, it is the identity for both the product and the

coproduct.

In the previous section we turned Lin into a symmetric monoidal closed category (see exercise

4.3.6). Recall, in particular, that the tensor product A„B is the coherent domain associated with

the coherent structure (|A|´|B|, -„), where (x,y)-„(x',y') iff x-x' and y-y'.

The dual of the tensor product, is È given by the tensor sum AÈB, that is, the coherent

domain associated with the coherent structure (|A|´|B|, -•È), where (x,y)-È(x',y') iff ( (x,y) =

(x',y') or x--x' or y--y'). Also in this case, the tensor product and sum have the same support,

but the coherence relation changes.

Notice that the identity for both the tensor product and its dual is the coherent domain 1 = ^ =

{Æ,{1}}, associated with ({1}, =).

86

4. Categories Derived from Functors and Natural Transformations

As for the contravariant functor (-)* , given a coherent structure (|A|, -), define A* as the

coherent domain associated with (|A|, -*), where x-*y iff ˜(x-y) in A . On a linear function f:

A®B, f*: B*®A* is defined in the following way: (y,x)ÎTr(f*) iff (x,y)ÎTr(f) .

As one could expect (and easily compute), in coherent domains one has T* = 0 = T and 1* = ^

= 1 . Moreover, the equations in theorem 4.4.6 are realized in Lin.

Memo For the reader's convenience, we summarize the identities in linear logic (and linear

categories):

1 for „ ; ^ for È ; T for Ç ; 0 for …

which are interpreted in Lin as 1 = ^ = {Æ,{1}} and T = 0 = {Æ}, with the obvious coherent

structure.

References Textbooks, which stress the applications of Category Theory to computer science

with an algebraic perspective, are Arbib and Manes (1975) and Rydeheard and Burstall (1988).

Goguen and Burstall (1984) contains a survey and references to part of this area, broadly construed,

which ranges from the work in Elgot (1971), to the contributions of the ADJ group (see, at the end of

this volume, the many references which include the names of Goguen, Thatcher, Wagner, or

Wright).

Besides the references to general Category Theory, the reader may consult Barr (1979) and Barr

and Wells (1985) for monoidal categories, monads and their mathematical applications. Further

references, which also discuss Linear Logic, are Barr (1990) and Marti-Oliet and Meseguer (1990).

The recent applications of ’monoidal notions“ we described are borrowed from Moggi (1989), as for

the understanding of programs as ’functions from values to computations“, and from Meseguer and

Montanari (1988) or Degano and al. (1989), as for the examples on Petri nets (see also Marti-Oliet

and Meseguer (1989)).

The main reference for linear logic is Girard (1987). Further work may be found, among others,

in Girard and Lafont (1987), Lafont (1988), DePavia (1987), and Seely (1987), where *-autonomous

categories are proposed for its semantics. Lambek (1968) contains early work on the categorical

significance of logical systems and discusses weakenings of the structural rules.

87

5. Universal Arrows and Adjunctions

Chapter 5

UNIVERSAL ARROWS AND ADJUNCTIONS

In chapter 3, we introduced the notion of functor as a uniform way to describe ’acceptable“

constructions in Category Theory. The reader may have noticed that in some cases, for a given

construction F: C®D, there exists a particular object c in C and an arrow u: F(c)®d , which has

a ’universal behaviour“ with respect to d, in the sense that every other arrow f: F(c')®d uniquely

factorizes through u , i.e., there exists a unique f': c®c' such that f = u ° F(f') or the following

diagram commutes:

Consider for example the product functor _´a: C®C where C is a CCC and aÎObC. The arrow

eval: ba´a®b is universal with respect to b, in the previous sense, since for every arrow f: c´a®b

there exists a unique arrow L(f): c®ba such that f = eval ° L(f), i.e.,

Also the product of two objects may be described in terms of universal arrows. Just take the diagonal

functor D: C®CxC , with D(c) = (c,c) and D(f) = (f,f) and observe that the following diagram

commutes:

88

5. Universal Arrows and Adjunctions

The aim of this chapter is to study the concept of universal arrow outlined above, and some of its

implications. In particular we prove that given a functor F: C®D, if for every dÎD there exists an

universal arrow ud : F(cd )®d, then the function g: ObD ®Ob C that takes d to cd may be

extended to a functor G: D®C. Such a functor G is called (right) adjoint to F. Remarkably, if G

is a (right) adjoint to F, then F is a (left) adjoint to G, in a dual sense, and each one describes the

other up to isomorphism. From another point of view, F and G can be seen as a pair of ’mutually

representable“ functors.

The notion of adjointness is probably the most profound and original contribution of Category

Theory to mathematics. The reader must not expect to understand its relevance upon first reading the

definition, or the few examples and applications in this chapter: only by a systematic use of

adjunctions will she or he become competent on the subject.

5.1 Universal arrows

In addition to the previous remarks, the careful reader has surely noticed that most of the definitions

of the constructions defined in chapter 2 (products, coproducts, terminal object, exponents . . .) have

the following common pattern:

for all . . . there exist a unique . . . such that . . . .

As a matter of fact, all those definitions can be seen as particular cases of a same notion (or its dual):

the universal arrow. For historical reasons, universal arrows are defined dually with respect to the

examples just mentioned (exponents, products . . . ). Couniversal maps, to be defined next, will fit

the examples.

5.1.1 Definition. Let F: C®D be a functor and dÎOb D . Then <u,cd> is universal from d

to F iff uÎD[d,F(cd)], cdÎObC, and "c'ÎObC, "fÎD[d,F(c')], $! f'ÎC[cd,c'] f = F(f')° u .

As usual, this may be equivalently visualized by

89

5. Universal Arrows and Adjunctions

Example <(q1,q2),(a#b,a#b)> is universal from (a,b) to D , where D : C®C´C is the diagonal

functor.

5.1.2 Definition. Let F: C®D be a functor and dÎOb D . <u,cd> is (co)universal from F to

d iff uÎD[F(cd),d], cdÎObC, and "c'ÎObC, "fÎD[F(c'),d] $! f'ÎC[c',cd] f = u ° F(f').

The diagrams and examples in the introduction to this chapter refer this ’dual“ notion. Here are other

interesting examples:

5.1.3 Example Let !C be the unique functor from the category C to the category 1; if id1 = u Î

1[!C(c),1] is universal, then c is terminal in C:

5.1.4 Example Let C be a category of partial morphisms, Ct be the associated category of total

morphisms, and Inc: Ct®C be the embedding functor (see section 2.6). Recall that, by definition,

the lifting of aÎObC is an object a°ÎObC together with a morphism exaÎCt[a°,a] such that for

every fÎC[c,a] , there exists one and only one f'ÎCt[c,a°] satisfying the equation exa ° f' = f .

This says exactly that exa: a°®a is an universal arrow from Inc to a :

90

5. Universal Arrows and Adjunctions

Exercise Define an initial object as a universal arrow from 1 to !C.

5.1.5 Proposition. Let F: C®D be a functor and dÎObD . Assume that <u,c> is universal

from d to F . Then

1. <u',c'> is universal from d to F Þ c @ c' ;

2. c @ c' via (h,h-1) Þ <F(h)° u,c'> is universal from d to F.

Proof

1. $!hÎC[c,c'] $!h'ÎC[c',c] u'= F(h)°u = F(h)°F(h')°u'= F(h°h')°u'. But u' = F(id) °u'.

By unicity, h°h' = id . Similarly, h'°h = id .

2. Exercise. ¨

By the proof of proposition 5.1.5, one even has that the isomorphism is unique. This is a strong

property of universal constructions as a very common tool in mathematics (see the examples below).

It is hard to think of a more suitable language than the categorical one for expressing properties like