Combining a monad and a comonad.
We give a systematic treatment of distributivity for a monad and a comonad as arises in giving category theoretic accounts of operational and denotational semantics, and in giving an intensional denotational semantics. We do this axiomatically, in terms of a monad and a comonad in a 2-category, giving accounts of the Eilenberg-Moore and Kleisli constructions. We analyse the eight possible relationships, deducing that two pairs are isomorphic, but that the other pairs are all distinct. We develop those 2-categorical definitions necessary to support this analysis.
Introduction
In recent years, there has been an ongoing attempt to incorporate operational
semantics into a category theoretic treatment of denotational semantics. The
denotational semantics is given by starting with a signature  for a language
without variable binding, and considering the category -Alg of -algebras [4].
The programs of the language form the initial -algebra. For operational seman-
tics, one starts with a behaviour functor B and considers the category B-Coalg
of B-coalgebras [5, 7]. By combining these two, one can consider the combination
of denotational and operational semantics [14, 16]. Under size conditions,
the functor  gives rise to a free monad T on it, the functor B gives rise to a
cofree comonad D on it, and the fundamental structure one needs to consider is
a distributive law of T over D, i.e., a natural transformation  : TD ) DT subject
to four axioms; and one builds the category -Bialg from it, a -bialgebra
being an object X of the base category together with a T -structure and a D-structure
on X , subject to one evident coherence axiom. This phenomenon was
the subject of Turi and Plotkin's [16], with leading example given by an idealised
parallel language, with operational semantics given by labelled transition
systems. In fact the work of this paper sprang from discussions between one of
the authors and Plotkin, whom we acknowledge gratefully.
As a separate piece of work, Brookes and Geva [2] have also proposed the
study of a monad and a comonad in combination. For them, the Kleisli category
for the comonad gives an intensional semantics, with maps to be regarded as
algorithms. They add a monad in the spirit of Moggi to model what has been
called a notion of computation [11]. They then propose to study the category
for which an arrow is a map of the form DX ! TY in the base category, where
T is the monad and D is the comonad. In order for this to form a category, one
needs a distributive law of D over T , i.e., a natural transformation
subject to four coherence axioms. Observe that this distributive law allowing
one to make a two-sided version of a Kleisli construction is in the opposite
direction to that required to build a category of bialgebras.
Motivated by these two examples, in particular the former, we seek an account
of the various combinations of a monad and a comonad, with a treatment
of Eilenberg-Moore and Kleisli constructions. That is the topic of this paper.
The answer is not trivial. It is not just a matter of considering the situation
for a distributive law between two monads and taking a dual of one of them, as
there are fundamental dierences. For instance, to give a pair of monads T and
distributive law of T over T 0 is equivalent to giving a monad structure
on T 0 T [1] with appropriate coherence, but nothing like that is the case for a
distributive law of a monad T over a comonad D. To give a distributive law of
equivalent to giving a lifting of the monad T to T 0 -Alg, but not
a lifting of T 0 to T -Alg. However, to give a distributive law of a monad T over
a comonad D is equivalent to lifting T to D-Coalg and also to lifting D to T -
Alg. Dual remarks, with the Kleisli construction replacing the Eilenberg-Moore
construction, apply to distributive laws of comonads over monads. So we need
an analysis specically of distributive laws between a monad and a comonad,
and that does not amount to a mild variant of the situation for two monads.
In principle, when one includes an analysis of maps between distributive laws,
one has eight choices here: given (T ; D;) on a category C and (T 0
one could consider natural transformations
or the other three alternatives given by
dualisation; and one could dualise by reversing the directions of  and  0 . But
not all of these possibilities have equal status. Two of them each arise in two
dierent ways, re
ecting the fact that a category -Bialg of bialgebras for a
monad T and a comonad D may be seen as both the category of algebras for
a monad on D-Coalg and as a category of coalgebras for a comonad on T -Alg.
And two of the eight possibilities do not correspond to applying an Eilenberg-
Moore or Kleisli construction to an Eilenberg-Moore or Kleisli construction at
all. We investigate the possibilities in Sections 6 to 8.
As an application of morphisms of distributive laws, consider Turi and
Plotkin's work [16]. Suppose we have two languages, each specied by a distributive
law for a syntax monad over a behaviour comonad. To give translations of
both syntax and behaviour, i.e., a monad morphism and a comonad morphism,
that respect the operational semantics, is equivalent to giving a morphism of
distributive laws. So this framework provides a consistent and comprehensive
translation of languages both in syntax and semantics. Similar remarks apply
to the other combinations of monads and comonads.
We make our investigations in terms of an arbitrary 2-category K. The reason
is that although the study of operational and denotational semantics in [16]
was done in terms of ordinary categories, i.e., modulo size, in the 2-category
Cat, it was done without a direct analysis of recursion, for which one would
pass to the 2-category of O-categories, i.e., categories for which the homsets
are equipped with !-cpo structure, with maps respecting such structure. More
generally, that work should and probably soon will be incorporated into axiomatic
domain theory, requiring study of the 2-category V -Cat for a symmetric
monoidal closed V subject to some domain-theoretic conditions [3]. Moreover,
our denitions and analysis naturally live at the level of 2-categories, so that
level of generality makes the choices clearest and the proofs simplest. Mathe-
matically, this puts our analysis exactly at the level of generality of the study of
monads by Street in [15], but see also Johnstone's [6] for an analysis of adjoint
lifting that extends to this setting. The 2-categorical treatment claries the
conditions needed for adjoint lifting. The topic of our study, distributivity for
monads and comonads, agrees with that of MacDonald and Stone [9, 10] when
restricted to Cat. Mulry [12] has also done some investigation into liftings to
Kleisli categories.
Much of the abstract work of the rst four technical sections of this paper is
already in print, primarily in Street's paper [15]. But that is an old paper that
was directed towards a mathematical readership; it contains no computational
examples or analysis; and the material relevant to us is interspersed with other
work that is not relevant. We happily acknowledge Street's contribution, but
thought it worthwhile to repeat the relevant part before reaching the substantial
new work of this paper, which appears in Sections 6 to 8.
Formally, we recall the denition of 2-category in Section 2, dene the notion
of a monad in a 2-category, and introduce the 2-categories Mnd(K) and
Mnd  (K). We characterise the Eilenberg-Moore construction and the liftings
to those constructions in Section 3. We also explain a dual, yielding the Kleisli
construction and the liftings to those constructions in Section 4. This is all
essentially in Street's paper [15]. In Section 5, we give another dual, yielding
accounts of the Eilenberg-Moore and Kleisli constructions for comonads, and
the liftings to them. Then lies the heart of the paper, in which we consider
the eight possible combinations of monads and comonads, characterising all of
them. For a given 2-category K, we rst consider the 2-category CmdMnd(K)
in Section 6. We characterise the category of bialgebras using this 2-category.
It also yields a characterisation of functors between categories of bialgebras. In
Section 7, we consider Mnd  Cmd  (K), characterising the Kleisli category of
a monad and a comonad and functors between them. We consider the other
possibilities in Section 8, which consists of four cases, i.e., four 2-categories
of distributive laws. We give explanations of the constructions of 0-cells, 1-
cells and 2-cells of K from 2-categories of distributive laws. We also give some
examples of categories constructed in this way when
2 Monads in 2-categories
In this section, we dene the notion of 2-category and supplementary notions.
We then dene the notion of a monad in a 2-category K and we dene two
2-categories, Mnd(K) and Mnd  (K), of monads in K.
2.1 Denition A 2-category K consists of
a set of 0-cells or objects
for each pair of 0-cells X and Y , a category K(X;Y ) called the homcate-
gory from X to Y
for each triple of 0-cells X , Y and Z, a composition functor
for each 0-cell X , an object id X of K(X;X), or equivalently, a functor
called the identity on X
such that the following diagrams of functors commute
@
@ @
@ @
R
In the denition of a 2-category, the objects of each K(X;Y ) are often called
1-cells and the arrows of each K(X;Y ) are often called 2-cells. We typically
abbreviate the composition functors by juxtaposition and use  to represent
composition within a homcategory.
Obviously, the denition of 2-category is reminiscent of the denition of
category: if one takes the denition of category and replaces homsets by hom-
categories, composition functions by composition functors, and the axioms by
essentially the same axioms but asserting that pairs of functors rather than
functions are equal, then one has exactly the denition of a 2-category.
2.2 Example The leading example of a 2-category is Cat, in which the 0-
cells are small categories and Cat(C; D) is dened to be the functor category
[C; D]. In this paper, we sometimes treat Cat as though Set is a 0-cell of Cat.
Technically, the existence of two strongly inaccessible cardinals together with a
careful variation in the use of the term small allows that.
2.3 Example For any symmetric monoidal closed category V , one has a 2-
category V -Cat, whose objects are small V -categories, and with homcategories
given by V -functors and V -natural transformations. Two specic examples of
this are
the 2-category LocOrd of small locally ordered categories, locally ordered
functors, and natural transformations, where V is the category Poset of
posets and order-preserving functions.
the 2-category of small O-categories, O-functors, and natural transforma-
tions, where O is the cartesian closed category of !-cpo's.
Each 2-category K has an underlying ordinary category K 0
given by the
0-cells and 1-cells of K. A 2-functor between 2-categories K and L is a functor
from K 0
to L 0
that respects the 2-cell structure. A 2-natural transformation
between 2-functors is an ordinary natural transformation that respects the 2-
cell structure. Given a 2-functor U denitions give rise to
the notion of a left 2-adjoint, which is a left adjoint that respects the 2-cells.
More details and equivalent versions of these denitions appear and are analysed
in [8].
Now we have the denition of 2-category, we can dene the notion of a monad
in any 2-category K, generalising the denition of monad on a small category,
which amounts to the case of
2.4 Denition A monad in a 2-category K consists of a 0-cell C, a 1-cell
subject to commutativity
of the following diagrams in the homcategory K(C;C)
@ @
@ @
@
R
For example, if one lets a monad in K as we have just dened
it amounts exactly to a small category with a monad on it. More generally, if
-Cat, then a monad in K amounts exactly to a small V -category together
with a V -monad on it. So, for instance, a monad in O-Cat amounts to a small
O-category together with a monad on it, such that the monad respects the !-cpo
structure of the homs.
For any 2-category K, one can construct a 2-category of monads in K.
2.5 Denition For any 2-category K, the following data forms a 2-category
0-cells are monads in K.
A 1-cell in Mnd(K) from (C; T
C 0 in K, together with a 2-cell subject to commutativity
in K(C;C 0 ) of
@ @
@ @
@
R
and

JT
A 2-cell in Mnd(K) from (J; j) to (H; h) is a 2-cell  : J ) H in K subject
to the evident axiom expressing coherence with respect to j and h, i.e.,
the following diagram commutes:
2.6 Example ([16]) Suppose we are given a language (without variable
binding) generated by a signature. The denotational models of this language
are given by -algebras on Set, where  is functor dened by
where  varies over signature. A -algebra is a set X together with a map
equivalently an interpretation of each  on the set X . In general,
each polynomial functor on Set freely generates a monad on Set, so there exists
a monad on Set such that -alg is isomorphic to T -Alg, the category
of Eilenberg-Moore algebras for the monad In this case, the set
for a set X is the set of terms freely generated by the signature applied to X .
Next suppose we are given  and  0 . The endofunctors freely generate
monads
lifts uniquely to a natural transformation such that (Id; t) is a
morphism from (Set; T Mnd(Cat). The X component
of t is a map from TX to T 0 X , i.e., a map which sends each term generated by
to a term generated by  0 respecting the term structure. So translation of
languages can sometimes be captured as a morphism of monads.
2.7 Example ([16]) Consider
A  1 -algebra consists of a set X together with a constant nil
each element a 2 A an atomic action a:
Now consider a second language  2
by adding parallel operator jj to the
signature of  1 . The corresponding polynomial functor is given by
For these two languages  1 and  2 , we can give an example of a natural
transformation  1
by dening the X component to be the inclusion of
X into the rst and second components of  2
X .
Both endofunctors
freely generate monads
spectively. The natural transformation induced by the above natural
transformation from  1
to  2
is the inclusion of T 1
X .
Finally in this section, we mention a dual construction. For any 2-category
K, one may consider the opposite 2-category K op , which has the same 0-cells
as K but K op composition induced by that of K. This
allows us to make a dierent construction of a 2-category of monads in K, as
we could say
2.8 Denition For a 2-category K, dene Mnd
Analysing the denition, a 0-cell of Mnd  (K) is a monad in K; a 1-cell from
together with a 2-cell
subject to two coherence axioms, expressing coherence
between  and  0 and between  and  0 ; and a 2-cell from (J; j) to (H; h) is a
2-cell in K from J to H subject to one axiom expressing coherence with respect
to j and h. The central dierence between Mnd(K) and Mnd  (K) is in the
1-cells, because j is in the opposite direction.
3 Eilenberg-Moore constructions
In this section, we develop our denitions of the previous section, in particular
that of Mnd(K), by characterising the Eilenberg-Moore constructions in terms
of the existence of an adjoint to a inclusion 2-functor [15].
For each 2-category K, there is a forgetful 2-functor U
sending a monad (C; in K to its underlying object C. This 2-functor
has a right 2-adjoint given by the 2-functor Inc sending an
object X of K to (X; id; id; id), i.e., to X together with the identity monad on
it. The denition of Mnd(K) and analysis of it are the central topics of study
of [15], a summary of which appears in [8].
3.1 Denition A 2-category K admits Eilenberg-Moore constructions for monads
if the 2-functor Inc : K ! Mnd(K) has a right 2-adjoint.
3.2 Remark Note in general what the above 2-adjunction means. There is an
isomorphism between two categories for each monad
X in K:
We denote the T-component " of the counit by a pair
@ @
@ @
@
R
Then the universality for 1-cells means that for each 1-cell (J;
for each 1-cell J and each 2-cell
satisfying coherence conditions, there exists a unique 1-cell J
K such that U T J
Next, the universality for 2-cells means that for each 2-cell  : (J;
subject to a
coherence condition, there exists a unique 2-cell
K such that U T  are implied by the universality
for 1-cells.
3.3 Proposition If has a right
2-adjoint given by the Eilenberg-Moore construction for a monad on a small
category.
Proof Let be a monad in Cat. We have a forgetful functor
be a natural transformation
given by u . Then we have a
We show that this 1-cell satises
the universal property.
Given a category X and given a map (J;
a functor
objects by putting
Ja, and arrows by sending f : a ! b to Jf : Ja ! Jb. Then we have
Mnd(Cat). The unicity of [
(J;
For 2-dimensional property, let  : (J; be a 2-cell in Mnd(Cat),
Ha for each object a in X , then b  :
turns out to be a natural transformation by coherence condition of . It is
easy to show that this b
is the unique natural transformation which satises
3.4 Remark Note here what the universal property says: it says that for any
small category X and any small category C with a monad T on it, there is a
natural isomorphism of categories between [X; T -Alg] and the category for which
an object is a functor J together with a natural transformation TJ )
J subject to two coherence conditions generalising those in the denition of T -
algebra. This is a stronger condition than the assertion that every adjunction
gives rise to a unique functor into the category of algebras of the induced monad.
3.5 Example If V has equalisers, then V -Cat admits Eilenberg-Moore constructions
for monads, and again, the construction is exactly as one expects.
This is a fundamental observation underlying [15].
3.6 Proposition Suppose K admits Eilenberg-Moore constructions, i.e., the
2-functor Inc has a right 2-adjoint K. Then for any 0-cell
of there exists an adjunction hF T
T-Alg in the 2-category K that generates the monad T.
Proof The proof is written in [15].
Consider the 1-cell Mnd(K). By using the universality
for 1-cells, we have a unique 1-cell F T-Alg such that u T F
U be the unit  of the monad
the 2-cell in K is a 2-cell from
by using the universality for 2-cells,
there exists a unique 2-cell "
Again by the universal property, U T ("
implies that " T F T  F T  By using the equation (1) and the coherence
Hence we can show the existence
of an adjunction in the 2-category K.
3.1 Liftings to Eilenberg-Moore constructions
Now assume K admits Eilenberg-Moore constructions for monads. For each
we call the 0-cell T-Alg in K an Eilenberg-Moore
construction for the monad T. Here, we investigate the existence and nature of
liftings of 1-cells to Eilenberg-Moore constructions at the level of generality we
have been developing.
3.7 Denition Let
Mnd(K). A 1-cell lifts to a 1-cell
J on Eilenberg-Moore
constructions if the following diagram commutes in K.
T-Alg
3.8 Denition Suppose both 1-cells lift to
respectively
on Eilenberg-Moore constructions. A 2-cell  : J lifts to a 2-cell
H on Eilenberg-Moore constructions if the equation U T 0
holds.
Lemma The right adjoint 2-functor sends each
1-cell in Mnd(K) to a lifting of J , and each
to a lifting of
Proof By using the 2-naturality of the counit, the following diagram commutes
for 1-cells (J;
Inc(T-Alg)
Inc((J; j)-Alg)
Hence we have U T 0
Similarly, naturality for a 2-cell  : (J; implies the equation
Conversely, every lifting arises uniquely from Mnd(K).
3.10 Theorem Suppose a 1-cell lifts to
Eilenberg-Moore constructions for monads
Then there exists a unique 1-cell (J; in Mnd(K) such that (J;
J .
Suppose both 1-cells lift to
tively, arising from 1-cells (J; j); (H; respectively, i.e., (J;
and (H;
H . If a 2-cell  lifts to
H on Eilenberg-
Moore constructions, then  is a 2-cell in Mnd(K) from (J; j) to (H; h) such
that
.
Proof Given
Jid =========
id
For this 2-cell j, note that j   0
a 1-cell from the T to T 0 . Since (J; j)-Alg is the unique 1-cell
such that u T 0
need only show that Ju T  jU
J .
But equation (1) implies Ju T  jU
J . So by
universality, we have (J;
J .
By denition of ( )-Alg, the 2-cell -Alg : (J; j)-Alg ) (H; h)-Alg is the
unique one such that U T 0
universality for 2-cells implies
.
3.11 Corollary Liftings of 1-cells to Eilenberg-Moore constructions are equivalent
to 1-cells in Mnd(K). Liftings of 2-cells to Eilenberg-Moore constructions
are equivalent to 2-cells in Mnd(K).
Given an arbitrary 2-category K, we have constructed the 2-category Mnd(K)
of monads in K. Modulo size, this construction can itself be made 2-functorial,
yielding a 2-functor Mnd : 2-Cat ! 2-Cat, taking a small 2-category K
to Mnd(K), with a 2-functor G sent to a 2-functor
similarly for a 2-natural transformation. In fact,
the 2-category 2-Cat forms a 3-category, and the 2-functor Mnd extends to a
3-functor, but we do not use those facts further in this paper, so we do not give
the deninitions here. It follows that, given a 2-adjunction F a U : K ! L, one
obtains another 2-adjunction Mnd(F ) a
shall use this fact later.
4 Kleisli construction
In this section, we consider a dual to the work of the previous section. This
is not just a matter of reversing the direction of every arrow in sight. But by
putting we can deduce results about Mnd  (K) from results about
Mnd(L). In particular, we have
4.1 Proposition
1. The construction Mnd  (K) yields a 2-functor Mnd  : 2-Cat ! 2-Cat.
2. The forgetful 2-functor U : Mnd  (K) ! K has a left 2-adjoint given by
sending an object X of K to the identity monad
on X .
We can characterise Kleisli constructions by using the 2-category Mnd  (K).
We can show the following by the dual argument to Proposition 3.3.
4.2 Proposition If has a left
2-adjoint given by the Kleisli construction for a monad on a small category.
Spelling out the action of the 2-functor ( )-Kl : Mnd  (Cat) ! Cat on 1-cells
and 2-cells, a 1-cell (J; sent to the functor
which sends an object a of T-Kl to the object Ja of
and an arrow f : a ! b of T-Kl, i.e., an arrow ^
of C, to the
arrow of T 0 -Kl given by j b  J
to the natural transformation -Kl : (J; j)-Kl ) (H; h)-Kl whose a component
is given by  0
Ha   a
The above construction and proof extend readily to the case of
In light of this result, we say
4.3 Denition A 2-category K admits Kleisli constructions for monads if the
has a left 2-adjoint.
4.4 Proposition Suppose a 2-category K admits Kleisli constructions for
monads. with the left 2-adjoint to Inc given by K. For
any 0-cell there is an adjunction hFT
in K that generates the monad T.
Proof Dual to the proof of Proposition 3.6.
4.1 Liftings to Kleisli constructions
Now we assume a 2-category K admits Kleisli constructions for monads. For
each monad in K we call T-Kl a Kleisli construction for the
monad T.
We can dene the liftings to Kliesli constructions as follows:
4.5 Denition Let
Mnd  (K). A 1-cell lifts to a 1-cell
constructions if the following diagram commutes in K.
T-Kl
FT 0We can also dene the notion of a lifting of a 2-cell.
4.6 Denition Suppose 1-cells lift to
Kleisli constructions. A 2-cell  lifts to a 2-cell
H on Kleisli
constructions if the equation
holds.
Since Mnd  we remark that
Lemma The following two conditions are equivalent.
1. K admits Kleisli constructions for monads.
2. K op admits Eilenberg-Moore constructions for monads.
So, dualising Theorem 3.10, we have
4.8 Theorem Suppose a 1-cell lifts to
constructions for monads
exists a unique 1-cell (J;
J .
Suppose both 1-cells lift to
respectively,
arising from 1-cells (J; j); (H; respectively, i.e., (J;
J and
H . If a 2-cell  lifts to
H on Kleisli constructions,
then  is a 2-cell in Mnd  (K) from (J; j) to (H; h) such that
.
4.9 Corollary Liftings of 1-cells to Kleisli constructions are equivalent to 1-
cells in Mnd  (K). Liftings of 2-cells to Kleisli constructions are equivalent to
2-cells in Mnd  (K).
5 Comonads in 2-categories
We now turn from monads to comonads. The results we seek about comonads
follow from those about monads by consideration of another duality applied to
an arbitrary 2-category. Given a 2-category K, one may consider two distinct
duals: K op as in the previous section and K co . The 2-category K co is dened
to have the same 0-cells as K but with K co (X; Y ) dened to be K(X;Y ) op .
In K op , the 1-cells are reversed, but the 2-cells are not, whereas in K co , the
2-cells are reversed but the 1-cells are not. One can of course reverse both 1-cells
and 2-cells, yielding K coop , or isomorphically, K opco .
5.1 Denition A comonad in K is dened to be a monad in K co , i.e., a 0-cell
C, a 1-cell subject to the
duals of the three coherence conditions in the denition of monad.
Taking a comonad in K as we have just dened it is exactly a
small category together with a comonad on it.
One requires a little care in dening Cmd(K), the 2-category of comonads
in K. If one tries to dene Cmd(K) to be Mnd(K co ), then there is no forgetful
2-functor from Cmd(K) to K.
5.2 Denition For a 2-category K, dene Cmd(K) to be Mnd(K co ) co .
Explicitly, a 0-cell in Cmd(K) is a comonad in K. A 1-cell in Cmd(K) from
together with a 2-cell
subject to two coherence conditions, one relating  and  0 , the
other relating  and  0 . A 2-cell from (J; j) to (H; h) is a 2-cell in K from J to
H subject to one coherence condition relating j and h.
Note carefully the denition of a 1-cell in Cmd(K). It consists of a 1-cell
and a 2-cell in K; of those, the 1-cell goes in the same direction as that in the
denition of Mnd(K), but the 2-cell goes in the opposite direction.
5.3 Example In [16], categories of coalgebras for behaviour endofunctors on
are used. Examples are
P! is the nite powerset functor. A B 1 -coalgebra is a set X together with
a
A-labelled transition system. A B 2
coalgebra is a nitely branching A-labelled transition system. B 1
-coalgebras are
used for deterministic processes and B 2 -coalgebras are used for nondeterministic
processes.
Similar to the algebras for endofunctors, endofunctors like
on Set
cofreely generate comonads, i.e., there exist comonads (D
respectively on Set such that B 1
-Coalg.
Suppose endofunctors B and B 0 cofreely generate comonads D and D 0 re-
spectively. Then every natural transformation between two behaviour
functors generates a natural transformation d : D ) D 0 such that (Id; d) is a
morphism from D to D 0 in Cmd(Cat). This analysis can be extended to consider
natural transformations from D to B 0 , but we do not have examples at that full
level of generality.
For the above endofunctors B 1 and B 2 , we can consider the natural transformation
whose X component sends  to ; and (a; x) to f(a; x)g. It
generates a comonad morphism from D 1
to D 2
Also, one may dene Cmd  Since the operations ( ) op
and ( ) co commute, we have
5.4 Proposition For any 2-category K, Cmd
5.1 Eilenberg-Moore constructions for comonads
Just as in the situation for monads, there is an underlying 2-functor U
K, which has a right 2-adjoint given by Inc sending an object
X to the identity comonad on X ; and again, one may say
Denition A 2-category K admits Eilenberg-Moore constructions for comon-
has a right 2-adjoint.
Although not stated explicitly in [15], it follows routinely that the 2-category
Cat admits Eilenberg-Moore constructions for comonads, and they are given by
the usual Eilenberg-Moore construction. Again here, the construction Cmd(K)
yields a 2-functor Cmd : 2-Cat ! 2-Cat.
5.6 Proposition Suppose a 2-category K admits Eilenberg-Moore constructions
for comonads. We denote the right 2-adjoint by
For any 0-cell of Cmd(K), there is an adjunction hU D ; G D ;
in K that generates the comonad D .
Proof Dual to the proof of Proposition 3.6.
5.1.1 Liftings to Eilenberg-Moore constructions
Now, dually to the case for monads, assume K admits Eilenberg-Moore constructions
for comonads. For each comonad in K, we call
D -Coalg an Eilenberg-Moore construction for D .
5.7 Denition Let
Cmd(K). A 1-cell lifts to a 1-cell
Eilenberg-Moore constructions if the following diagram commutes in K.
U D
Denition Suppose 1-cells lift to
0 -Coalg on Eilenberg-Moore constructions. A 2-cell  : J lifts to a 2-cell
H on Eilenberg-Moore constructions if U D 0
we remark that
Lemma The following two conditions are equivalent.
1. K admits Eilenberg-Moore constructions for comonads.
2. K co admits Eilenberg-Moore constructions for monads.
So, dualising Theorem 3.10, we have
5.10 Theorem If
-Coalg is a lifting of a 1-cell J
Eilenberg-Moore constructions, then there is a unique 1-cell (J;
in Cmd(K) such that (J;
J .
Suppose 1-cells
respectively. If a 2-cell
in K is a lifting of a 2-cell  : J
is a 2-cell in Cmd(K) from (J; j) to (H; h) such that
.
5.11 Corollary Liftings of 1-cells to Eilenberg-Moore constructions are equivalent
to 1-cells in Cmd(K). Liftings of 2-cells to Eilenberg-Moore constructions
are equivalent to 2-cells in Cmd(K).
5.1.2 Liftings to Kleisli constructions
Now assume K admits Kleisli constructions for comonads. For each comonad
in K, we call D -CoKl a Kleisli construction for the comonad D .
5.12 Denition Let
Cmd  (K). A 1-cell lifts to a 1-cell
Kleisli constructions if the following diagram commutes in K.
F DJ
Denition Suppose 1-cells lift to
-CoKl respectively on Kleisli constructions. A 2-cell  lifts to a
2-cell
H on Kleisli constructions if
Similarly to Lemma 4.7,
Lemma The following two conditions are equivalent.
1. K admits Kleisli constructions for comonads.
2. K op admits Eilenberg-Moore constructions for comonads.
Once again by dualising Theorem 3.10, we have
5.15 Theorem If
-CoKl is a lifting of a 1-cell
C 0 to Kleisli constructions for comonads, then there is a unique 1-cell (J;
J .
Suppose 1-cells
respectively. If a 2-cell
(H; h)-CoKl in K is a lifting of a 2-cell  : J is a 2-cell in Cmd  (K)
from (J; j) to (H; h) such that
.
5.16 Corollary Liftings of 1-cells to Kleisli constructions for comonads are
equivalent to 1-cells in Cmd  (K). Similarly, liftings of 2-cells to Kleisli constructions
for comonads are equivalent to 2-cells in Cmd  (K).
In previous sections, we have dened 2-functors Mnd, Mnd  , Cmd and Cmd  .
So in principle, one might guess that there are eight possible ways of combining
a monad and a comonad as there are three dualities: start with the monad or
start with the comonad; taking ( )  on the monad or not; and likewise for the
comonad. In fact, as we shall see, there are precisely six. First we analyse the
2-functor CmdMnd. In order to do that, we give the denition of a distributive
law of a monad over a comonad in a 2-category.
6.1 Denition Given a monad on an object
C of a 2-category K, a distributive law of T over D is a 2-cell
which satises the laws involving each of , ,  and :
6.2 Denition For any 2-category K, the following data forms a 2-category
Dist(K) of distributive laws :
A 0-cell consists of a 0-cell C of K, a monad T on it, a comonad D on it,
and a distributive law  : TD ) DT .
consists of a 1-cell
together with a 2-cell subject to the
monad laws, together with a 2-cell in K of the form
subject to the comonad laws, all subject to one coherence condition given
by a hexagon
JTD
@
@ @
@
@
R
@ @
@ @
@
R
A 2-cell from (J; consists of a 2-cell from J to H in K
subject to two conditions expressing coherence with respect to j t and h t
and coherence with respect to j d and h d .
6.3 Proposition For any 2-category K, the 2-category CmdMnd(K) is isomorphic
to Dist(K).
Thus Dist(Cat) gives as 0-cells exactly the data considered by Turi and
Plotkin [16]. Turi and Plotkin did not, in that paper, address the 1-cells of
but they propose to do so in future. The 0-cells provide them with
a combined operational and denotational semantics for a language; the 1-cells
allow them to account for the interpretation of one language presented in such
a way into another language thus presented. In fact, it was in response to
Plotkin's specic proposal about how to do that that much of the work of this
paper was done. For a simple example, one might have a monad and comonad
on the category Set, and embed it into the category of !-cpo's in order to add
an account of recursion.
6.4 Example We give an example of a distributive law for a monad over a
comonad. Let be the monad on Set sending a set X to the set X  of -
nite lists, and let (D; ; ) be the comonad that sends a set X to the set of streams
. Consider the natural transformation  : TD ) DT whose X component
sends a nite list of streams
a 1
a 2
an with
a i1 a i2 a i3    ; (1  i  n) to
the stream of nite lists (a 11 a 21
an1 )(a 12 a 22
an2 )(a 13 a 23
an3 )    . This
natural transformation satises the axioms for a distributive law of a monad
over a comonad. Hence these data give an example of a 0-cell of CmdMnd(Cat).
It also becomes a 0-cell of both Cmd  Mnd(Cat) and Mnd  Cmd(Cat) later.
6.5 Example The distributive laws in [16] are given in the following manner.
For a given language  and a suitable behaviour B, Turi and Plotkin model a
GSOS rule by a natural transformation (Id B) ) BT , where is the
monad freely generated by the endofunctor . They then show that the monad
lifts to B-coalg the category of B-coalgebras for the endofunctor B,
which means T ;  and  lift.
B-coalg
~
for the comonad (D; ; ) cofreely generated by B,
this diagram is equivalent to the lifting diagram for the monad to the
category of Eilenberg-Moore coalgebras for the comonad D . By Theorem 3.10,
this is equivalent to one datum and two conditions:
a natural transformation
a 1-cell of Cmd(Cat).
the natural transformation a 2-cell from (T ; ) 2 to
the natural transformation  : a 2-cell from Id to (T ; ) in
Cmd(Cat).
Hence it is equivalent to give a distributive law  : TD ) DT .
A corollary of Proposition 6.3, which although easily proved, is conceptually
fundamental, is
6.6 Corollary CmdMnd(K) is isomorphic to MndCmd(K).
Proof It is easily to check that Dist(K) is isomorphic to Dist(K co ) co . Since
6.7 Theorem Suppose K admits Eilenberg-Moore constructions for monads
and comonads. Then, Inc : K ! CmdMnd(K) has a right 2-adjoint.
Proof Since K admits Eilenberg-Moore constructions for monads, Inc
Mnd(K) has a right 2-adjoint. Since Cmd : 2-Cat ! 2-Cat is a 2-functor, it
sends adjunctions to adjunctions, so Cmd(Inc)
a right 2-adjoint. Since K admits Eilenberg-Moore constructions for comonads,
has a right adjoint. Composing the right adjoints gives
the result.
This result gives us a universal property for the construction of the category
of -Bialgebras, given a monad T, a comonad D , and a distributive law of T
over D. In this precise sense, one may see the construction of a category of
bialgebras as a generalised Eilenberg-Moore construction.
Using Proposition 6.3 and Corollary 6.6, we may characterise the right 2-
adjoint in three ways, giving
6.8 Corollary If K admits Eilenberg-Moore constructions for monads and
comonads, then given a distributive law of a monad
the following are equivalent:
-Bialg determined directly by the universal property of a right 2-adjoint
to the inclusion Inc sending X to the identity distributive
law on X
the Eilenberg-Moore object for the lifting of T to D -Coalg
the Eilenberg-Moore object for the lifting of D to T-Alg.
By the universal property, the right 2-adjoint ( )-Bialg inherits an action on
1-cells and 2-cells. The behaviour of the right 2-adjoint on 0-cells gives exactly
the construction ( )-Bialg studied by Turi and Plotkin [16]. Its behaviour on
1-cells will be fundamental to their later development as outlined above.
More concretely, the right 2-adjoint sends each 1-cell (J;
-Bialg such that the following diagram
commutes, where U  : -Bialg ! C is the canonical 1-cell.
-Bialg
U
It also sends each 2-cell  to a 2-cell -Bialg :
satisfying the equation U  0
6.9 Remark Although all 1-cells and 2-cells in MndCmd(K) give liftings to
bialgebras, we do not have a converse as we cannot construct the data for a
1-cell in MndCmd(K) from a given lifting.
6.10 Example Consider the Eilenberg-Moore construction, i.e., the category
of -bialgebras, for the monad, comonad, and distributive law  of Example
6.4. Since the comonad (D; ; ") is cofreely generated by the endofunctor
on Set, D-Coalg is isomorphic to Id-coalg, the category of coalgebras for the
endofunctor Id; this is the category of deterministic dynamical systems. Hence
every object of D-Coalg can be seen as a dynamical system
(X; ) with state space X and transition function
The Eilenberg-Moore construction T-Alg for the monad T is as follows: each
object is a semigroup X with a structure map h which sends a list
of elements to their composite.
So the category -Bialg for the distributive law  : TD ) DT is as follows.
An object of -Bialg is a dynamical system (X; )
where the state space X is given by a semigroup such that h(x 1 x 2    xn
every nite sequence x 1
xn of X elements.
An arrow f
is a Y that is a morphism of both semigroups and dynamical
systems.
7 Mnd  Cmd  (K)
This section is essentially about Kleisli constructions, considering the complete
dual to the previous section. One can deduce from Corollary 6.6
7.1 Corollary Mnd  Cmd  (K) is isomorphic to Cmd  Mnd  (K).
Moreover, one can deduce an equivalent result to Proposition 6.3: this yields
that the isomorphic 2-categories of Corollary 7.1 amount to giving the opposite
distributive law to that given by Cmd and Mnd, and hence give an account of
Kleisli constructions lifting along Kleisli constructions. The left 2-adjoint to
can again be characterised in three ways:
7.2 Corollary If K admits Kleisli constructions for monads and comonads,
then given a distributive law of a comonad (D; ; ) over a monad
following are equivalent:
-Kl determined directly by the universal property of the inclusion Inc :
sending X to the identity distributive law on X
the Kleisli object for the lifting of T to D -Kl
the Kleisli object for the lifting of D to T-Kl
This is the construction proposed by Brookes and Geva [2] for giving intensional
denotational semantics.
The fundamental step in the proof here lies in the use of the proof of Theorem
6.7, and that proof relies upon the following: some mild conditions on K
hold of all our leading examples, allowing us to deduce that K admits Eilenberg-
Moore and Kleisli constructions for monads and comonads; and each of the
constructions Mnd, Mnd  , Cmd and Cmd  is 2-functorial on 2-Cat, so preserves
adjunctions.
Spelling out the action of the 2-functor on 1-cells and 2-cells, a 1-cell (J;
sent to the 1-cell J-Kl : -Kl !  0 -Kl such that
the following diagram commutes:
-Kl
F J
F  0Here F  and F  0
are canonical 1-cells.
sent to the 2-cell -Kl
such that -KlF
7.3 Remark Although all 1-cells and 2-cells in Mnd  Cmd  (K) give liftings to
Kleisli constructions for monads and comonads, we can not have a converse as
we cannot construct the data for a 1-cell in Mnd  Cmd  (K) from a lifting.
7.4 Proposition When Cat, the Kleisli construction for monads and
comonads exists and is given as follows. Let (D; ; ) be a comonad and
be a monad on C and  : DT ! TD be a distributive law on D and T . Then
the objects of -Kl are the those of C. An arrow from x to y in -Kl is given by
an arrow f : Dx ! Ty in C. For each object x, the identity is given by  x   x .
The composition of arrows f z in -Kl seen as arrows
in C is given by the composite  z
f) x
in C.
Proof We need only write the image under the left 2-adjoint Inc
Cmd  Mnd  (Cat). This left adjoint is given by composing the two left 2-adjoints
as in Theorem 6.7: the 2-functor Cmd  applied to the Kleisli construction of T ,
and the Kleisli construction of D.
Now we give an example of a distributive law of a comonad over a monad,
hence a 0-cell of Cmd  Mnd  (K), and the Kleisli construction for a monad and
comonad.
7.5 Example Let (P;
fg) be the powerset monad on Set, i.e., the powerset
functor P and union operation S
mapping
a comonad on Set where the endofunctor D
sends a set X to the product set A  X for some set A. Consider the natural
component sends a pair (a; ) of an
element a of A with  2 P (X) to the set f(a; x)jx 2 g. This satises the
axioms for a distributive law of a comonad over a monad. Hence this gives an
example of a 0-cell in Cmd  Mnd  (Cat). It also turns out to be a 0-cell in both
CmdMnd  (Cat) and MndCmd  (Cat).
This distributive law is essentially the same as the one in Power and Turi's
paper [13]. Their monad is the nonempty powerset monad on Set.
7.6 Example Applying Proposition 7.4, we spell out the Kleisli construction
-Kl for the monad and comonad given in the above example. The objects
of the category -Kl are the those of Set. An arrow from X to Y in -Kl is
given by a The identity arrow for each object X
is given by the map sends a pair (a; x) to
the singleton fxg. The composition of arrows
-Kl seen as maps ^
composite
sends (a; x) to the
subset
f(a; x)g of Z.
8 The other four possibilities
Applying the work of previous sections to the remaining four possible combinations
of a monad with a comonad, we can summarise the various 2-categories
by the following table, including the previous 2-categories.
Each 2-category is dened as follows.
A 0-cell consists of a 0-cell C of K, a monad T on it, a comonad D on it,
and a distributive law  whose direction is listed in the second column of

Table

1.

Table

1: Distributive laws
Cmd  Mnd TD
Mnd  Cmd TD
CmdMnd
MndCmd  DT
Cmd  Mnd
consists of a 1-cell J :
together with a 2-cell j t with direction in the third column,
subject to monad laws, and a 2-cell j d in the fourth column, subject to
comonad laws, all subject to to one coherence hexagon.
A 2-cell from (J; consists of a 2-cell from J to H in K
subject to two conditions expressing coherence with respect to j t and h t
and coherence with respect to j d and h d .
8.1 Remark As described in the Table 1, the 2-categories CmdMnd(K);Cmd  Mnd(K)
and Mnd  Cmd(K) have the same 0-cells, and CmdMnd  (K); MndCmd  (K) and
Cmd  Mnd  (K) have the same 0-cells.
In considering the possible ways of combining a pair of categories each with
a monad and a comonad, there appear three possible independent dualities:
or the dual
or the dual
or the dual.
This gives eight possibilities, but we can see from above list that two of them
do not arise. The two that do not arise are
and the complete dual, dualising all three items,
8.1 Cmd  Mnd(K)
Consider Cmd  Mnd(K). When K admits Kleisli constructions for comonads
and Eilenberg-Moore constructions for monads, we can consider the Kleisli construction
for a comonad lifting to the Eilenberg-Moore object for the monad.
In detail, for a 0-cell (C; T;
and a comonad distributive law  : TD ) DT , we rst
lift the comonad D on to the Eilenberg-Moore construction for the monad T by
applying the 2-functor Cmd  to obtain
the comonad (T-Alg; (D; )-Alg; -Alg; -Alg) in Cmd  (K). Then we apply the
2-functor ( )-CoKl to obtain the Kleisli construction for the comonad. Observe
that the composition 2-functor ( )-CoKlCmd  (( )-Alg) cannot be characterised
as a left or right 2-adjoint functor to Inc.
When construction gives the following category for a given
Mnd(Cat). Objects are the Eilenberg-Moore algebras
for the monad T. An arrow f from h : y is an arrow
in C such that k . For each T-algebra h :
the identity arrow is given by the arrow  x
8.2 Example Applying the above construction to the 0-cell given in Example
6.4, we have the following category. An object is a T-algebra for the monad T,
hence it is a semigroup arrow f from a semigroup
to Y is a morphism of semigroups from the semigroup
to k, where the multiplication of h ! is dened by
8.2 Mnd  Cmd(K)
When K admits Eilenberg-Moore constructions for comonads and Kleisli construction
for monads, we have a composite 2-functor ( )-KlMnd
Mnd  Cmd(K) ! K. This functor sends each 0-cell of Mnd  Cmd(K) to the
Kleisli construction for the monad lifted to the Eilenberg-Moore construction
for the comonad.
Spelling out the above construction when Cat, the construction sends
each to the following category. Objects are D -coalgebras. An
arrow from is an arrow f in C such
that Df
8.3 Example Recall Example 6.4, the example of a distributive law of a
monad over a comonad and consider the above construction. It yields the
following category. Objects are D -coalgebras, hence deterministic dynamical
systems. An arrow f from a dynamical system (X; ) to (Y; ) is a morphism
of dynamical systems from (X; ) to (Y  ;   ) where (Y  ;   ) is the dynamical
system whose state space is given by the set of nite lists Y  of the set Y and
with transition function   given by   (y 1 y 2
yn
8.3 CmdMnd  (K)
When K admits Eilenberg-Moore constructions for comonads and Kleisli constructions
for monads, we have a 2-functor (
K, which sends each 0-cell to an Eilenberg-Moore construction for the comonad
lifted to the Kleisli construction for the monad.
Spelling out the construction when sends each 0-cell (C; T;
to the following category. An object is an arrow h in C such
that T  x  An arrow from
TDy is an arrow f : x ! Ty in C such that
Dy
These conditions on both objects and arrows are strict. One can consider
application of this construction to the distributive law given in Example 7.5.
Each object is a hence a labelled transition system,
but the rst equation on objects says that every state x 2 X can only have
transitions to itself with labels in A.
8.4 Remark In the above example, the 0-cell constructed by the Eilenberg-
Moore construction for a comonad lifted to the Kleisli construction for a monad
is restrictive. In [13], by forgetting the counit and comultiplication of a given
comonad, Power and Turi considered the category of coalgebras for an endofunctor
rather than a comonad on the Kleisli category for the monad, where they
used only distributivity for the nonempty powerset monad and the A-copower
endofunctor. In order to provide a framework for their example, we need to
investigate the 2-category of endo-1-cells in K.
8.4 MndCmd  (K)
When K admits Kleisli constructions for comonads and Eilenberg-Moore constructions
for monads, we have a 2-functor (
K sending each 0-cell to the Eilenberg-Moore construction for the monad lifted
to the Kleisli construction for the comonad.
Spelling out the construction when sends each 0-cell (C; T;
to the following category. An object is an arrow h in C such
that h  D An arrow from
y is an arrow f : Dx ! y in C such that
f  Dh
We can also apply this construction to the distributive law in Example 7.5,
but we cannot see any concrete meaning to the objects and arrows in that
category.



--R


Categories in Computer Science
Axiomatic domain theory in categories of partial maps
An initial algebra approach to the speci

Adjoint lifting theorems for categories of algebras

Review of the elements of 2-categories
Foundational Methods in Computer Science
Liftings and Kleisli extensions
Notions of computation and monads
Lifting theorems for Kleisli categories.
A Coalgebraic Foundation for Linear Time Semantics
Initial algebra and
The formal theory of monads
Towards a mathematical operational seman- tics
--TR
Notions of computation and monads
Axiomatic domain theory in categories of partial maps
Initial Algebra and Final Coalgebra Semantics for Concurrency
Lifting Theorems for Kleisli Categories
Towards a Mathematical Operational Semantics

--CTR
Marco Kick , John Power , Alex Simpson, Coalgebraic semantics for timed processes, Information and Computation, v.204 n.4, p.588-609, April 2006
Marina Lenisa , John Power , Hiroshi Watanabe, Category theory for operational semantics, Theoretical Computer Science, v.327 n.1-2, p.135-154, 25 October 2004
Paul-Andr Mellis, Comparing hierarchies of types in models of linear logic, Information and Computation, v.189 n.2, p.202-234, March 15, 2004
algebra;coalgebra;monad;comonad;2-category;distributive law;kleisli construction;bialgebra