<<

. 3
( 10)



>>

Proof. The terminal object is the functor T : Cop®Set, which takes every object c in ObC to the
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

<<

. 3
( 10)



>>