What is a categorical model for Linear Logic?
Andrea Schalk
Department of Computer Science
University of Manchester
October 15, 2004
The aim of these notes is to give an outline of the categorical structure required for a model
of linear logic. That means that we only try to motivate the various conditions imposed on
such models; this is by no means intended to be a full account. For intuitionistic linear logic a
detailed description of the process of defining such a model can be found in Gavin Bierman’s
thesis [Bie94]. There are a number of exercises in these notes, they either aim to give examples
for the various notions defined or they state minor results that are used subsequently and
which hopefully are not too difficult to establish. If the category theory in these notes is too
advanced you may want to try [BS] which does not assume any knowledge in that area at all,
but proceeds fairly rapidly to the notions we use here.
Originally these notes were written for my PhD students, but since I made the first version
available on my webpage a number of people have told me they found them useful. As a result
I felt obliged to to add details which were rather sketchy in the original account. In particular
the account now contains more proofs and so I am hopeful that the various formulations of
the notion of linear exponential comonad are finally correct. I would like to thank Paola
Maneggia, Peter Selinger, Robin Houston and Nicola Gambino for useful feedback on these
notes.
1
Intuitionistic linear logic
When modelling any logic there has to be a valuation telling us how to interpret any variables
or literals. In the case of categorical logic, each variable is so interpreted as an object in the
modelling category. We take valuations for granted from now on.
When people talk about intuitionistic linear logic they often mean the calculus with the
connectives ⊗, (, u and !, and this is the system we will be referring to when using that
name. Since there is no negation, the De Morgan duals of these can not be defined within this
system. Further the system only allows onesided judgements to be made. For a full discussion
of the rules see Bierman’s thesis [Bie94], for a summary of the categorical structure of models
for linear logic, [Bie95].
MILL—the multiplicative fragment
The rules for this fragment are given in Table 1, with the exception of the exchange rule which
allows the exchange of any two neighbouring formulae in a sequent Γ.
Exercise 1 Compare this system to N{→, u}, a natural deduction system for implication
and conjunction. What are the differences, what the similarities? Can you deduce some
categorical structure suitable for modelling the above from this?
1
Identity
Multiplicative connectives
left
right
Γ, A, B ` C
Γ`A
Γ, A ⊗ B ` C
Cut
∆`B
Γ, ∆ ` A ⊗ B
Γ`A
A`A
Γ`A
∆, B ` C
A, ∆ ` B
Γ, ∆ ` B
Γ, A ` B
Γ, ∆, A ( B ` C
Constants
`I
Γ`A(B
Table 1: Rules for MILL.
Given a formula A we have to define an object of the category, which is usually denoted
by [[A]]. The only way we have so far of building new formulae is to apply ⊗, so we want our
category to support an operation which we also refer to as ⊗ so that we can recursively define
[[A1 ⊗ · · · ⊗ Am ]] = [[A1 ]] ⊗ · · · ⊗ [[Am ]].
We use the left rule for ⊗ is to justify modelling a proof of a judgement
A1 , . . . , Am ` B
as a morphism
[[A1 ]] ⊗ · · · ⊗ [[Am ]]
 [[B]]
in some category C with a suitable ⊗operation.
We use [[A1 , . . . , Am ]] = A1 ⊗ · · · ⊗ Am .
Using semantic brackets becomes somewhat tedious over time, and so we frequently assume
that the formula A is interpreted by an object we also refer to as A.
We want to recursively define an assignment from proofs in the logic to morphisms in the
category. We do this by saying how to treat each of the proof rules in the system. Some
proofs are identified when they are mapped into the category, and how much identification
goes on provides some measure of how good a model we might have.
Not all identifications are bad, however: There are some proofs that are ‘similar enough’
for us to want them to be identified. We use this idea to motivate some of the equations we
expect to hold in any categorical model. For now the central question is what properties the
operation ⊗ on the category C should have.
We start by looking at the rule
Γ`A
∆`B
Γ, ∆ ` A ⊗ B
.
It means that given morphisms
[[Γ]]
 A
and
[[∆]]
 B
we have to be able to define a morphism
[[Γ, ∆]] = [[Γ]] ⊗ [[∆]]
2
 A⊗B
and if ⊗ is a bifunctor on C, that is a functor C × C  C, then this is taken care of for
us automatically: We merely take the tensor product of the given morphism [[Γ]]  A with
that of the given morphism [[∆]]  B.
Functoriality of this assignment means the following: The leaf rule A ` A is interpreted
by the identity on (the interpretation of) A. So preservation of identities by ⊗ means that
the identity on A ⊗ B is used to interpret
A, B ` A ⊗ B,
which itself is a consequence of A ` A and B ` B. Since from there we can, in fact, prove
that A ⊗ B ` A ⊗ B this seems to make sense.1 These are some of the identifications we want
to be able to make.
This leaves us with the question of why ⊗ should also preserve composition. Composition
in the category is the interpretation of the Cut rule:
Γ`A
A, ∆ ` B
Γ, ∆ ` B
.
From arrows
f : [[Γ]]
and
 A
g : A ⊗ [[∆]]
 B
we have to define an arrow
[[Γ]] ⊗ [[∆]]
 B,
and fortunately there’s something to fill the gap:
[[Γ]] ⊗ [[∆]]
f ⊗id[[∆]]
 A ⊗ [[∆]]
g
 B.
Exercise 2 Find a justification for demanding that ⊗ preserve composition.
Because lists of formulae are associative by definition, we expect ⊗ to be associative.
Further, because of the exchange rule we expect it to be symmetric. And finally we need an
‘empty’ version of the tensor product in order to interpret judgements which have an empty
context. We refer to this object as I, and it is clear that it should behave like a unit for ⊗.
Definition 1 A (symmetric) monoidal category is a category C together with a bifunctor ⊗ on C that is associative, (symmetric) and has a unit I. By that we mean 2 that
there exist natural isomorphisms α, (σ,) ρ and λ such that the diagrams given below commute.
These isomorphisms ‘mediate’ between objects and so provide us with associativity, symmetry
and unit laws. Their naturality is expressed in the following set of diagrams.
A ⊗ (B ⊗ C)
αA,B,C
 (A ⊗ B) ⊗ C
f ⊗(g⊗h)
(f ⊗g)⊗h
?
0
0
?
 (A0 ⊗ B 0 ) ⊗ C 0
0
A ⊗ (B ⊗ C )
αA0 ,B 0 ,C 0
1
If we only allow axioms to introduce literals (say p, q) then tensor preserving the identity amounts to the
tensor of the identities on p and q interpreting p ⊗ q ` p ⊗ q, which can be proven from p ` p and q ` q.
2
Strictly speaking, the isomorphisms are part of the structure that form the symmetric monoidal category,
but in practice people are often quite lax about this—it is common to say that a category ‘is symmetric
monoidal’ without exhibiting the corresponding tensor product.
3
A⊗B
σA,B
 B⊗A
f ⊗g
?
I ⊗ A0
σA0 ,B 0
λ A0
 A
f ⊗idI
f
?
?
 B 0 ⊗ A0
ρA
A⊗I
 A
idI ⊗f
g⊗f
A0 ⊗ B 0
λA
I⊗A
f
?
?
 A0
A0 ⊗ I
ρA0
?
 A0
These natural isomorphisms interact with each other as given by the diagrams below.
αA,B,C⊗D
A ⊗ (B ⊗ (C ⊗ D))
 (A ⊗ B) ⊗ (C ⊗ D)
idA ⊗αB,C,D
αA⊗B,C,D
?
?
 ((A ⊗ B) ⊗ C) ⊗ D
αA,B⊗C,D
 (A ⊗ (B ⊗ C)) ⊗ D
A ⊗ ((B ⊗ C) ⊗ D)
A ⊗ (B ⊗ C)
αA,B,C
 (A ⊗ B) ⊗ C
αA,B,C ⊗idD
σA⊗B,C
 C ⊗ (A ⊗ B)
idA ⊗σB,C
αC,A,B
?
A ⊗ (C ⊗ B)
A ⊗ (I ⊗ C)
αA,C,B
 (A ⊗ C) ⊗ B
?
 (C ⊗ A) ⊗ B
σA,C ⊗idB
αA,I,C
id
σB,A
B
⊗
λ
 B⊗A
id A
ρA ⊗idA
A⊗
σA,B
A⊗B
 (A ⊗ I) ⊗ C
C
 ?

A⊗C
A⊗B
?
Remark. There are further equations one might be tempted to impose on (symmetric)
monoidal categories. Two of those are the following which commute in every (symmetric)
monoidal category.
I⊗I
=
λI
σI,A
 A⊗I
ρA
λA
ρI
I⊗A

? ?
?
A
I
The proof is not totally obvious. The coherence theorem tells us that all ‘sensible’ diagrams
we may build from the natural isomorphisms do, in fact commute.
Exercise 3 Show that the category of sets and relations Rel is symmetric monoidal. Hint:
The tensor product we are looking for (because it will return in subsequent exercises) is given
by cartesian product. You might want to convince yourself that this is not the product in
this category.
4
Exercise 4 Convince yourself that a category with finite products is symmetric monoidal.
Do the same for categories with finite coproducts.
So in order to be able to interpret ⊗ we require our category C to be symmetric monoidal.
The question of what a functor of symmetric monoidal categories should be can be answered
in several ways. Maybe the most straightforward would be to demand that the symmetric
monoidal structure is preserved (at least up to isomorphism), but that turns out to be too
strong for many examples. Instead, we choose the following notion, which is a lax one (in the
technical sense). Note that we do not distinguish between the tensor products in different
categories in our notation, similarly for the unit I. Also note that we are sloppy in our
notation and write − ⊗ − for the functor C × C  C although nothing in the notation
suggests that we assume it to have two (possibly different) arguments rather than just one.
Definition 2 Let C and D be symmetric monoidal categories.
(a) A functor F : C  D is said to be symmetric monoidal if there exist a morphism
 F (− ⊗ −) respecting
mI : I  F (I) and a natural transformation m : F (−) ⊗ F (−)
the symmetric, associative, and unit structures.
 D with natural transformations
(b) Let F and G be two symmetric monoidal functors C
 G is monoidal if the
m and n respectively. We say that a natural transformation τ : F
following diagrams commute.
I
mI
 F (I)
nI
τI
F (A) ⊗ F (B)
 F (A ⊗ B)
τA ⊗τB

?
G(I)
mA,B
τA⊗B
?
G(A) ⊗ G(B)
?
 G(A ⊗ B)
nA,B
A priori there is no good reason to demand the natural transformation to go in the given
direction, it might as well go the other way—however, some justification for choosing this
direction is provided by Exercise 9.
Exercise 5 (a) If you are unsure about what it meant by ’respecting the ... structures’ try
drawing some diagrams.
(b) Show that if F is a symmetric monoidal endofunctor on a symmetric monoidal category
C then so is F ◦ F . Further show that the identity functor on a symmetric monoidal category
is symmetric monoidal.
(c) Show that the following endofunctors are monoidal for every symmetric monoidal category
C:
• The ‘constant I functor’ CI which maps every object to I and every morphism to the
identity on I.
• The ‘diagonal functor for tensor’ ∆ which maps an object A of C to A ⊗ A and a
morphism f : A  B to f ⊗ f : A ⊗ A  B ⊗ B.
This brings us to the next connective, linear implication (. This connective is very tightly
linked to the morphisms of our category C for the following reason. Any judgement A ` B is
5
interpreted by a morphism A  B. This judgement allows us to deduce ` A ( B, which
is interpreted by a morphism I  A ( B. Hence there is a connection between morphism
A  B and those I  A ( B which is tightened by the following derivation. Assume
now that we have a derivation of ` A ( B.
·
·
·
`A(B
A`A B`B
A, A ( B ` B
Cut
A`B
For our category that means that we must be able to go the other way, too. We expect
the following onetoone correspondence:
A B
===========
I  A(B
or, more generally,
C ⊗A  B
============
 A(B
C
Assuming we make the usual naturality assumptions this means that the functor − ⊗ A is
leftadjoint to A ( −. The better known notion of a cartesian closed category is a special
case of this: the monoidal structure, that is the tensor product, is given by a product.
Definition 3 A symmetric monoidal closed category is a symmetric monoidal category
in which each functor − ⊗ A has a right adjoint.
We use ( to refer to these right adjoints. Note that the adjunction does impose more
structure on the linear function space construct than one might think at first.
Exercise 6 (a) Show that in every symmetric monoidal closed category I(A ∼
= A naturally.
(b) Show that in every symmetric monoidal closed category (A ⊗ B) ( C is naturally isomorphic to A ( (B ( C).
(c) Show that in every symmetric monoidal closed category C, C(A ⊗ B, C) is isomorphic to
C(A, B(C) and that this isomorphisms is natural in all three of A, B and C. (This is because
we have an example of a parametrized adjunction, see for example [Mac71], Theorem VI.7.3.)
Symmetric monoidal closed categories have all the categorical structure required to model
the multiplicative fragment of intuitionistic linear logic.
Definition 4 A model for MILL is any symmetric monoidal closed category.
Exercise 7 Show that Rel is a symmetric monoidal closed category. Hint: the underlying
set for A ( B is again the cartesian product of A and B.
Exercise 8 For every rule in Table 1 find the
morphisms interpreting the hypothesis, find the
the same vice versa, that is for every equation
category, find a proof justifying it. (For this it
described using equations only.)
6
categorical counterpart, that is given the
morphism interpreting the conclusion. Do
imposed on a symmetric monoidal closed
is useful to recall how adjunctions can be
One might assume that something additional is required for a functor between symmetric
monoidal closed (rather than merely symmetric monoidal) categories, but this is not the case.
Definition 5 A morphism of symmetric monoidal closed categories is a symmetric
monoidal functor.
This definition is justified by the following result.
Exercise 9 Assume that C and D are symmetric monoidal closed categories. Show that
if F : C  D is a symmetric monoidal functor then there exist natural transformations
F (A ( −)  F (A) ( F (−) and F (− ( B)  F (−) ( F (B), and so a natural transformation F (− ( −)  F (−) ( F (−) which is natural in both arguments.
MALL—the multiplicative additive fragment
We add one of the additive connectives to the multiplicative fragment MILL, namely the
conjunction u. For that we add the following rules to those given in Table 1, and call the
result MALL.
Additive connectives
left
Γ, A ` C
Γ, B ` C
Γ, A u B ` C
Γ, A u B ` C
Constants
right
Γ`A
Γ`B
Γ`AuB
Γ`1
Table 2: The rules for u
The categorical interpretation for the new connective u certainly should be something
similar to a tensor product. But looking at the left introduction rules we find that we need
something stronger here. In particular given C ` A and C ` B we obtain C ` A u B,
 A and C
 B we have to be able to construct a morphism
so given morphisms C
C
A u B. This looks just like the requirement we demand for products, at least the
part about being able to construct such morphisms. So how about the second requirement,
the projections? From A ` C we have to be able to conclude that A u B ` C. So given
 C. If we do have
a morphism A  C we have to be able to construct one A u B
 A then we can simply precompose that with the given morphism
a projection A u B
to obtain the desired result. Similar for the symmetric version. Since the usual categorical
symbol for a product is × we often write that rather than u for the interpretation of that
connective in the category. The interpretation of 1 is similarly determined. Clearly there will
have to be a morphism A  1 for every object A. We demand that there be precisely one
of those for each A, making 1 the terminal object or ‘empty product’.
Definition 6 A model for MALL is given by a symmetric monoidal closed category with
finite products.
Exercise 10 Show that Rel is a model for MALL. Hint: the categorical product is given by
the disjoint union; projections are the ‘reversed’ injections.
Exercise 11 Justify the equations defining a categorical product from the rules for MALL.
7
Exercise 12 Show that if C and D are categories with products then for every functor
F : C  D, F op : C op  Dop is monoidal.
Since we are happy with this much connection between the structure of the source and
the target category there is no need to define new morphisms of models of MALL.
ILL—the intuitionistic fragment
In order to obtain the intuitionistic fragment of linear logic we have to add one other connective, the unary !. This is our way of marking formulae which we allow to be subject to the
weakening and contraction rules. This fragment is obtained by adding the rules in Table 3 to
MALL.
The linear exponential !
Γ`B
Γ, A ` B
Γ, !A ` B
Γ, !A ` B
Γ, !A, !A ` B
!Γ ` A
Γ, !A ` B
!Γ ` !A
Table 3: The rules for the linear exponential !
We wish to interpret ! in the categorical model C by a functor C  C which we also
refer to as !. This functor will have to come with additional structure so that we can define
morphisms corresponding to various rules. We postpone the argument for why ! should be
defined on morphisms too.
The judgement A ` B is interpreted by a morphism A  B, and from that we have to
be able to obtain a morphism !A  B. This can be done most easily if we demand that
there exist a morphism A : !A  A for each object A, then the composite
!A
A
 A
 B
can be used to interpret the resulting proof of !A ` B.
Further from !A ` B we get !A ` !B and thus for a morphism !A  B we want to be
able to define a morphism !A  !B, that is we want a map (−)∗ : C(!A, B)  C(!A, !B).
If we want to enforce that certain proofs create the same morphisms in our model then we
have to impose some conditions on these.
Consider the proof
A`A
!A ` A
!A ` !A
We might just as well have started with the axiom !A ` !A and therefore we demand that
(A )∗ = id!A . Next consider the proof
·
·
·
!A ` B B ` B
!A ` !B
!B ` B
!A ` B
8
Cut
This amounts to cutting against the identity (well, almost), and should really be the same
as the original proof of !A ` B. Hence we demand that the assignment B ◦ (−)∗ be the
identity on C(!A, B).
Finally consider the two proofs
·
·
·
!A ` B
!B ` C
!A ` !B
!B ` !C
!A ` !C
·
·
·
!A ` B
!A ` !B !B ` C
!A ` C
Cut
Cut
!A ` !C
Arguably we have performed ‘the same’ cut both times, and these proofs should be considered equal. Therefore we demand that for f : !A  B and g : !B  C we have that
g ∗ ◦ f ∗ = (g ◦ f ∗ )∗ .
Hence we have that !, and (−)∗ form the dual of a Kleisli triple. An alternative way
of defining the same structure is the following.
Definition 7 A comonad on a category C consists of a functor ! and natural transformations : !  idC and δ : !  !! such that the following diagrams commute for all objects A.
!A
δA
 !!A
id !
!A
A
δA
!A
δA
 !!A
δA

?
!!A
!A
?
 !A
δ!A
?
!!A
!δA
?
 !!!A
We often call the counit of the comonad and δ its comultiplication.
Exercise 13 Show that the dual of a Kleisli triple (that is, assignments (!, , (−)∗ ) as above
satisfying the given equations) defines a comonad and vice versa.
A definition of our linear exponential comonad (see Definition 10) in terms of (the duals
of) Kleisli triples appears as ‘exponential structure’ in [Mel].
Exercise 14 Show that the following is a comonad on the category of sets and relations.
On objects let !A be the set of multisets over A. For a morphism R : A + B set x !R y
if and only if there exists c ⊆ R such that π1 [c] = x and π2 [c] = y (we are viewing the
pij [c] as multisets here). For the counit, take the reverse of the ‘singleton’ relation. For the
comultiplication take the ‘sum’ of the multisets in question.
This allows us to interpret the rules on the right hand side of Table 3. Before we turn to
the rules on the left hand side of the same table we resolve another matter.
Consider the following proofs.
A`A
B`B
!A ` A
!B ` B
`I
!A, !B ` A ⊗ B
` !I
!A, !B ` !(A ⊗ B)
!A⊗!B ` !(A ⊗ B)
9
So there must be morphisms mA,B : !A⊗!B  !(A ⊗ B) which we expect to be natural
in A and B, and there must be a morphism mI : I  !I. In other words we expect that ! is
a monoidal functor. We further demand that and δ are monoidal natural transformations.
Definition 8 We say that a comonad (!, , δ, m, mI ) is monoidal if ! is a monoidal functor
(witnessed by m and mI ) and and δ are monoidal transformations.
Exercise 15 Show that the multiset comonad from Exercise 14 is monoidal.
Exercise 16 Can you find prooftheoretic reasons for demanding that and δ be monoidal?
How about the naturality of m?
We finally turn to the left rules for !. Given a morphism I  B which is the interpretation of (some proof of) ` B, we have to be able to define a morphism !A  B which
serves as the interpretation of !A ` B. Again we use a composite, namely
!A
eA
 I
 B,
demand that for every object A there be a morphism eA : !A  I.
Similarly we demand the existence of a morphism dA : !A  !A⊗!A to interpret the
contraction rule. As is to be expected, the mere existence of these morphisms is not sufficient
for our purposes.
First of all we expect symmetry, transitivity and unit laws to hold. Clearly when contracting three occurrences of, say, !A, it should not matter in which order this happens.
Exchanging two such occurrences and then contracting them should be the same as just contracting them. And first introducing !A by weakening and then contracting it with an existing
copy should be the same as doing nothing at all. Mathematically, what we are talking about
is a commutative comonoid, and this is something that can be formulated quite generally in
any symmetric monoidal category.
Definition 9 A commutative comonoid in a symmetric monoidal category C is an object
A with two morphisms e : A  I and d : A  A ⊗ A such that the following diagrams
commute.
d
d
 A⊗A
 A⊗A
A
A


?
A⊗A
A
d
e⊗idA
λA
d
σA,A
 A⊗A
d
d⊗idA
 (A ⊗ A) ⊗ A
αA,A,A
?
A⊗A
?
I⊗A
idA ⊗d
10
?
 A ⊗ (A ⊗ A)
A morphism of comonoids from (A, e, d) to (A0 , e0 , d0 ) is a morphism f : A
specting the comonoid structure, that is the following diagrams commute.
A
A
d
 A⊗A
f ⊗f
f
f
 A0 re
e
e0
?

?
A0
A0
 I
d
?
 A0 ⊗ A 0
0
Exercise 17 (a) Show that the multiset over a set A is a commutative comonoid in the
category Rel.
(b) Show that if C is a category with finite products then every object carries a comonoid
structure, and every morphism preserves it.
We want every triple (!A, eA , dA ) to be a commutative comonoid. Clearly objects of
the form !A play a particular role—they are the interpretations of formulae on which we
may perform the structural rules such as weakening and contraction. In the first published
definition of a model for linear logic [Laf88] it was demanded that (!A, eA , dA ) be the free
commutative comonoid over A. However, that turns out to be a definition which leaves out
many perfectly good models of linear logic, for example that of coherence spaces with the
powerset comonad. Instead the following definition of Bierman’s [Bie95] (building on work by
Seely [See89]) has been generally accepted. The following essentially the original definition
of a ‘linear category’ as given by Bierman [Bie95]. It can be shown that a Lafonttype model
is a special case of one of these.
Definition 10 A symmetric monoidal category has a linear exponential comonad if it
has a monoidal comonad (!, , δ, m, mI ) such that
• all objects of C which are of the form !A are equipped with a commutative comonoid
structure (A, eA , dA );
• the comonoid structure gives rise to monoidal natural transformations e : !
d : !  ∆◦! for the endofunctors !, CI and ∆◦! on C;
 CI and
• the natural transformations e and d satisfy the following diagrams;
δA
!A
 !!A
!dA
dA
?
!A⊗!A
δA ⊗δA
 !!A⊗!!A
?
 !(!A⊗!A)
m!A,!A
!A
δA
 !!A
!eA
eA
?
I
mI
?
 !I
• every morphism of the form δA is a morphism of comonoids.
This is not the only way of defining the concept, and one of the equivalent formulations,
see Proposition 4, is a lot shorter, and maybe the easiest to understand.
We introduce various categories that are connected with comonads which allows us to
reformulate the desired structure. The first of these concentrates on ‘objects of the form !A’.
We have to be careful about how we talk about them because we cannot afford to forget
11
the underlying object A. Hence given a category C with a comonad (!, , δ) we define a new
category whose objects are labelled by the objects of C, but which we secretly think of as
objects of the form !A. This becomes noticeable in the notion of morphism for such objects.
Definition 11 The category C! of free coalgebras for a comonad (!, , δ) on a cat B are morphisms
egory C has objects A, where A is an object of C. Morphisms A
f : !A  !B in C such that the following diagram commutes.
!A
f
 !B
δB
δA
?
!!A
!f
?
 !!B
Exercise 18 Show that every morphism in C! can be written as a composite of morphisms
of the form δA and !f .
There is a generalized form of ‘coalgebra’ for a comonad. We have to refer to this because in
general there is no monoidal structure on the category of free coalgebras in our situation. (One
might want to use tensor and its unit from C, and indeed there are appropriate symmetry,
associativity and unit isomorphisms on C! ; symmetry between A ⊗ B and B ⊗ A, for example,
is given by !σA,B . However, it is impossible to make ⊗ into a bifunctor—there is just nothing
sensible one can do on morphisms. Fortunately the category of free coalgebras embeds into a
larger category where we can define a suitable monoidal structure.
Definition 12 The category C! of EilenbergMoore coalgebras for a comonad (!, , δ)
 !A such that the following diagrams
on a category C has objects Cmorphisms ξ : A
commute.
ξ
ξ
 !A
 !A
A
A
id A
A
δA
ξ

?
?
!A
A
!ξ
?
 !!A
We also refer to these objects as coalgebras (for the comonad). Morphisms between
 !B are given by morphisms f : A
 B such
two such objects ξ : A  !A and ζ : B
that the following diagram commutes.
A
f
 B
ζ
ξ
?
!A
!f
?
 !B
Exercise 19 (a) Show that C! embeds into C! by mapping an object A to the object given
by δA : !A  !!A, and a morphism f : A  B in C! to the underlying f : !A  !B
(from C), viewed now as a morphism in C! . Note that this embedding is full.
12
(b) Show that if ξ : A  !A is a coalgebra then ξ is a morphism in C! from ξ : A
to δA : !A  !!A (which you have just shown to be another coalgebra).
 !A
(c) Show that the category of free coalgebras C! is isomorphic to the Kleisli category of a
comonad. This category has objects A where A is an object in C and morphisms A  B
are given by morphisms !A  B in C. The identity on an object A is A and the composite
of f : A  B and g : B  C is given by g◦!f ◦ δA : A  C. If you haven’t seen this
construction before you might want to prove that it does indeed give a category.
We define the monoidal structure on C! which we are interested in.
Proposition 1 Let (!, , δ, m, mI ) be a monoidal comonad on a symmetric monoidal category C. Then C! is symmetric monoidal. The tensor product of two objects
ξ: A
 !A
and
ζ: B
 !B
is given by
A⊗B
ξ⊗ζ
 !A⊗!B
mA,B
The unit for the tensor product is given by mI : I
 !(A ⊗ B).
 !I.
Exercise 20 (a) Prove Proposition 1.
(b) Show that mI and mA,B are morphisms in C! between the appropriate coalgebras.
Whenever we refer to a tensor product on C! then this is the one we mean. We shall,
however, make this explicit in the results we state. Note that now the tensor product of two
objects of the category of free coalgebras A and B, which we think of as δ A : !A  !!A and
δB : !B  !!B in the larger category, now has !A⊗!B as its ‘underlying object’ as desired.
!
Let C⊗
! be the closure of C! under finite tensor products in C .
Exercise 21 (a) Show that there is an adjunction between C and C! . Hint: The functor
C  C! maps an object A to δA : !A  !!A; the functor C!  C is the identity on
objects. Show that this adjunction is monoidal, that is both functors are monoidal and so
are the natural transformations connecting them.
(b) Do the same for C and C! . Hint: C  C! maps an object A to A, and a morphism
f : A  B of C to the morphism of C! given by !f : !A  !B. The functor C!  C
maps an object A to !A and maps a morphism f : A  B in C! to the underlying morphism
f : !A  !B from C.
(c) Show that the first adjunction factors through the second one by making use of the
embedding from Exercise 19(a). Use this to establish an adjunction between C and C ⊗
! and
show that this adjunction is monoidal.
A linear exponential comonad is, in fact, equivalent to a stronger sounding structure. We
began by concentrating on the category of coalgebras.
Proposition 2 A symmetric monoidal category C has a linear exponential comonad if and
only if it has a monoidal comonad such that the category of EilenbergMoore coalgebras,
with the induced tensor product (see Proposition 1), is naturally a category of commutative
comonoids. By this we mean that
• every object of the Eilenberg Moore category has a comonoid structure such that
13
• the comonoid structure yields natural transformations idC!
and these are monoidal.
 CI and id !
C
 ∆
Before proving this result it is worth to expand the conditions which appear in it. Exercise 5(b) and (c) establishes that it makes sense to talk about monoidality in this context.
We use e and d to refer to the natural transformations given by counit and comultiplication
respectively. Note that from here on we typically refrain from bracketing tensored expressions and leave out any mentioning of the associativity isomorphism. This results in better
readability, and interested readers can reestablish the results with that isomorphism made
explicitly if they are so inclined.
First of all, the components of e and d must be morphisms of C! . That means that for
a coalgebra ξ : A  !A we have the following, where we abbreviate coalgebras by merely
naming the underlying morphism.
dξ
A
eξ
A
 A⊗A
 I
ξ⊗ξ
?
ξ
mI
?
!A
!eξ
!A⊗!A
ξ
?
 !I
mA,A
?
 !(A ⊗ A)
?
!A
!dξ
Secondly, they must be natural. Assume that we have a second coalgebra, namely
ζ : B  !B and a morphism f from ξ to ζ.
A
eξ
f
eζ
 A⊗A
f ⊗f
f
?

?
B
dξ
A
 I
?
 B⊗B
B
dζ
Remark. Naturality of the comonoid structure is equivalent to saying that every morphism
of coalgebras is a morphism of comonoids.
Lastly there are the monoidality conditions.
I
idI
A⊗B
 I
idA⊗B
 A⊗B
eξ ⊗eζ
id I
e mI

?
?
I⊗I
I
14
λI =ρI
eξ⊗ζ
?
 I
idI
I
idA⊗B
A⊗B
 I
 A⊗B
−
λI
dξ ⊗dζ
1
d mI
=
dξ⊗ζ
1
−
ρI

?
?
 A⊗B⊗A⊗B
?
A⊗A⊗B⊗B
I⊗I
idA ⊗σA,B ⊗idB
Remark. The monoidality of the natural transformations given by the comonoid structure
implies that the comonoid structure is wellbehaved with respect to the monoidal structure
on C! .
By this we mean that
 !I, the structure is given by
• for the tensor unit mI : I
idI : I  I
−1
λ−1
I = ρI : I
counit
comultiplication
 I ⊗ I;
• the comonoid structure on the tensor product of ξ : A  !A (with comonoid structure
(e, d)) and ξ 0 : A0  !A0 (with comonoid structure (e0 , d0 )) is given by
counit
comultiplication
A ⊗ A0
e⊗e0
A ⊗ A0
d⊗d0
 I⊗I
λI =ρI
 I
 A ⊗ A ⊗ A 0 ⊗ A0
idA ⊗σA,A0 ⊗idA0
 A ⊗ A0 ⊗ A ⊗ A 0 .
Proof. We begin with the ‘if’ part, so let’s assume we have a structure on C! as given
in the statement of the proposition. For !A, pick the comonoid structure for the coalgebra
δA : !A  !!A given by the assumption, that is, set dA = dδA , where reusing the letter d
hopefully is not too confusing.
Naturality is easy to establish. It follows from the fact that morphisms of the form !f are
morphisms of coalgebras and so by the above remark morphisms of comonoids.
We establish monoidality for the natural transformations e and d. Note that m I is a
morphism in C! from mI : I  !I to δI : !I  !!I by Exercise 20(b) and so a morphism of
comonoids by assumption. For similar reasons mA,B is a morphism of coalgebras from
m!A,!B ◦(δA ⊗δB )
 !(!A⊗!B)
!A⊗!B
counit:
λI ◦ (eA ⊗ eB )
comultiplication: (id!A ⊗ σ!A,!B ⊗ id!B ) ◦ (dA ⊗ dB )
to
!(A ⊗ B)
eA⊗B
dA⊗B
δA⊗B
 !!(A ⊗ B)
and so a morphism of comonoids.
Since emI = idI by monoidality of e we get the left hand diagram below from the fact that
mI preserves the counit, and the right hand diagram from the fact that mA,B preserves the
counit as well.
I
mI
!A⊗!B
 !I
id I
eI
mA,B
 !(A ⊗ B)
eA ⊗eB
eA⊗B

?
?
I
I⊗I
15
λI =ρI
?
 I
Monoidality of the natural transformation d is very similar. We know that m I must also
−1
preserve the comultiplication, and for the algebra mI : I  !I that is given by λ−1
I = ρI ,
which gives the left diagram. For the right diagram we once again use that m A,B is a morphism
of comonoids as indicated above and so must preserve the comultiplication.
mI
I
 !I
−1
λ−1
I =ρI
 !(A ⊗ B)
dA ⊗dB
dI
dA⊗B
?
?
 !I⊗!I
?
I⊗I
mA,B
!A⊗!B
?
 !A⊗!B⊗!A⊗!B
!A⊗!A⊗!B⊗!B
mI ⊗mI
id!A ⊗σ!A,!B⊗id!B
The two diagrams given explicitly in the definition of linear exponential comonad say
that every component of the natural transformations is a morphism of the (appropriate)
coalgebras, which is part of the assumptions. Lastly, every morphism of the form δ A is a
morphism of coalgebras as follows
δA
!A
 !!A
δ!A
δA
?
!!A
!δA
?
 !!!A
and so covered by the remark that naturality of the comonoid operations is equivalent to
every morphism of coalgebras being a morphism of comonoids.
Now for the ‘only if’ part. Assume that we have a linear exponential comonad. For a
coalgebra ξ : A  !A we use the fact that this makes A (in C) a special kind of retract
of !A. We define the following morphisms which we show give it a comonoid structure:
A
ξ
dA
 !A
 !A⊗!A
and
A
ξ
 !A
A ⊗A
 A⊗A
eA
 I.
We note in passing that for the coalgebra δA : !A  !!A the new comonoid structure
coincides with the old since δA is a morphism of comonoids.
!A
dA
!A
 !A⊗!A
id
id
δA ⊗δA
δA
!!A
δA
!A
?
 !!A⊗!!A
d!A
 !A⊗!A
?
!!A
!A ⊗!A

?
eA
!A
⊗
e!A
We begin by establishing symmetry.
A
ξ
 !A
dA
 !A⊗!A
 A⊗A
σA,A
dA
σ!A,!A

?
!A⊗!A
16
A ⊗A
?
 A⊗A
A ⊗A
 I
Next we find it useful to establish that
(ξ ⊗ ξ) ◦ (A ⊗ A ) ◦ dA ◦ ξ = dA ◦ ξ.
ξ
A
 !A⊗!A
d!A
dA
δA
⊗
δA
δA
ξ⊗ξ
?
 !A⊗!A
!A ⊗!A 

?
 !!A⊗!!A
?
 !!A
?
 A⊗A
!ξ⊗!ξ
!ξ
!A
A ⊗A
dA
 !A
ξ
(∗)
A
⊗!
id !A

!A⊗!A
We use in the above diagram that ξ is a coalgebra, naturality of d and as well as the fact
that δ is a morphism of comonoids and one of the comonad equations.
We show that the unit law holds.
ξ
A
 !A
dA
 !A⊗!A
A ⊗A
 A⊗A
ξ
ξ⊗ξ
?
 !A⊗!A
dA
id A
ξ⊗

!A
A
⊗
A
id !
id A
λA
eA ⊗id!A


?
I⊗!A
!A ⊗ A
A
⊗
id A
A
eA ⊗idA


?
A
λA
?
 I⊗A
In the above diagram we use the just established equation (∗) at the top, that A ◦ ξ = idA ,
and various naturality conditions.
Finally we turn to associativity, where we leave out bracketing and the associativity isomorphism for readability.
17
A
ξ
A ⊗A
dA
 !A
 !A⊗!A
 A⊗A
id
A⊗
ξ
ξ

?
!A
?
 !A⊗!A
 A⊗A
A ⊗A
A⊗!A⊗!A
id!A ⊗dA
dA
?

?
 !A⊗!A
dA
!A
dA
!A⊗!A
A
ξ⊗ξ
ξ⊗ξ
idA ⊗dA
?
 !A⊗!A⊗!A
?
A⊗!A⊗!A
dA ⊗id!A
id A
ξ⊗
A
⊗
A
A

!A ⊗ A
 !A⊗!A ⊗ A
dA ⊗idA
idA ⊗A ⊗A
⊗
 ?
 A⊗A⊗A
A ⊗A ⊗idA
Again we have used the equation (∗) and the same coalgebra equation.
Hence we have indeed defined a comonoid structure. It remains to establish the conditions
stated in the bullet points. First we establish that the comultiplication and counit we have
just defined are morphisms in C! . Again we use the equation (∗), the equation for d stated as
a diagram in the definition of linear exponential comonad, and various coalgebra, comonad
and naturality equations.
A
ξ
dA
 !A
 !A⊗!A
A ⊗A
 A⊗A
ξ

 !A⊗!A
!A
dA
id
!A
δA ⊗δA
ξ
⊗
!A
 ?
 !A⊗!A
?
!!A⊗!!A
δA
ξ⊗ξ
!A ⊗!A
mA,A
m!A,!A
?
!A
?
 !!A
!ξ
?
 !(A ⊗ A)
!dA
?
 !(A ⊗ A)
!(A ⊗A )
For the second diagram we merely require a coalgebra equation and the equation for e
stated in the assumptions.
A
ξ
 !A
eA
δA
ξ
?
!A
!ξ
?
 !!A
18
 I
mI
!eA
?
 !I
Let f be a morphism from ξ : !A  A to ζ : !B  B in C! . To establish naturality
of the new comonoid operations we provide the following diagrams, where we use naturality
of e and d.
A
ξ
 !A
dA
 !A⊗!A
!f ⊗!f
ζ
?
 !B⊗!B
dB
A
f
ξ
!f
f
?
 B⊗B
?
B
B ⊗B
 !A
ζ
?
 !B

?
 !B
?
B
 A⊗A
eA
!f
f
A ⊗A
eB
 I
It remains to establish that these natural transformations are monoidal, compare the
diagrams on page 14. For the counit this is a straightforward consequence of the monoidality
of e—it is harder to convince oneself that the diagrams below do indeed establish what’s
desired! For that recall that in C! , the tensor product of ξ : A  !A and ζ : B  !B is
given by
A⊗B
I
mI
ξ⊗ζ
 !A⊗!B
 !I
mA,B
 !(A ⊗ B).
A⊗B
ξ⊗ζ
 !A⊗!B
mA,B
 !(A ⊗ B)
eA ⊗eB
id I
eI

?
eA⊗B
?
I ⊗I
I
λI =ρI
?
 I
For the comultiplication, which involves the counit of the comonad , we also require the
monoidality of that natural transformation.
mI
I
 !I
−1
λ−1
I =ρI
?
I⊗I
dI
?
 !I⊗!I
mI ⊗mI
id
I ⊗I
I⊗
I

?
I⊗I
19
A⊗B
ξ⊗ζ
?
mA,B
!A⊗!B
 !(A ⊗ B)
dA ⊗dB
dA⊗B
?
!A⊗!A⊗!B⊗!B
?
 !(A ⊗ B)⊗!(A ⊗ B)
id!A ⊗σ!A,!B ⊗id!B
mA,B ⊗mA,B
A ⊗
A ⊗
 !A⊗!B⊗!A⊗!B
A ⊗
B ⊗
B

A⊗A⊗B⊗B
B ⊗
A⊗B ⊗A⊗B
A ⊗
B
idA ⊗σA,B⊗idB
 ?
 A⊗B⊗A⊗B
That completes the proof.
2
The following proposition talks in terms of the Kleisli category as far as possible—we
have to go to C⊗
! to get a symmetric monoidal category which we need in order to talk about
comonoids of the desired type (but see Proposition 5). It is easiest here if we view C ⊗
! as
!
a subcategory of C . Recall from Exercise 21(a) that there is a functor (which by abuse of
notation we are going to call ! again
!: C
 C!
 !!A
which corestricts to C⊗
! and which maps an object A of C to the free coalgebra δ A : !A
⊗
and a morphism f to !f . There is also a monoidal functor from C to C! which maps everything to the unit for tensor in the target. It is merely a slight generation of the constant I
endofunctor from Exercise 5(c). Again we will abuse notation and refer to that functor as C I .
Proposition 3 A symmetric monoidal category C has a linear exponential comonad if and
only if it has a monoidal comonad (!, , δ, m, mI ) such that the closure under tensor of C! in
C! (under the tensor product from Proposition 1), C⊗
! has the following structure:
• Every object of the category has a comonoid structure such that
• the comonoid structure yields natural transformations !
!, CI : C  C⊗
! , these are monoidal.
 CI and !
 ∆◦!, where
Proof. All the hard work was done in the proof of Proposition 2. For the ‘if’ part we use
the given structure on C⊗
! to define the desired structure on C in precisely the same way as
we do in the proof of that proposition.
For the ‘only if’ part, we invoke Proposition 2, and assume that the linear exponential
comonad is given as stated there. Then all we have to do here is to restrict that structure to
C⊗
2
! . It is easy to see that the resulting structure has the desired properties.
As far as I know the various equivalent ways of describing a linear exponential comonad
given above have not appeared in print. They have certainly been used because the original
definition is rather lengthy, but without a full justification being given
20
The following result is probably the most surprising restatement of what it means for a
category to have a linear exponential comonad, and it certainly is the briefest, and the least
cluttered. It appears in Paola Maneggia’s thesis [Man04].
Proposition 4 A symmetric monoidal category C has a linear exponential comonad if and
only if the tensor product on C! from Proposition 1 is in fact a product.
Proof. The ‘if’ part is easy to establish. We take the comonoid structure from Exercise 17:
The counit is given by the unique morphism to the unit for product, that is the terminal
object. The comultiplication arises from the diagonal arrow hid, idi. We establish that we
have a structure as in Proposition 2.
Obviously the unique morphisms to the terminal objects are natural as desired, and similarly for the diagonal arrows. It only remains to cover monoidality.
Since morphisms into the terminal object are unique there is nothing to be done for the
counit (compare the diagrams on page 14. For the comultiplication note that in a category
−1
where tensor is given by product, λ−1
I = ρI = hidI I, and obviously
idA×B
A×B
 A×B
hidA ,idA i×hidB ,idB i
hidA×B ,idA×B i hidA ×idB i×hidA ×idB i
?
A×A×B×B
?
 A×B×A×B
idA ×hπ2 ,π1 i×idB
Now for the ‘only if’ part. Since Proposition 2 already talks about structure on the
category of coalgebras, that’s the definition of linear exponential comonad we choose to work
with for this proof. Assume we have the two natural transformations e and d as stated there.
Assume that ξ : A  !A and ζ : B  !B are two coalgebras. We have to exhibit
projections, for which we propose the arrows
A⊗B
A⊗B
idξ ⊗eζ
ρA
 A⊗I
eξ ⊗idζ
 I⊗B
 A
λB
 B.
and
(1)
(2)
Being composites of morphisms of coalgebras (for ρA and λB this was established in Exercise 1), these are morphisms of coalgebras.
 !C,
We also have to give a pairing operation. Assume we have a third coalgebra, χ : C
and morphisms f from χ to ξ and g from χ to ζ. Consider the following morphism from χ to
ξ ⊗ ζ.
dχ
 C ⊗ C f ⊗g
 A⊗B
C
We begin by establishing that this composes with the proposed projections as appropriate.
Clearly it is sufficient to consider just one case.
21
dχ
 C ⊗C
C
f ⊗g
 A⊗B
idA ⊗eζ
idC ⊗eζ
?
id C
C ⊗I
?
 A⊗I
f ⊗idI
ρC
ρA

?
C
f
?
 A
Here we use that g is a morphism of comonoids and therefore preserves the counit, as
well as the unit law for the comonoid structure and naturality of ρ.
It remains to establish the uniqueness of the proposed paired morphism. So assume there
 A ⊗ B which composes with the proposed projections to give f and
is a morphism h : C
g as appropriate.
C
dχ
 C ⊗C
h⊗
h
h
f ⊗g
?
A⊗B
dξ ⊗dζ
 A⊗A⊗B⊗B
ρ −1
A
⊗λ
idA ⊗σA,B⊗idB

 A⊗B⊗A⊗B
idA ⊗eξ ⊗eζ ⊗idB
−
B 1
 ?
A⊗I⊗I⊗B
?
 A⊗I⊗I⊗B
idA ⊗σA,B ⊗idB
ρA
idA⊗B
idA ⊗eζ ⊗eξ ⊗idB
ρA ⊗λB
⊗λ
B

?
A⊗B
That completes the proof.
2
For completeness’ sake we also introduce a notion of morphism between categories with
a linear exponential structure. But note that sometimes a stricter version is appropriate,
see [Man04].
Definition 13 Let C and D be symmetric monoidal categories with linear exponential comonads. A functor F : C  D is linearly distributive if and only if F is monoidal (with
 F ! of a functor over a
structure mI , m) and is equipped with a distributive law κ : !F
22
comonad, that is
!F A
δF A
!F A
!κA
?
F

?
F !A
!F !A
κA
A
κA
 !!F A
F A
 FA
κ!A
?
F !A
F δA
?
 F !!A
respecting the comonoid structure, in the sense that
I
eF (A)
!F A
dF (A)
m!A,!A ·(κA ⊗κA )
κA
mI
?
?
F (I)
F (eA )
F !A
 !F A⊗!F A
F (dA )
?
 F (!A⊗!A)
Definition 14 We say that a category C is a model for intuitionistic linear logic if
• it is symmetric monoidal closed;
• it has finite products;
• it has a linear exponential comonad.
Exercise 22 Show that Rel is a model for intuitionistic liner logic.
Morphisms of models for intuitionistic linear logic are given by linearly distributive functors.
Before we move on to situations with more structure it makes sense to give an overview
over other attempts at modelling intuitionistic linear logic. Instead of working in terms of a
monoidal comonad one can work with a monoidal adjunction between a symmetric monoidal
closed and a cartesian closed category [Ben95]. For comparisons of various definitions found
in the literature, see [Mel]. It turns out that if one devises term calculi for linear logic (or
looks at the internal languages of these different styles of categorical logic) then there are
subtle differences [MMdPR].
2
Cartesian closed categories
Models for intuitionistic linear logic are not just interesting for their own sake. They give
rise to a cartesian closed category. Cartesian closed categories are the standard model for
the {u, →} fragment of classical logic, and this is the right universe to give semantics for
various programming languages. We already know from Proposition 4 that if C has a linear
exponential comonad then C! has products, and they are given by the tensor product from
Proposition 1. But if the underlying category C also has products (on top of the symmetric
monoidal and linear exponential comonad structure) then the Kleisli category is particularly
wellbehaved.
23
Proposition 5 Let C be a model for intuitionistic linear logic. Then
!A⊗!B ∼
=!(A × B).
In particular the Kleisli category C! for the linear exponential comonad is closed under the
tensor product from C! . Hence the Kleisli category C! has finite products.
Proof. The claim follows from Proposition 4 and Exercise 21(b) by the fact that right adjoints
preserve products.
2
This isomorphism is part of Seely’s [See89] definition of a model for linear logic, only that
he was interested in the classical case which we consider in the last section. The following
result also appears in [See89], if once again in the classical setting (which does not affect the
proof).
Theorem 6 Let C be a model for intuitionistic linear logic. Then its Kleisli category is
cartesian closed.
Proof. By the previous proposition the Kleisli category C! has finite products, and the
product of A and B is A × B. It remains to find a right adjoint for this functor. This is given
by A → B =!A ( B as is shown by the following series of equations.
C! (A × B, C) ∼
= C(!(A × B), C)
∼
= C(!A ⊗ !B, C)
∼
= C(!A, !B ( C)
∼
= C! (A, !B ( C)
∼
= C! (A, B → C)
2
3
Classical linear logic
Classical linear logic can be understood to be obtained by adding negation to the intuitionistic
fragment—at least if one uses the De Morgan rules to define all the missing connectives (while
this does not do the logic justice it is how the model is built). We will not go into details
here regarding the full system—see for example [Gir87, Gir95]. Variables in this system come
in dual pairs, and then dualization (or negation) can be defined for all formulae using De
Morganstyle rules. The system is typically twosided, that is its judgements are of the form
A 1 , . . . , A m ` B 1 , . . . , Bn .
Proofs of such judgements are interpreted by arrows
A1 ⊗ · · · ⊗ A m
 B1 ......................... · · · ......................... Bn ,
..........
where ................. is defined as the De Morgan dual of ⊗.
Formulae can be moved to the other side of ` by dualizing them. In particular, we can
freely move between A ` B and B ⊥ ` A⊥ . Hence in our category we will have to be able
to freely move between morphisms A  B and morphisms B ⊥  A⊥ . This suggests
having a contravariant functor C  C as the interpretation of dualization, and one that
is its own inverse.
24
Definition 15 We say that a category C has an involutary duality if there is a func C and for which (−)⊥⊥ is
tor (−)⊥ : C  Cop which is adjoint to its partner Cop
equivalent to the identity on C.
Exercise 23 Argue that dualization (as the interpretation of negation) should preserve composition and identities.
Clearly we would like the categorical interpretation of dualization to satisfy the De Morgan
.........
equations connecting the various connectives. For t (the De Morgan dual of u), ................ , and ? (the
De Morgan dual of !) we may indeed use the De Morgan equations to define interpretations,
⊥
.........
for example the semantics of A ................. B will be (A⊥ ⊗ B ⊥ ) . But the connection we wish to
achieve between ⊗ and ( has to be built into the definition of what a model for (classical)
linear logic should be.
Definition 16 A symmetric monoidal closed category C is ∗autonomous if has an object
 (A ( ⊥) ( ⊥ (the transposes of the evaluation
⊥ such that the canonical arrows A
maps) are isomorphisms.
Exercise 24 (a) Show that for a ∗autonomous category we have an involutary duality given
by − ( ⊥ : C  Cop . Further show that for that duality, for every object A, the functor
⊥
− ⊗ A : C  C is left adjoint to (A ⊗ (−)⊥ ) : C  C.
(b) Find conditions to add to the above which are required to ensure that adding an involutary
duality to a symmetric monoidal category gives rise to a ∗autonomous one.
If we have a ∗autonomous category with products then in particular we have a symmetric
monoidal closed category with finite products, so we can interpret MALL. But because we now
.........
can interpret negation, we can also interpret ................ using the De Morgan rules, so
⊥
.........
A .................. B := (A⊥ ⊗ B ⊥ ) .
Exercise 25 Show that Rel is ∗autonomous. Hint: the dual of a set is the set itself; for
morphisms the dual is defined by taking the reverse of the relation in question.
In fact, Rel is more than just ∗autonomous, it is what is called compact closed. A ∗autonomous category is compact closed if for all objects A and B, (A ⊗ B) ⊥ ∼
= A⊥ ⊗ B ⊥
⊥
∼
or, equivalently, A ( B = A ⊗ B. Compact closed categories are degenerate models of linear
.........
logic in the sense that the interpretation of ................ is the same as that of ⊗.
Exercise 26 (a) Show that a category with an involutary duality which has finite products
also has finite coproducts.
(b) Define a linear exponential monad (to interpret ?) and convince yourself that a category
with an involutary duality which has a linear exponential comonad also has one of those.
This exercise justifies the following definition.
Definition 17 We say that a category C is a model for (classical) linear logic if and
only if it is
• ∗autonomous;
• has finite products (and thus finite coproducts);
25
• has a linear exponential comonad (and thus a linear exponential monad).
In other words, all that is added to a model of intuitionistic linear logic is the selfdualization, which has to behave well when it comes to connecting the tensor and the linear
function space. The rest of the structure comes for free, using De Morgan dualization.
References
[Ben95]
N. Benton. * a mixed linear and nonlinear logic: Proofs, terms and models.
In Proceedings of Computer Science Logic ’94, number 933 in Lecture Notes in
Computer Science. Springer Verlag, 1995.
[Bie94]
G.M. Bierman. On intuitionistic linear logic. Technical Report 346, University of
Cambridge Computer Laboratory, August 1994.
[Bie95]
G. M. Bierman. What is a categorical model of intuitionistic linear logic? In
Proceedings of the Second International Conference on Typed Lambda Calculus,
volume 902 of Lecture Notes in Computer Science, pages 73–93, 1995.
[BS]
R. Blute and P. Scott.
manuscript.
[Gir87]
J.Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
[Gir95]
J.Y. Girard. Linear logic: its syntax and semantics. In Girard et al. [GLR95].
[GLR95]
J.Y. Girard, Y. Lafont, and L. Regnier, editors. Advances in Linear Logic, volume
222 of London Mathematical Society Lecture Note Series. Cambridge University
Press, 1995.
[Laf88]
Y. Lafont. Logiques, catégories et machines. PhD thesis, Université Paris 7, 1988.
[Mac71]
S. MacLane. Categories for the Working Mathematician. SpringerVerlag, 1971.
[Man04]
P. Maneggia. Models of linear polymorphism. PhD thesis, School of Computer
Science, The University of Birmingham, 2004.
[Mel]
P. A. Melliés. Categorical models of linear logic revisited. Prépublication de
l’équipe PPS (September 2003, number 22). To appear in Theoretical Computer
Science.
Category theory for linear logicians.
Unpublished
[MMdPR] M. E. Maietti, P. Maneggia, V. de Paiva, and E. Ritter. Relating categorical semantics for intuitionistic linear logic. To appear in Applied Categorical Structures.
[See89]
R. Seely. Linear logic, *autonomous categories and cofree coalgebras. AMS Contemporary Mathematics, 92:371–382, 1989.
26