. 4
( 10)



We next give two alternative characterizations of the notion of universal arrow: the first one, in
theorem 5.1.6, is of an equational nature; the second one, in theorem 5.1.7, makes use only of the
notion of a natural isomorphism. In a sense, the definition of universal arrow given in definition
5.1.1 is in the middle way: it is based on one equation and on the existence of an isomorphism (does
the reader see any analogy with the various characterizations of products and exponents we have

5.1.6 Theorem Let G: C® D be a functor, dÎ O b D and cd Î O b C . Then there exists
uÎD[d,G(c d )] such that <u,cd > is universal from d to G iff, for every cÎOb C there is an
operation tc: D[d,G(c)]®C[cd,c] such that, for every fÎD[d,G(c)] and every hÎC[cd,c] ,
1. G(tc(f)) ° u = f
2. tc(G(h) ° u) = h

5. Universal Arrows and Adjunctions

(Ü) let <u,cd> be universal from d to G. For every fÎD[d,G(c)] define tc(f) as the unique
arrow f' such that G(f') ° u = f. (1) is then immediate by definition, and (2) follows by unicity.
(Þ) let tc: D[d,G(c)]®C[cd,c] be an operation which satisfies (1) and (2) above. We must
only prove that it is an isomorphism. Define then, for every hÎC[cd,c] tc-1(h) = G(h) ° u ; thus,
we have:
tc-1(tc(f)) = G(tc(f)) ° u = f by (1)
tc(tc-1(h)) = tc(G(h) ° u) = h by (2). ¨

5.1.7 Theorem. Let C, D be locally small categories, G: C®D, dÎOb D and cdÎOb C . Then
there exists uÎD[d,G(cd)] such that <u,cd> is universal from d to G iff C[cd,_] @ D[d,G_] .
(Ü) For c'ÎObC and f'ÎC[cd,c'], set tc'(f') = G(f') ° u Î D[d,Fc'] .
Then t: C[cd,_]®D[d,G_] is a natural transformation, since tc'(g ° h) = G(g ° h) ° u = G(g) ° tc(h).
That is, for gÎC[c,c'], the following diagram commutes:

Moreover, "fÎD[d,Fc'] $!f'ÎC[cd,c'] f = tc'(f') , by definition. Thus, by proposition 3.2.3, t
is a natural isomorphism.
(Þ) Let t : C[cd,_] @ D[d,G_] and set u = tcd(id). Then uÎD[d,G(cd)] . By the naturality of
t, for all c,c'ÎObC , G(g) ° tc(_) = tc'(g°_) and, hence, "fÎD[d,G(c')]
G(tc'-1(f)) ° u = G(tc'-1(f))°tcd(id)
= tc'(tc'-1(f))
That is, "fÎD[d,G(c')] $!f'(= tc'-1(f))ÎC[cd,c'] such that f = G(f')°u . ¨

Exercise: Give the dual version of theorems 5.1.6 and 5.1.7.

Recall now that a functor F : C®Set is representable if there exists a cÎC such that F @ C[c,_]

5. Universal Arrows and Adjunctions

5.1.8 Corollary Let C, D be small categories, G: C®D, dÎOb D and cd ÎOb C . Then there
exists uÎD[d,G(c d )] such that <u,cd > is universal from d to G iff the functor D[d,G_]:
C®Set is representable.

5.2 From Universal Arrows toward Adjunctions
The construction of a universal arrow ud: G(cd)®d from G: C®D to d usually depends on d.
If this construction can always be performed, the function d |_ cd can be extended to a functor F:
D®C. We shall see in the next section that such G and F relate in an important way called
adjunction; for the moment we concentrate on the construction of the functor F.
In this and in the following section, we assume that we are dealing with locally small categories.

5.2.1 Theorem. Let G: C®D be a functor such that "dÎObD $<ud,cd> universal from d to
G Then there exists a functor F: D®C such that
i. F(d) = cd
ii. C[F_,_] @ D[_,G_].
(Note that C[F_,_], D [_,G_] : D op ´C® Set). Moreover, the functor F is unique, up to
Proof: By assumption we know that, for all fÎD[d,d'] ,

Set then F(f) = g, that is, ud'°f = G(Ff))°ud . By the uniqueness property, G(id) = id.
Moreover, by twice the definition of F,

5. Universal Arrows and Adjunctions

And again by unicity of F(h ° f), one then has F(f°h) = F(f) ° F(h).
We need now to define a natural isomorphism j: D[_,G_] @ C[F_,_]. Thus we first need to check,
for a suitable j, that for all gÎD[d',d] and hÎC[c,c'] the following diagram commutes:

1. "fÎD[d,Fc] j(G(h)°f°g) = h°j(f)°Fg .
Now write u (u') for ud (ud', respectively). We know then that "fÎD[d,G(c)] $!f'ÎC[F(d),c]
f = G(f') ° u . Define j(f) = f', that is, f = G(j(f))°u (compare with the definition of F ). j is
clearly a set-theoretic isomorphism; thus, we have only to prove the naturality (1).
By the definition of the functors G and F, the following diagram commutes:

5. Universal Arrows and Adjunctions

That is, G(j(f°g))°u' = G(j(f)°F(g) )°u' , since G is a functor. By unicity,
2. j(f ° g) = j(f) ° F(g) .
Moreover, for all fÎD[d,G(c)],

by the definition of G .
(G(h) ° f ° g) = h ° j(f ° g) by the diagram and unicity
= h ° j(f) ° F(g) by (2).
This proves (1), i.e. the naturality of j , and by proposition 3.2.3 the proof is completed. ¨

Dually, we have the following:

5.2.2 Theorem. Let F: D®C be a functor such that "cÎObC $<uc,dc> universal from F to
c. Then there exists a (unique) functor G: C®D such that
i. G(c) = dc
ii. C[F_,_] @ D[_,G_] .

5. Universal Arrows and Adjunctions

Proof The result follows by duality; anyway we explicitly reprove it, but by using a different
technique from the one used above. As the reader will see, the difference is essentially notational, but
she or he is invited to study both proofs since they are good examples of two common proof styles in
Category Theory.
Let GOb: ObC®ObD be the function defined by GOb(c) = dc, where uc: F(dc)®c is the
universal arrow. We have
"fÎC[F(d),c] $!gÎD[d,GOb(c)] f = uc ° F(g)
Now define, "gÎD[d,GOb(c)] td,c(g) = uc ° F(g) .
For every dÎOb D and cÎOb C , t d,c :D[d,G Ob (c)]® C[F(d),c] is clearly a set-theoretic
isomorphism. Note that, "hÎD[d',d],
1. td',c(g ° h) = uc ° F( g ° h ) = uc ° F(g) ° F(h) = td,c(g) ° F(h)
By taking td,c-1(f) for g in (1), we have td',c( td,c-1(f) ° h ) = f ° F(h), or equivalently,
2. td,c-1(f) ° h = td,c-1( f ° F(h) )
For simplicity, we now omit the indexes of t and t-1 .
Let GMor: MorC ® MorD be the function defined by
"kÎC[c,c'] GMor(k) = t-1(k ° uc) ÎD[GOb(c), GOb(c')]
We want to prove that G = (GOb, GMor) is a functor:
G(idc) = t-1(uc)
= t-1(uc ° idF(G(c)) )
= t-1(uc ° F(idG(c)) )
= t-1( t(idG(c) ) )
= idG(c)
and, for every f: c'®c", k: c®c',
G(f ° k) = t-1( f ° k ° uc)
= t-1(f ° uc' ° F( t-1(k ° uc) ) )
= t-1(f ° uc') ° t-1(k ° uc) by (2)
= G(f) ° G(k)
(1) proves the naturality of td,c in the component d . We have still to prove the naturality in c, that
is, "gÎD[d,GOb(c)], "kÎC[c,c']
3. td,c'(G(k) ° g ) = k ° td,c(g)
We have:
t(G(k) ° g ) = t( t-1(k ° uc) ° g )
= t( t-1(k ° uc ° F(g) ) ) by (2)
= k ° uc ° F(g)
= k ° t(g)
By taking td,c-1(f) for g in (3) we obtain td,c'(G(k) ° td,c-1(f) ) = k ° f , or equivalently:
4. G(k) ° td,c-1(f) = td,c'-1(k ° f).

5. Universal Arrows and Adjunctions

(2) and (4) state the naturality of t-1.
Note that since G must satisfies (4) , then
G(k) = G(k) ° id = G(k) ° t-1(uc) = t-1(k ° uc)
which shows that the adopted definition for G was actually forced. This proves the unicity of the
functor G. ¨

5.2.3 Example An interesting example of application of theorem 5.2.2 refers to Cartesian closed
categories. By the previous section, we know that if C is a CCC, then for all a,b in ObC , (p:
a´b®a, p2: a´b®b) is universal from D to (a,b), and evala,b: ba´a®b is universal from _´a
to b. Then the functions _´_: ObC´ C®ObC and _a : ObC®ObC which respectively take (a,b)
to a´b and b to ba, can be extended to two functors _´_: C´ C®C and _a : C®C. The explicit
definition is the following: for every f: a®c , g: b®d
(_´_)(f,g) = f´g = < f ° p1, g ° p2 > : a´b®c´d
(_a)(g) = L(evala,b ° g) : ba®da
For every object c in C, even the unique arrow !c: c®t may be seen as universal arrow from the
unique functor !C: C®1 to t. In this case, the extension of the function that takes 1ÎOb1 to t
to a functor T: 1®C is trivial, but it is interesting that the existence of the terminal object t in C
may be expressed by the natural isomorphism 1[!C(c)=1 ,1] @ C[c,T(1)=t].

5.2.4 Example Consider C, C t and Inc as in example 5.1.4, and assume that for each object
aÎObC there exists the lifting a°. By example 5.1.4 we know that exa: a°®a is an universal
arrow from the embedding functor Inc: Ct®Cp to a. By theorem 5.2.2 the function _°: ObC®ObC
which takes every object a to its lifting a°, may be extended to a functor _°: Cp®Ct. The explicit
definition of the functor _° on a partial arrow f: b®c is the following
(_°)(f) = f° = t(f ° exb)ÎCt[b°,c°]
where t(f°exa) is the only arrow such that exc ° t(f°exb) = f°exb.
Note that nearly all the facts about partiality and extendability we proved depend directly on
properties of natural transformations and adjunctions. That is, it was not possible to derive the
properties of the lifting of b by assuming just a set-theoretic isomorphism between Cp[a,b] and
C t[a,b°] for all a, as one may be tempted at first thought. The expressive categorical notion of
natural transformation turns out to be essential for these purposes.

5.3 Adjunctions
In this section we derive a general notion from the previous constructions and say that the functors F
and G in theorems 5.2.1 and 5.2.2 are ’adjoint“ to one another. The idea is that an adjunction
establishes a relation between two categories C and D through two functors F: D®C and G:

5. Universal Arrows and Adjunctions

C®D; this relation creates a bijective correspondence j of arrows in the two categories of the kind
described by the following picture:

5.3.1 Definition Let F: D®C and G: C®D be functors. Then an adjunction from D to C is
a triple <F,G,j> such that j: C[F_,_] @ D[_,G_] is a natural isomorphism. F is called left
adjoint of G, and G is called right adjoint of F.

The naturality of the isomorphism j deserves to be spelled out. For any fÎC[F(d),c], kÎC[c,c']
and hÎD[d',d], we have
1. jd,c'(k ° f) = G(k) ° jd,c(f)
2. jd',c(f °F(h) ) = jd,c(f) ° h

5. Universal Arrows and Adjunctions

It is equivalent to require that j -1 is natural, that is, for any gÎC[d,G(c)], kÎC[c,c'] and
3. j-1d,c'(G(k) ° g) = k ° j-1d,c(g)
4. j-1d',c(g ° h) = j-1d,c(g) ° F(h) .

1. Let D, C be partial order categories, and (ObD ,£D ), (ObC ,£C ) the associated p.o.sets. An
adjunction from D to C is a pair of monotone functions f: ObD®ObC, g: ObC®ObD such that,
for every dÎObD , cÎObC,
f(d) £C c Û d £D g(d) .
Consider for example the partial order Z of relative numbers, and the partial order R of real
numbers. Let I: Z®R be the obvious inclusion, and «_»: R®Z be the function that takes a real
number r to its lower integer part «r». Then I and «_» define an adjunction from Z to R , since
1. I(z) £R r Û z £Z «r»
Conversely let ©_ù: R®Z be the function that takes a real number r to its upper integer part ©rù.
Then ©_ù and I define an adjunction from R to Z, since
2. ©rù £Z z Û r £R I(z)
Note that «_» and ©_ù are respectively the right and left adjoint to the same functor I. Note,
moreover, that «_» and ©_ù are the unique functions that respectively satisfy conditions (1) and (2)
for all r and z.
Another interesting example of adjunctions between partial orders as categories is the following:
consider the p.o.set of positive integers N. For every natural number n , let _ .n : N®N be the
function that takes a natural numbers m to the product m.n . The right adjoint to _ .n is the the
function div(_,n): N®N that takes q to (the lower integer part of) q divides n .
Indeed, for every m, q, m.n £ q Û m £ div(q,n)
Analogously the ’minus“ operation is right adjoint to ’plus.“
2. This further example uses familiar notions and applies the categorical understanding of a
fundamental technique in (universal) algebra. Given a category C of structures and a category D of
slightly more general ones, the right adjoint of the forgetful functor from C to D defines the ’free
structures“ over the objects in the category D. This technique is widely explained in several places
(see references), so that we just hint at it here.
The category Graph was defined in the example 4.1.5. Recall now that a graph G is given by:
- a set V of objects (nodes)
- a set T of arrows (edges)
- a function ¶1: T®O which assigns to each arrow f its range ¶1(f)
- a function ¶2: T®O which assigns to each arrow f its target ¶2(f) .

5. Universal Arrows and Adjunctions

Morphisms of graphs G, G' are pairs <f,g>, where f: T®T' and g: V®V' have the properties in
the example 4.1.5. We already mentioned (see the exercise following that example) that each small
category C may be regarded as a graph G = U(C), just forgetting identities and composition. Of
course, U takes objects to nodes and arrows to edges. Moreover, every functor F: C®D gives a
morphisms H = U(F): U(C)®U(D) between the associated graphs; the reader should have checked
that U: Cat ®Graph is actually a (forgetful) functor. Conversely every graph G generates a
category C = C(G) with the same objects of G, and, for arrows, the finite strings (f1,...,fn) of
composable arrows of G, i.e., of arrows in the due types (the empty strings are the identities in
C(G)). Composition in C(G) is just string concatenation, that is,
(f1 , . . . ,fn ) ° (g 1 , . . . ,gm ) = (f1 , . . . ,fn ,g1 , . . . ,gm ) .
Note that (f1,...,fn) = f1 ° . . . ° fn. The category C(G) is called the free category generated by
This construction may be extended to morphisms of graphs: if H: G ® G' then C(H):
C(G)®C(G') is the functor that coincides with H on objects, and that is defined on morphisms by:
C(H)(f 1 ,...,fn ) = (H(f1 ),... H(fn )).
It is easy to prove that C is a functor from Grph to Cat. Actually, we have an adjoint situation, since
there is an isomorphism Q : Cat[C(G), C] @ Grph[G, U(C)] which is natural in G and C. The
isomorphism Q takes every functor F: C(G)®C to the morphism Q(F): G®C, which is the
’restriction“ of F on G. For the nature of C(G), every functor F: C(G)®C is uniquely determined
by its behavior on the arrows of G, indeed if (f1,. . . ,fn) is an arrow in C(G), by definition of a
functor, F((f1,. . . ,fn)) = F( f1 ° . . . ° fn) = F(f1) ° . . . ° F(fn). This proves that Q is injective. But
Q is also surjective, since if H: G®U(C) , we can define a functor F: C(G)®C by F((f1,. . . fn))
= H(f1) ° ... ° H(fn), and clearly Q(F) = H. We leave it to the reader to prove the naturality of the

Exercise In section 4.3 we turned each Petri net N into a monoidal category C„(N) . Describe
C„(N) as a freely generated category.

Exercise Let C and D be discrete categories (i.e., the only morphisms of the categories are
identities). Prove that <G,F,t>: C ® D is an adjunction if and only if G and F define an
isomorphism between C and D.

In the previous section, we have actually shown how to construct an adjunction when one can
uniformly obtain a universal arrow <ud,cd> from each object d . Now we show how to obtain
universal arrows out of an adjunction, and put together the two results.

5.3.2 Theorem. If < F: D®C , G: C®D ,j > is an adjunction from D to C, then
1. < u =j(idF(d)) : d®G(F(d)) , F(d)> is universal from d to G

5. Universal Arrows and Adjunctions

u is called unit of the adjunction
2. <u'=j-1(idG(c)): F(G(c))®c ,G(c) > is universal from F to c
u' is called counit of the adjunction.
Conversely, if G: C®D is a functor and (1) holds (or F: D®C is a functor and (2) holds), then
<F,G,j > is an adjunction from D to C.
Proof. (1) is given by theorem 5.1.6 (Ü) and the definition of G. Note that (2) follows dually. The
converse is stated in theorems 5.2.1 and 5.2.2. ¨

Thus, if < F, G ,j > is an adjunction, then the functor F of theorem 5.2.1 is the left adjoint of G
and, conversely, G in theorem 5.2.2 is the right adjoint of F. In view of the expressive power of the
notion of adjunction, we can now state in one line some of the concepts we introduced in the
previous chapters.

5.3.3 Corollary Let C be a category. Then
i. C has a terminal object iff the unique functor !C: C ® 1 has a right adjoint;
ii. C has finite products iff the diagonal functor has a right adjoint;
iii. C is a CCC iff it is cartesian (i.e., !C: C®1 and D : C®C´C have right adjoints) and, for
each aÎObC, the functor _´a : C®C has a right adjoint.
Proof. Immediate by theorem 5.2.2 and the considerations in example 5.2.3. ¨

5.3.4 Corollary Let C be a category of partial morphisms. The lifting functor _° : C®Ct is the
right adjoint of the embedding functor Inc: Ct®C.
Proof Immediate by 5.2.2 and the considerations in example 5.2.4. ¨

As the reader probably expects, it is also possible to give a fully equational characterization of

5.3.5 Theorem An adjunction <F, G,t> : C®D is fully determined by the following data:
- the functor G: D®C
- a function f: ObC®ObD such that, for every object c of C, f(c) = F(c)
- for every object c of C, an arrow unitcÎC[c, G(f(c))]
- for every object c of C and d of D, a function tc,d-1: C[c,G(d)]®D[f(c),d]
such that, for every hÎC[c,G(d)] and kÎD[f(c),d],
1. G(tc,d-1(h)) ° unitc = h ;
2. tc,d-1(G(k) ° unitc ) = k .

5. Universal Arrows and Adjunctions

Proof The theorem is an immediate consequence of theorems 5.3.2 and 5.1.6. A direct proof is not
difficult, and its study is a good exercise for the reader since it summarizes many of the previous
results. Here it is:
The function f may be extended to a functor F by setting, for kÎC[c,c'], F(k) = tc',d-1(unitc' ° k).
Note that
F(idc) = tc,f(c)-1(unitc)
= tc,f(c)-1(idG(f(c)) ° unitc)
= tc,f(c)-1(G(idf(c)) ° unitc)
= idf(c) . by (2)
and moreover, omitting the indexes for notational convenience,
F(h ° k) = t-1(unit ° h ° k )
= t-1( G(t-1(unit ° h)) ° unit ° k ) by (1)
= t-1( G(t-1(unit ° h)) ° G(t-1(unit ° k)) ° unit ) by (1)
= t-1( G( t-1(unit ° h) ° t-1(unit ° k) ) ° unit )
= t-1(unit ° h) ° t-1(unit ° k) by (2)
= F(h) ° F(k) .
Let now, for every object c of C and d of D, tc,d: D[f(c),d]®C[c,G(d)] be the function defined by
tc,d(k) = G(k) ° unitc . Equations (1) and (2) express exactly the fact that tc,d and tc,d-1 define an
isomorphism. We have still to prove their naturality. Let kÎD[d,d'], hÎC[c,G(d)], h'ÎC[c',c],
and k'ÎD[f(c),d] ; then
nat-1. t-1(G(k) ° h ) = t-1(G(k) ° G(t-1(h)) ° unitc )
= t-1(G(k ° t-1(h)) ° unitc )
= k ° t-1(h) ;
t-1(h ° k ) = t-1(G(t-1(h) ) ° unit ° k )
nat-2. by (1)
= t-1(h) ° t-1(unit ° k ) by (nat-1)
= t-1(h) ° F(k) ;
t(k' ° F(h') ) = t (t-1(t(k')) ° F(k) )
= t (t-1(t(k') ° h') by (nat-2)
= t(k') ° h' ;
nat-4. t(k ° k' ) = G( k ° k') ° unit
= G( k ) ° G(k') ° unit
= G( k ) ° t(k'). ¨

5.3.6 Proposition Let <F,G,t>: C ® D be an adjunction. Then there exist two natural
transformations h : IdC®GF and e: FG®IdD such that, for every c in C and d in D, h(c) and
e(d) are respectively the unit and counit of the adjunction.
Proof: exercise. ¨

5. Universal Arrows and Adjunctions

In other words, one may construct the unit and counit ’uniformely“ and naturally. Observe also
that, if h : IdC®GF and e: FG®IdD are the natural transformations in proposition 5.3.6, then the
following diagram commutes:

The previous diagrams fully characterize an adjunction: as a matter of fact many authors prefer to
define an adjunction between two categories C and D as a quadruple (F, G, h , e) where F:
C®D and G: D®C are functors, and h : IdC®GF , e: FG®IdD are natural transformations
such that
(Ge) ° (hG) = idG ;
(eF) ° (Fh) = idF .
We leave it as an exercise for the reader to prove the equivalence of this notion with the one we have
adopted. We shall use the definition of adjunction as a quadruple in the next section, since it
simplifies the investigation of the relation between adjunctions and monads.

1. An adjointness (F, G, h , e) from C to D is an adjoint equivalence if and only if h and e
are natural isomorphisms. Prove that given two equivalent categories C and D (see section 3.2) it
is always possible to define an adjoint equivalence between them.
2. Given an adjointness (F, G, h, e) from C to D, prove the equivalence of the following
i. hGF = GFh;
ii. hG is an isomorphism;
iii. eFG = FGe;
iv. eF is an isomorphism.

5.3.7 Example In section 3.4 we defined the CCCs of limit and filter spaces, L-spaces and FIL
respectively, which generalize topological spaces, Top. The functorial ’embeddings“ mentioned in
that example are actually adjunctions. Recall that H : Top ® FIL is given by
H((X,top)) = (X,F) where F(x) = {F | F is a filter and "0Îtop (xÎ0 Þ 0ÎF)}.
H(f) = f by the definition of continuity. H has a left adjoint T : FIL ® Top defined by
T((X, F)) = (X,top) where 0Îtop iff "xÎ0 "FÎF(x) 0ÎF .
Also in this case, filter continuity corresponds to topological continuity, i.e., T(f) = f . The reader
may easily define the natural isomorphism t .

5. Universal Arrows and Adjunctions

In general, limits are not unique in filter spaces. A stronger notion of convergence, to be used for
computability (see the final remark in section 8.4), may be given as follows. For (X,F) in FIL
consider (X,top) = T((X, F)) and define
F¯sx iff FÎF(x) and "0ÎFÇtop xÎ0 .
Then top is T0 iff s-convergent filters have a unique limit.
Let N = (w, F) be the natural numbers with the filter structure induced by the discrete topology
and M = NN. With some work (see references) one can show that MM is not topological, i.e. for
no (X,top) one has MM = H((X,top)). The idea is that each topological filter space has a least filter
for each F(x), the neighborhood filter at x; deduce from this that the associated adjointness
(T,H,h,e) to (T,H,t) is not an adjoint equivalence (which one of h and e is not a natural

Exercises (based on the previous example and exercises)
1. Consider the full subcategory of FIL given by the filter spaces (X,F) such that, for each x, there
is a least FÎF(x). Give an adjoint equivalence between Top and this category.
2. Check that the functors between L-spaces and FIL defined in the exercise in section 3.4.2 yield
an adjunction, which is not an adjoint equivalence.
3. Give directly an adjunction between Top and FIL, and compare the definition with the adjunction
obtained by composition of functors. (Hint for the direct construction: given an L-space (X,¯),
define (X,top) by 0Îtop iff "xÎ0, "{xi}¯x, {xi}Í 0 eventually. Conversely, for (X, top)
topological space, define (X,¯) by {xi}¯x iff "0Îtop (xÎ0 Þ {xi}Í 0 eventually).

5.4 Adjunctions and Monads
In this section we study the relation between two seemingly distant concepts as adjunction and
monad. As a matter of fact, every adjunction immediately defines a monad, and conversely every
monad can be thought of as generated by an adjunction, called a resolution for the monad (see
5.4.2 below). Resolutions for a given monad can be build up in a category by introducing a natural
notion of morphism between them; it then happens that the Eilenberg-Moore and the Kleisli
Categories associated with the monad (see definitions 4.2.3 and 4.2.4) are respectively the terminal
and initial object of the category.
The presentation is rather technical; at first reading, the reader may just look at the first theorem,
which will be applied in the next section.

5.4.1 Proposition Let (F, G, h , e) be an adjunction from C to D; then (T = GF, h , m = GeF)
is a monad on C and (T = FG, d = GhF, e) is a comonad.

5. Universal Arrows and Adjunctions

Proof Note first that GF, h, and GeF have the correct types, i.e., T = GF: C®C, h: IdC ®GF,
and m = GeF: GFGF®GF. We must prove the unity and associative laws for the monad.
As for the unity laws we have
m ° Th = GeF ° GFh = G(eF ° Fh) = G(idF) = idGF
m ° hT = GeF ° hGF = (Ge ° hG)F = idG(F) = idGF
For the associative law, note first that
e ° eFG = e ° FGe .
Indeed, for any dÎObD , and letting f = ed: FG(d)®d,
ed ° eFG(d) = f ° eFG(d)
= ed ° FG(f) by naturality of e
= ed ° FG(ed)
Then one has the following:
m ° mT = GeF ° GeFGF
= G(e ° eFG)(F)
= G(e ° FGe)(F)
= GeF ° GFGeF
= m ° Tm .
The rest is an exercise in duality. ¨

5.4.2 Definition Let (T, h , m) be a monad over a category C. A resolution for (T, h , m) is a
category D and an adjunction (F, G, h , e) from C to D such that T = GF and m = GeF. A
morphism between two resolutions (F, G, h , e): C®D and (F', G', h , e'): C®D' (for the
same monad) is a functor H: D®D' such that F' = H ° F, G = G' ° H , and He = e'H.

It is easily proved that resolutions with the associated morphisms form a category. Now we are going
to prove that the Eilenberg-Moore and Kleisli categories associated with a monad (T, h , m) both give
rise to resolutions. In particular, they are respectively the terminal and initial objects in the category of
all resolutions for that monad.

5.4.3 Proposition Let (T, h , m) be a monad over a category C , and let CT be the Eilenberg-
Moore category associated with the monad. Then there exists a resolution for (T, h , m) which is an
adjunction from CT to C.
Proof Let UT: C T®C be the forgetful functor that takes every algebra (c,a) to c, and every
morphism of algebras h to the same h regarded as a morphism in C. Let FT : C®C T be the
functor which takes every object c to its free algebra (T(c),mc), and every morhism f: c®c' to
FT(f) = T(f). Let eT: FTUT®idCT be the natural transformation defined by eT(c,a) = a (note
that a: T(c)=FTUT(c,a)®c). We want to prove that (FT, UT, h , eT) is a resolution for (T, h , m).

5. Universal Arrows and Adjunctions

Obviously UT ° FT = T . UT eT FT = m, since for any object c one has
(UT eT FT)(c) = UT(eT FT(c))
= UT(eT(T(c), mc)) by def. of FT
= UT(mc) by def. of eT
by def. of UT
= mc
We still haveto prove that (FT, UT, h , eT) is an adjunction from CT to C, that is,
(UTeT) ° (hUT) = idUT
(eTFT) ° (FTh) = idFT
One has, for every T-algebra (c,a),
(UTeT ° hUT) (c,a) = UT(eT(c,a) ) ° hUT(c,a)
by def. of eT and UT
= a ° hc
= idc by def. of T-algebra
And for every cÎObC :
(eTFT ° FTh) (c) = eTFT(c) ° FT(hc)
by def. of eT and FT
= mc ° T(hc)
= idT(c) by the unity law of the monad.¨

We say that the resolution (FT, UT, h , eT) from C to the Eilenberg-Moore category CT, and given
by proposition 5.4.3, is associated with CT .

5.4.4 Proposition Let (T, h , m) be a monad over a category C .Then the resolution (FT, UT,
h, eT ): C®C T , associated with the Eilenberg-Moore Category C T , is a terminal object in the
category of all the resolution for the monad (T, h , m).
Proof Let (F, G, h , e): C®D be another resolution for (T, h , m). We must prove that there
exists a unique arrow from (F, G, h , e) to (FT, UT, h , eT). Remember (cf. definition 5.4.2) that
such an arrow is a functor H: D®CT , such that FT = H ° F, G = UT ° H , and He = eTH.
Define, for any object d, and any morphism f of D,
H(d) = (G(d), G(e(d)) )
H(f) = G(f).
Then one has, for any cÎObC, any hÎMorC,
H(F(c)) = (G(F(c)), G(e(F(c))) ) = (T(c), mc) = FT(c)
H(F(h)) = G(F(h)) = T(h) = FT(h)
that proves the equality H ° F = FT.
Moreover, for any dÎObD, and any fÎMorD,
UT(H(d)) = UT(G(d), G(e(d)) ) = G(d)
UT(H(f)) = UT(G(f)) = G(f), as UT is the identity on morphisms.
That proves the equality G = UT ° H .

5. Universal Arrows and Adjunctions

Finally, for any dÎObD,
eTH(d) = eT(G(d), G(e(d)) ) = G(e(d)) = H(e(d))
that proves the equality He = eTH.
We have still to prove that H is the unique morphism from (F, G, h , e) to (FT, UT, h , eT).
Let H' be another morphism; then, for any fÎMorD,
H'(f) = UT(H'(f) = G(f) = UT(H(f) = H(f)
and, for any dÎMorD,
H'(d) = ( UT(H'(d), eTH'(d)) by def. of UT and eT
= ( G(d), H'(eT(d)) ) as G = UT ° H'
= ( UT(H(d), H(eT(d)) ) as H'(f) = H(f)
= ( UT(H'(d), eTH(d))
= H(d).
This completes the proof. ¨

The unique functor to (FT, UT, h , eT) in the category of all resolutions for a given monad (T, h ,
m) is called comparison functor and it is usually denoted by KT.
The category of resolutions of a monad has also an initial object, which is based on the Kleisli
category associated with the monad.

5.4.5 Proposition Let (T, h , m) be a monad over a category C, and let C T be the Kleisli
category associated with the monad. Then there exists a resolution for (T, h, m) that is an adjunction
from CT to C.
Proof: Let UT: CT®C be the functor defined by the following:
for any object c of CT (i.e., of C ), and any morphism hÎCT[c,c'] (and thus hÎC[c,T(c')])
UT(c) = T(c);
UT(h) = mc' ° T(h).
Let FT: C®CT be functor defined by the following:
for any object c of C, and any morphism fÎC[c,c']
FT(c) = c;
FT(f) = hc' ° f ( = T(f) ° hc ).
Let eT: FTUT®id be the natural transformation defined by the following:
for any object c of CT
eT(c) = idT(c) (in C).
We want to prove that (FT, UT, h , eT): C®CT is a resolution for (T, h , m).
Obviously, UT ° FT = T .
Moreover, UT eT FT = m, since for any object c one has
(UT eT FT)(c) = UT(eT (c) ) by def. of FT

5. Universal Arrows and Adjunctions

= UT(idT(c)) by def. of eT
= mc. by def. of UT
We have still to prove that (FT, UT, h , eT) is an adjunction from C to CT, that is,
(UTeT) ° (hUT) = id: UT®UT
(eTFT) ° (FTh) = id: FT®FT
One has, for every object c of CT:
(UTeT ° hUT) (c) = UT(idT(c)) ° hT(c) by def. of eT and UT
= mc ° T(idT(c)) ° hT(c) by def. UT on morphisms
= mc ° hT(c) as T is a functor
= idc. by the unity law of the monad
And, for every cÎObC,
(eTFT ° FTh) (c) = eT(c) ° (hT(c) ° hc) by def. of FT
= idT(c) ° (hT(c) ° hc) by def. of eT
= mC ° T(idT(c)) ° hT(c) ° hc by def. of composition ° in CT
= mC ° hT(c) ° hc
= hc by the unity law of the monad
= idc by def. of the identity in CT. ¨

5.4.6 Proposition Let (T, h, m) be a monad over a category C. The resolution (FT, UT, h , eT):
C®CT associated with the Kleisli Category CT is an initial object in the category of resolutions for
the monad (T, h , m).
Proof Let (F, G, h , e): C®D be another resolution for (T, h , m). We must prove that there
exists a unique arrow from (FT, UT, h , eT) to (F, G, h , e), that is a unique functor K: CT®D,
such that F = K ° FT, UT = G ° K , and KeT = eK.
Define, for any object c of CT, and any morphism fÎCT[c,c'],
K(c) = F(c);
K(f) = eF(c') ° F(f).
where c and f are regarded as object and morphism of C.
Then one has, for any cÎObC, any hÎC[c,c'],
K(FT(c)) = K(c) = F(c)
K(FT(h)) = K(hc' ° h) by def. of FT
= eF(c') ° F(hc' ° h) by def. of K
= eF(c') ° F(hc') ° F(h) as F is a functor
= F(h) as (F, G, h , e) is an adjunction
This proves the equality K ° FT = F .
Moreover, for any object c of CT, and any morphism fÎCT[c,c'],
G(K(c)) = G(F(c)) = T(c) = UT(c)

5. Universal Arrows and Adjunctions

G(K(f)) = G(eF(c') ° F(f)) by def. of K
= G(eF(c')) ° G(F(f)) as G is a functor
= mc' ° T(f) as (F, G, h , e) is a resolution
= UT(f) by def. of UT
that proves the equality UT = G ° K .
Finally, for any dÎObD,
K(eT(c)) = K(idT(c)) by def. of eT
= eF(c') ° F(idT(c)) by def. of K
as F is a functor
= eF(c')
by def. of K
= eK(c')
that proves the equality KeT = eK.
We have still to prove that K is the unique morphism from (FT, UT, h , eT) to (F, G, h , e).
Let K': CT®D be another morphism; then, for every object c of CT,
K'(c) = K'(FT(c)) by def. of FT
= F(c) as K' ° FT = F
= K(FT(c)) as K ° FT = F
= K(c) by def. of FT
and, for any fÎCT[c,c'],
K'(f) = K'(idc' ° f )
= K'(mc' ° hT(c') ° f) by the unitary law of the monad
= K'(mc' ° T(idT(c')) ° hT(c') ° f)
= K'(idT(c') ° (hT(c') ° f) ) by def. of composition ° in CT
= K'(idT(c')) ° K'(hT(c') ° f) ) as K' is a functor
= K'(eT(c')) ° K'(FT(f)) ) by def. of eT and FT
= eK'(c') ° F(f) as K'eT=eK' and F=(K'°FT)
= eF(c') ° F(f) as K'(c) = K(c) = F(c)
= K(f). by def. of K
This completes the proof. ¨

For consistency with the terminology adopted for the comparison functor, we shall denote by KT
the unique arrow from the initial object (FT, UT, h , eT) in the category of all resolutions for a
monad (T, h , m).
Consider now the comparison functor from the initial to the terminal object. Of course, it must be
KT = KT; let us check this explicitly.
For any object c in CT,
KT(c) = (UT(c), UT(eT(c)) ) by def. of KT
= (T(c), mc ° T(idT(c)) ) by def. of UT and eT

5. Universal Arrows and Adjunctions

= (T(c), mc)
= FT(c) by def. of FT
= KT(c). by def. of KT
And for any morphism fÎCT[c,c'],
KT(f) = UT(f) by def. of KT
= mc' ° T(f) by def. of UT
= eT(T(c'), m(c')) ° T(f) by def. of eT
= eTFT(c') ° FT(f) by def. of FT
= KT(f) . by def. of KT

1. Prove that the comparison functor KT = KT : CT®CT is full and faithful.
2. Prove that the Kleisli Category is isomorphic to the full subcategory of CT consisting of all free

5.5 More on Linear Logic
In this section, we complete an introductory presentation of linear logic and its categorical meaning,
initiated in section 4.4. As already mentioned, the leading idea of this system refers to the ’linear“ use
of ’resources“ or logical assumptions. From assuming A, one derives less than from assuming A, A,
i.e., twice A . The logic-oriented reader, mostly used to classical or intuitionistic reasoning, may find
this a little strange. Probably, though, this habit hides a nonconstructive view which may result in a
limitation of our understanding of effective processes. Indeed, the alternative approach proposed by
linear logic, which enriches and complements the traditional ones, seems to suggest formalizations
and understanding of processes, such as parallel ones, which have so far escaped to a description by
usual tools (see the examples on monoids and Petri nets in section 4.3 and the references, for recent
developments of this idea).
As the reader may recall, the changes in the structural rules motivate a duplication of the
connectives (see section 4.4). However, there is a way to recover the usual possibility, in classical as
well as in intuitionistic logic, of an iterated use of assumptions. The idea is to introduce a connective
’!“ (read ’of course“), which allows to assume as (finitely) many times one wishes a given
assumption. This connective has a categorical meaning, which may be given in the terms of
adjunctions and monads, following the previous section. The interesting categorical significance of
this relation to classical and intuitionistic logic, as well as the categorical understanding we described
in section 4.4, via structures such as the categories Stab and Lin, is probably what makes the
difference between linear logic and previous formal experiments with the structural rules in other
areas of logic.

5. Universal Arrows and Adjunctions

The rules below are meant to extend the system in section 4.4. Observe that the structural rules of
weakening and contractions apply with respect to the connective !. This is exactly what it is
introduced for: it is meant to allow copies of assumptions and observe that they lead to the same
consequences. This is expressed also by the rules (!,r) and (!,l) . Following Girard•s work, we
explicitly introduce the dual ’?“ (read ’why not“), of the connective ! . Its operational behaviour is
described by the rules, which mimic those for ! on the other side of the entailment (cf. the duality of
(-)^ in 4.4.3), and by the equivalence of !A and (?(A^))^, proved below.
The exponential fragment of Linear Logic is as follows:

5.5.1 exponential unary connectives: ! (of course), ? (why not)

5.5.2 exponential rules

G |- D G |- D
________ ________
(weak-l) (weak-r)
G,!A |- D G |- ?A,D

G,!A,!A |- D G |- ?A,?A,D
___________ ___________
(contr-l) (contr-r)
G,!A |- D G |- ?A,D

G, A |- D !G |- A,?D
________ ________
(!,l) (!,r)
G,!A |- D !G |- !A,?D

!G, A |- ?D G |- A,D
_________ _______
(?,l) (?,r)
!G,?A |- ?D G |- ?A,D

The duality between ! and ? is easily obtained by the following deductions:

A |- A A |- A
_______ _______
(!,l) (^,r)
|- A^, A
!A |- A
_______ _______
(^,l) (?,r)
!A, A^ |- |- ?A^, A
_________ ________
(?,l ) (!,r)
!A, ?A^ |- |- !A,?A^
__________ __________
(^,r) (^,l)
!A |- (?A^)^ (?A^)^ |- !A

5. Universal Arrows and Adjunctions

Exercise Prove that !(AÇB) |- !A „!B and !A „!B |-!(AÇB).

5.5.3 Remark The connective ’!“ is exactly what is needed to recover the intuitionistic calculus: it
is possible to prove that there is an embedding of intuitionistic (and classical) logic into linear logic.
The embedding maps every intuitionistic formula A to a linear formula A in the following way:
A=A if A is an atomic formula
A™B = A Ç B
A•ÚB = !A … !B
A•ÞB = ! A __o B
( ! is supposed to bind tighter than __o and È ).
The absurdum F of intuitionistic is translated into 0, the identity for … . Thus ˜A = !A__o0.
In other words, the iterated use of the premises, in a linear implication, gives exactly the intuitionistic
implication. Then, if, G |-i A, in intuitionistic Logic, then ! G |- A in Linear Logic.

Our aim now is to give categorical meaning to the connective !, of course. By duality, in linear
categories (see definition 4.4.4), we also obtain an interpretation for ?, why not.
We have already remarked that a resource such as !A can be duplicated and erased, and in a
sense these properties characterize the meaning of the connective ! . Thus, at the sematic level, we
expect to have two morphisms d: !A®!A „!A , and e: !A®1 where 1 is the identity of the
monoidal category. (Commutative) comonoids in 4.3.4 seem the right structure for this, as they are
characterized by a sort of diagonal map, such as d, and a map e which dualizes the map h in
definitions 4.2.1 and 4.3.3.
We start then with a monoidal category C. By definition, C must satisfy certain natural
isomorphisms, given in 4.3.1, which we rebaptize in this section, for convenience, with more
suggestive names
1. assoc: X „ ( Y „ Z ) @ ( X „ Y ) „ Z
2. ins-l: X @ 1 „ X
3. exch: X „ Y @ Y „ X
Let also:
4. ins-r = exch ° ins-l : X @ X „ 1
As mentioned in section 4.4, the connective of linear implication __o is interpreted by the right
adjoint to the tensor product „ , when C is a monoidal closed category, as defined in section 4.3.
Recall that the category CoMonC of commutative comonoids over a monoidal category C, has
as objects, for c in C, (c, d: c®c„c, e: c®1), and morphisms f: (c, d, e)®(c', d', e'), for each
arrow f: c®c' in C , such that
d' ° f = (f„f) ° d : c®c'„c',
e' ° f = e: c®1 .

5. Universal Arrows and Adjunctions

Given a commutative comonoid (c, d: c®c„c, e: c®1) observe that the following equations hold:
(e„idc) ° d = ins-l : c®1„c
exch ° d = d : c®c„c
assoc ° (idc„d) ° d = (d„idc) ° d : c®(c„c)„c .

Exercise As pointed out after definition 4.3.6, if C is Cartesian, in the sense that „ is actually a
cartesian product Ç and the isomorphisms are the canonical ones, then all the maps and
isomorphisms above can be constructed for each object in C (in particular, recall that d and e are
canonically given; namely, d = <id,id> : c®cÇc is the diagonal and e: c®t is the unique map to
the terminal object). Prove that, if C is Cartesian, then C is actually isomorphic to CoMonC. Does
the converse hold?

5.5.4 Definition A ! - model is a linear category C and a comonad (!,D,E) such that there
exist natural isomorphisms
I : !(AÇ B) @ !(A)„!(B)
J : !t @ 1
where t and 1 are the identities for Ç and „ , the Cartesian and tensor products in C.

Indeed, by definition, in a linear category one has both a monoidal and a Cartesian structure. The
relation established by the natural isomorphisms gives the monoids we need.

5.5.5 Lemma Let <C,(!,D,E)> be an !-model. Then, for each object c in C, there exist maps
d':!c®!c„!c and e': !c®1, such that (!c, d', e') is a comonoid.
Proof. Just set d'= I»!d : !c ®!(cÇc) ®!c„!c
e'= I»!e : !c ® !t ®1
where d = <id,id> : c®cÇc and e: c®t are the monoidal maps in the remark above, w.r.t. the
Cartesian product Ç. The rest is easy.¨

Thus, the comonad (!: C®C, D: !®!° !, E: !®Id C ) associated with a !-model gives all the
ingredients for the interpretation of the connective !, of course. In view of the above lemma, we can
define the functor !: C ® CoMonC by
!(c) = (!c, d':!c ®!c„!c, e': !c ®1) .
This gives the required monoids, while the natural transformations D and E uniformly yield maps
Dc : !c ®!°!c and Ec : !c ®c, which are needed to interpret the rules in (!,r) and (!,l).
We already mentioned in section 4.4 that the idea of the interpretation relies on viewing
entailments as morphisms. In short, observe that, with an informal blend of syntax and semantics,

5. Universal Arrows and Adjunctions

the rules are interpreted by the fact that

(weakenings) each morphism f: 1®D
gives a morphism f»ea: !a®D

(contractions) each morphism f: !a„!a®D
gives a morphism f»da: !a®D

(!,l) each morphism f: a®D
gives a morphism f»Ea: !a®D

(!,r) each morphism f: !c®a
gives a morphism !f»Dc: !c®!a .

As for the rules which contain ?, their meaning is easily derivable by duality. The idea is to define a
functor ? : C®C by
that is ?A = (!A*)*. Then the following theorem gives the categorical meaning of the modality ?,
why not.

5.5.6 Theorem Let <C,(!,D,E)> be an !-model. Then there exist a monad (?, D': ?» ?®?, E':
Id®?) and natural isomorphisms
I': ?(A…B) @ ?(A)È?(B)
J': ?0 @ ^ ,
where 0 and ^ are the identities for … and È, the duals of the Cartesian and tensor products in
Proof. Set ? = * » ! » * : C ® C and, for each object A, D'A = (DA*)* and E'A = (EA*)*. As
D: !®!°!, one has
DA*: !A*®!°!A*
(DA*)*: (!°!A*)*®(!A*)* by def.of (-)*
(DA*)*: (!°*°*°!A*)*®(!A*)* by Id @ (-)**
D'A: ?°?A®?A
Each of these steps is an isomorphism, uniform in A, and gives a natural transformation D': ?»?®?.
Similarly, from E: !®Id C one has EA* : !A*®A* and, thus, E'A = (EA* )*: A®?A. The
properties required for a monad follow by duality.
As for the natural isomorphisms, compute
?(A…B) = * » ! » *(A…B)
= * » !(A*ÇB*) by theorem 4.4.6

5. Universal Arrows and Adjunctions

@ (!(A*)„!(B*))* by def. of !-model
= ?AÈ?B by theorem 4.4.6.
Finally, ?0 = * » ! » *0 @ * » ! t @ 1* @ ^ , by definition and theorem 4.4.6. ¨

Exercise Endow a structure of monoid over each object in a monoidal category whose tensor
product is actually a Cartesian coproduct. Then give the details of the interpretation of the rules for ?.

Next we find, within any categorical model of linear logic, an interpretation for the intuitionistic
connectives Ç and Þ, by using the comonad construction in the !-model. Namely, given an !-
model C, one may interpret intuitionistic ’and“ and ’implication“ by Cartesian product and
exponential in a suitable category derived from C. As the purpose of the iterator ! was to take us
back to intuitionistic logic, we use its categorical meaning to construct this new category.
As a matter of fact, in the remark 5.5.3, we hinted how to derive intuitionistic connectives from
linear ones, once the connective ! is available. The following result gives the categorical counterpart
of that construction.
Observe that in general, given a comonad (T, d, e) over C, the co-Kleisli category K is the
category whose objects are those of C, and the set K[A,B] of morphisms from A to B in K is
C[T(A),B]. The identity in K[A,A] is eA: T(A)®A. The composition of fÎK[A,B] and gÎK[B,C]
in K is
gof = g ° T(f) ° dA : T(A)®T2(A)®T(B)®C
(see definition 4.2.4 where Kleisli categories over monads were defined).

5.5.7 Theorem If C be an !-model. Then the co-Kleisli category K associated with the comonad
(!,D,E) is Cartesian closed.
Proof (hint) The exponent of two objects B and C is (!B__oC). We then have the following
chain of isomorphisms:
K[AÇB, C] @ C[!(AÇB), C] by definition of K
@ C[!(A)„!(B), C] as !(AÇB) @ !(A)„!(B)
@ C[!(A), !B__oC ] as C is monoidal closed
@ K[A, !B__oC ] by definition of K. ¨

Example In section 2.4.2 we defined the category Stab of coherent domains and stable functions.
In that section (see exercise 4) the subcategory Lin, with linear maps, was also introduced and, later
(see section 4.4), it was given as an example of linear category. We also defined a function ! on
coherent domains as follows: if X is a coherent domain, then !X is the coherent domain defined by:
i. |!X| = {a / aÎX, a finite};
ii. a-b [mod !X] iff aÈbÎX.

5. Universal Arrows and Adjunctions

We need now to extend it to a functor ! : Stab®Lin. Recall that a linear map g: Z®Z' is uniquely
determined by its behavior on the points of the coherent domain Z, i.e., on the elements of |Z|.
Moreover, any stable map may be equivalently described in terms of its trace. Set then, for each
stable map f : X®Y,
Tr(!f) = {({a}, b) | bÎY, b finite, aÎX, a finite and least such b Í f(a) }.
Next, we define an adjunction between ! and the obvious inclusion functor Inc from Lin into
Stab. This is given by a natural isomorphism
(iso) j : Lin[!A,B] @ Stab[A,B]
where the inclusion functor is omitted.
Once more we use traces, that is, for each gÎLin[!A,B] set
Tr(j(g)) = {(a, y) | ({a}, y)ÎTr(g) } .
The reader may prove for exercise the naturality of j. In particular, the unit and counit of the
adjunction are given, as usual, by
hA = j(id!A) : A®!A where Tr(hA) = {(a, a) | aÎA finite }
eA = j-1(idA) : !A®A where Tr(eA) = {({x}, x) | xÎ|A| }.

Exercise Check, by actual computations in the structure, that !f = j-1(hA»f) and f = j(eA»!f).

Following theorem 5.4.1, (!, Inc, h, e) yields a comonad
(! = !»Inc: Lin®Lin, D = !hInc: !®!°!, E = e: !®IdC )
as required to turn Lin into an !-model. Moreover, it is a matter of a simple observation on the
’hardware“ of coherent domains to show that the isomorphisms needed to complete the definition
hold in Lin, namely, that !(AÇB) @ !(A)„!(B) and !t @ 1 are uniformly valid in this model (see
the example in section 4.4).
Interestingly enough, by (iso) above, Stab is the co-Kleisli category associated with the
comonad (!, D, E) on Lin.

We conclude this section by identifying a class of categories which yield an interesting interpretation
of the modality ! . The idea is to interpret !A as the commutative comonoid freely cogenerated by A,
not just as a comonoid in the intended linear category.

5.5.8 Definition Let C be a linear category and U: CoMonC®C be the forgetful functor which
takes (c, d, e) to c. Then C is a free !-model if there exists a right adjoint to U, that is a functor
! : C®CoMonC and a natural isomorphism W: C[c,a] @ CoMonC[(c,d,e), !(a)] .

We need to show that free !-models are indeed !-models. This follows from the simple, but
powerful, adjointness property stated in 5.5.8. As already recalled, by proposition 5.4.1, each

5. Universal Arrows and Adjunctions

adjunction yields a comonad. We explicitly reconstruct the units and counits as they bear some

5.5.9 Lemma Let C be a free !-model and <U,!,W > be the given adjunction. Then, for ! =
U°!, there exist natural transformations D: !®!°! and E: !®IdC such that
(!: C®C, D: !®!°!, E: !®IdC )
is the comonad associated with C, in the sense of proposition 5.4.1.
Proof By the definition of morphism in CoMon C , for every hÎC[c,a], the morphism W(h)Î
CoMonC[(c,d,e),!(a)] satisfies the following equations:
hom-1. da ° W(h) = ( W(h)„W(h) ) ° d : c®!a„!a ;
hom-2. ea ° W(h) = e : c®1 .
Moreover, the naturality of W is expressed by the following equations:
for every hÎC[c,a] , fÎC[a,b] , gÎCoMon C [(c',d',e'), (c,d,e)] :
nat-1. W(f ° h) = !(f) ° W(h) ;
nat-2. W(h ° U(g)) = W(h) ° g .
The counits of the adjunction (W, U, !): CoMon C ®C, are arrows E c=W -1(id!(c)): !c®c. By
equation (nat-1) above, for h = Ec, we obtain !(f) = W(f ° Ec), and by equation (nat-2), Ec ° U(W(h))
= h . The family of arrows {Ec}cÎC defines a natural transformation E: (U ° !)®I. Dually the
units of the adjunction define a natural transformation H : I®(! ° U), where: H(c,d,e) = W(idc) :
(c,d,e)® !c. The adjunction between CoMon C and C is thus equivalently expressed by the
parameters (U, ! , H: I®(! ° U), E: (U ° !)® I ).
Remember now that a comonad over a category C is a comonoid in the category of endofunctors
from C to C (with composition as product, see 4.2.2).
By proposition 5.4.1, every adjunction (F, G, h: IdC ®G °F, e: F °G®IdC' ) from C to C'
determines a comonad (T = F°G, d = FhG: T® T°T, e : T®IdC') over C'.
In particular the adjunction (U, ! , H: I®(! ° U), E: (U ° !)® I ): CoMon C ®C, defines a
comonad (! = U ° ! , D = UH! : ! ® ! ° ! , E : ! ®IdC ) over the !-model C. ¨

Finally we derive the natural isomorphisms in definition 5.5.4.

5.5.10 Theorem Let C be a free !-model and (!: C®C, D: !®!°!, E: !®IdC) be the comonad
associated with it by the lemma. Then there exist natural isomorphisms
I: !(AÇB) @ !(A)„!(B)
J: !t @ 1
where t and 1 are the identities for Ç and „ , the Cartesian and tensor products in C.
Proof Consider the comonoid (!(A)„!(B),d,e) where
d = mix ° (dA„dB) : !(A)„!(B) ® (!(A)„!(B))„(!(A)„!(B))

5. Universal Arrows and Adjunctions

e = ins-r-1 ° (eA„eB) : !(A)„!(B) ® 1
mix : (!(A)„!(A))„(!(B)„!(B)) ® (!(A)„!(B))„(!(A)„!(B))
is the obvious isomorphism.
Then, by hypothesis, we have an isomorphism
W: C[!(A)„!(B),AÇB] @ CoMonC[ (!(A)„!(B),d,e), !(AÇB) ]
The isomorphism IA,B from !(AÇB) to !(A)„!(B), which we write I for short, is given by
I = (!fst „!snd) ° dAÇB : !(AÇB) ® !(A)„!(B)
Note that I is a morphism of comonoids, that is, as it is easily verified,
d ° I = (I„I) ° dAÇB
e ° I = eAÇB
The inverse image of I is defined in the following way.
k1 = EA ° ins-r-1 ° (id!A „ eB): !(A)„!(B)®A
k2 = EB ° ins-l-1 ° (eA „ idB): !(A)„!(B)®B
k = <k1, k2> : !(A)„!(B)®AÇB
Then the inverse image of I is U(W(k)) = W(k) : !(A)„!(B)®!(AÇB), indeed:
W(k) ° I =
= W(k ° I) by (nat-2)
= W( <k1, k2> ° I ) by def. of k
= W( <k1 ° I, k2 ° I >)
= W( <EA°ins-r-1°(id!A„eB)°(!fst„!snd)°dAÇB, EB°ins-l-1°(eA„idB)°(!fst„!snd) ° dAÇB >)
by def. of k1, k2 and I
= W( <EA°ins-r-1°(id!A„eA)°(!fst„!fst)°dAÇB, EB°ins-l-1°(eB„idB)°(!snd„!snd) ° dAÇB >)
as eB°!snd = eAÇB = eA°!fst
= W( < EA ° ins-r-1 ° (id!A„eA) ° dA ° !fst, EB ° ins-l-1 ° (eB„idB) ° dB ° !snd >)
as !fst and !snd are comonoid morphisms
= W( < EA ° !fst, EB ° !snd >) by properties of comonoids
= W( < fst ° EAÇB, snd ° EAÇB >) by naturality of E
= W( EAÇB)
= id!(AÇB) . by def. of E

I ° W(k) =
= (!fst „!snd) ° dAÇB ° W(k)
= (!fst „!snd) ° ( W(k)„W(k) ) ° d by (hom-1)
= (!fst ° W(k) )„(!snd ° W(k) ) ° d

5. Universal Arrows and Adjunctions

= ( W( fst ° k) )„( W( fst ° k) ) ° d by (nat-1)
= ( W(k1) )„( W(k2) ) ° d by def. of k
= ( W( EA ° ins-r-1 ° (id!A „ eB) )„( W(EB ° ins-l-1 ° (eA „ idB) ) ° d
by def. of k1 and k2
= ( ins-r-1 ° (id!A „ eB) )„( ins-l-1 ° (eA „ idB) ) ° d
by (nat-2) and def. of E
= ( ins-r-1 ° (id!A „ eB) )„( ins-l-1 ° (eA „ idB) ) ° mix ° (dA„dB)
by def. of d
= ( ins-r-1 ° (id!A „ eA) )„( ins-l-1 ° (eB „ idB) ) ° (dA„dB)
by application of mix
= ( ins-r-1 ° (id!A „ eA) ° dA )„( ins-l-1 ° (eB „ idB) ° dB)
by properties of comonoids
= id!(A)„id!(B)
= id!(A)„!(B) .

The construction is clearly uniform in A and B.
As for the natural isomorphism J, note that !A @ !(AÇt) @ !A„!t , !A @ !(tÇA) @ !t„!A and
that the right and left identity, in a monoidal category, are unique. ¨

References Universal arrows and adjunctions are fundamental notions in Category Theory.
Their treatment, in various forms, and references to their origin may be found in all textbooks we
mentioned in the previous chapters. References for Linear Logic have been given in chapter 4.

6. Cones and Limits

Chapter 6


In chapter 2, we learned how common constructions can be defined in the language of Category
Theory by means of equations between arrows of given objects. In chapter 4, we saw that those
definitions were based on the existence of an universal arrow to a given functor. The category-
theoretic notion of limit is merely a generalization of those particular constructions, as it stresses their
common universal character. From another point of view, the limit is a particular and important case
of universal arrow, where the involved functor is a ’diagonal,“ or ’constant“ functor, as we shall
see. To help the reader become confident with this new notion, we begin this chapter by looking back
at the constructions of chapter 2 and we regard them as particular instances of limits. Then we study
some relevant properties concerning existence, creation, and preservation of limits. As for computer
science, limits have been brought to the limelight mainly by the semantic investigation of recursive
definition of data types: this particular application of the material in this chapter will be discussed in
chapter 10.

6.1 Limits and Colimits
The concept of limit embodies the general idea of universal construction, that is, of an entity which
has a privileged behavior amongt a class of objects that satisfy a certain property. The only way to
define a property in the categorical language is by specifying the existence and equality of certain
arrows, that is, essentially by imposing the existence of a particular commutative diagram amongt
objects inside the category.

6.1.1 Definition A diagram D in a category C is a directed graph whose vertices iÎI are
labeled by objects di and whose edges eÎE are labeled by morphisms fe.

A diagram D in C is similar to a subcategory of C; however, it does not need to contain identities,
nor must it be closed under composition of morphisms.
More formally, a diagram in a category C should be defined as a graph homomorphism D
from an index graph I to the (graph underlyng the) category C . Such a diagram is called ’of type
I“. For the adjunction between graphs and categories, this is exactly the same as a functor from the
category I freely generated by the graph I (the index category) to C. A graph is called small when
the index category is small.

6. Cones and Limits

6.1.2 Definition. Let C be a category and D a diagram with objects di, iÎI . Then a cone to
D is an object c and a family of morphisms {fiÎC[c,di] | iÎI } such that
"i,jÎI "eÎE feÎC[di,dj] ’Þ fe ° fi = fj .

A cone may be visualized by

Cocones are defined dually.

Example In a partial order P, cones correspond to lower bounds, cocones to upper bounds.

Note now that, given a diagram D, the cones to D form a category, call it ConesC,D . Just take
as morphisms from (c,{fiÎC[c,di] | iÎI}) to (c',{hiÎC[c',di] | iÎI}) any gÎC[c,c'] such that
"iÎI hi ° g = fi. That is,

Clearly, ConesC,D is a category. Dually one defines the category CoconesC,D .

6.1.3 Definition. Let C be a category and D a diagram. Then a limit for D is a terminal object
in Cones C,D . Colimits are defined dually.

(c,{fiÎC[di,c] | iÎI}) is the initial object in CoconesC,D, it may be visualized by the following
commutative diagram:

6. Cones and Limits

Limits are also called universal cones, as any other cone uniquely factorizes via them. Dually,
colimits are called universal cocones.

1. Let P be a partial order. Then limits correspond to greater lower bounds, while colimits
correspond to least upper bounds.
2. Let D = ({di}iÎw, {fiÎSet[di, di+1]}iÎw ) be a diagram in Set such that di Í di+1, and fi =
incl (the set-theoretic inclusion). Then the colimit of d0 ®.......di ® di+1 ®..... is È{d i}
(exercise: what is the limit of the same diagram?) .

Exercise Prove that the colimits in C are the limits in Cop of the dual diagram.

Consider now a diagram as a functor from an index category I to C. Note first that any object c
of the category C is the image of a constant functor Kc: I®C, and so Kc can be regarded as a
degenerate diagram of type I in C. Once diagrams are defined as functors, it makes sense to
consider natural transformations between diagrams. If D and D' are two diagrams of type I, a
natural transformation from D to D' is a family of arrows fi indexed on objects in I such that for
each arrow e in I (each edge of the graph of type I)

A cone for a diagram D of type I from an object c is then a natural transformation from the
constant diagram Kc to D

6. Cones and Limits

Dually, a cocone for a diagram D of type I to an object c is a natural transformation from D to
the constant diagram Kc .

6.2 Some Constructions Revisited
Let D be an empty diagram, that is a diagram with no objects and no arrows. By definition, a cone
in C to D is then just an object c of C, with no other structure (and every object of C can be seen
as a cone). A limit for the empty diagram is then an object t such that for any other object c there is
exactly one arrow from c to t, i.e., it is a terminal object. Dually, the initial object is the colimit
of the empty diagram.
A graph is called discrete if it has no arrows. For example the set {1,2} can be regarded as a
discrete graph. A diagram of type {1,2} in a category C is an ordered pair of objects, (c1,c2). A
limit for such a diagram is an object d, together with two arrows f1: d®c1 and f2: d®c2, such
that for any other cone (d',{giÎC[d',ci] | iÎ{1,2} }) there exists exactly one arrow h: d'®d, with
fi ° h = gi for iÎ{1,2}.

But this is just the definition of product d of c1 and c2 with f1 : d®c 1 and f2 : d®c 2 as
Dually, the coproduct ci#cj, if it exists, is just the the colimit of the diagram {ci,cj}.
The product of any indexed collection of objects in a category is defined analogously as the limit
of the diagram D: I®C where I is the index set considered as a discrete graph. This product is
usually denoted by PiÎIDi, although explicit mention of the index set is often omitted.
Consider the graph I with two vertices and two edges

A diagram of type I in a category C is a pair of objects, a and b, and a pair of parallel arrows
f,gÎC[a,b]. A cone for this diagram consists of an object d, and two arrows hÎC[d,a] and
kÎC[d,b] such that g ° h = k and f ° h = k. A limit is a cone (d,{h,k}) that is universal, that is,
for any other cone (d',{h',k'}) there exists exactly one arrow l: d'®d such that h ° l = h', and k °
l = k'.

6. Cones and Limits

Note now that the existence of two arrows, h and k, such that g ° h = k and f ° h = k, is
equivalent to the existence of an arrow h such that g ° h = f ° h. Moreover, h ° l = h' implies k ° l =
k', since k ° l = f ° h ° l = f ° h' = k', thus the above limit is just the equalizer of f and g .
Dually, coequalizers are the colimits for the same diagram.
Consider now the following graph:


. 4
( 10)