Arrows are Strong Monads
Kazuyuki Asada
Research Institute for Mathematical Sciences, Kyoto University,
Kyoto 606-8502, Japanasada@kurims.kyoto-u.ac.jp

Abstract
Hughes’ arrows were shown, by Jacobs et al., to be roughly monads in the bicategory Prof of profunctors (distributors, modules).
However in their work as well as others’, the categorical nature of
the first operator was not pursued and its formulation remained
rather ad hoc. In this paper, we identify first with strength fora monad, therefore: arrows are strong monads in Prof . Strong
monads have been widely used in the semantics of functional programming after Moggi’s seminal work, therefore our observation
establishes categorical canonicity of the notion of arrow.
Categories and Subject Descriptors F.3.2 [Logics and Meanings
of Programs]: Semantics of Programming Languages—Denotationalsemantics
General Terms Languages, Theory
Keywords arrow, strong monad, Freyd category, computational
effect, profunctor

1.

In this way we have got a clean understanding of the categorical nature of arrows—except for the first operator. It is our
main result that identifies first with a strength for a monad inProf . Therefore: arrows are strong monads in Prof . The notionof strength for a monad is employed in Moggi’s seminal work [24]in order to accommodate “context information” within computational effects—as the first operator does for arrows. Our main
result (Theorem 14) makes this intuitive analogy a mathematicallyrigorous one.
Use of profunctors in theoretical computer science is not new:
In categorical semantics of programming languages, profunctors—
often called modules (or discrete indexed categories)—are sometimes used instead of usual categories [21, 23]. In [7, 16, 25],
profunctors are used as models in a domain theory for concurrency. Also potential use of profunctors can be seen in recent work:
e.g. [8, 12].
Profunctor can be viewed also as “generalized relation”: a profunctor is to a functor what a relation is to a function. Therefore ourresult is illustrated as:strong monadfunctorfunction==arrow
profunctor
relation .

Introduction

The notion of arrow was introduced by Hughes [17, 18] for functional programming languages such as Haskell. Its benefits areclaimed to be as follows. First, it provides more natural syntax for
Point-free programming; second, it allows programmers to organize a bigger variety of computational effects than the notion ofmonad does.
This paper is about categorical semantics of arrows. There
have been roughly two approaches towards that goal. The firstone employs premonoidal categories with certain additional structure (called Freyd categories) [3, 22, 26]. The other is the approachbased on profunctors (also called distributors or modules) [4, 6],
which we follow.
In the papers [15, 19], Jacobs et al. characterized an arrow as a
monoid in a monoidal category [C op ×C, Set] that is additionallyequipped with the so-called first operator. The monoidal products in the monoidal category [C op ×C, Set] are given by certain
coends; they are in fact the same as composition of profunctors.
Then one readily sees that an arrow is a monad—in an internalsense—in the bicategory Prof of profunctors, equipped with afirst operator.

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
MSFP 2010 September 25, 2010, Baltimore, Maryland, USA.
c 2005 ACM [to be supplied]. . . $10.00
Copyright ⃝We define the notions of arrow and of strong monad in Prof
not only over cartesian categories but over any monoidal categories.
After identifying arrows as strong monads in Prof , we define thenotion of internal strong monad in a general setting, i.e., not only inProf . From this, we obtain some variants of the notion of arrow.
1.1

Relation to Other Work

ist Operator
As we already mentioned, this work follows the profunctor approach that originated in [15, 19]. In these works, they introduced
what they called “internal strength”, i.e., ist operator; then they
showed the equivalence between ist and first. The formulationof ist is pretty similar to that of first, but has certain technicaladvantage, which they exploited.
It should be noted that their ist operator’s definition is quite
different from the genuine internal strength, i.e., the notion ofstrength defined for a monad in an internal way in a bicategory.
The latter is what we call (internal) strength throughout the present
paper.
The notion of strength is a monoidal notion: it is defined for any
monoidal object as in Section 6, and not only for a cartesian object.
On the other hand, the definition of ist operator and the proof ofthe equivalence between ist operator and strength (Theorem 16)
need the structure of cartesian products. Therefore, ist operator
is not what should be called strength. However we can prove ist
operator to be equivalent to strength; the name for ist was with
fortunate wisdom.

Enriched Freyd Category and Self-enrichment
In [3], Atkey investigated many variants of the notion of arrow.
Among them, he gave a categorical definition of arrow and also
defined the notion of enriched Freyd category, and he showed thatthey are equivalent.
Atkey’s definition of arrow and that given in [15, 19] are different: the former is (self-)enriched; the latter is not. This gap between
enriched and non-enriched notions was not present for monads (inCat). This is because in a cartesian closed category—a common
setting for functional programming—strong monads are the samething as enriched monads.
In the present paper, we first give the theorem that arrows
are strong monads in Prof in the non-enriched setting (in Theorem 14), in order to concentrate on other aspects than suchself-enrichment problem. Then, in Section 6, we define a “selfenriched” version of strong monad in Prof in Definition 21, andshow that it is equivalent to Atkey’s definition of arrow in Theorem 23. One technical advantage of our characterization for arrowis that we can define it over any symmetric monoidal category;
while for Atkey’s definition, we use structures of cartesian categories (see Definition 22).
Arrows as Relative Monads
In [1], Altenkirch et al. gave a generalized notion of monad, i.e., thenotion of relative monad. A relative monad is defined over a (base)functor, while a monad is defined over a (base) category. They
showed that for a category C, relative monads over the Yonedab bijectively correspond to (arr,>>>)embedding y : C −→ Cfragments of arrows over C (in Definition 9), and hence to monads
over C in Prof (by Theorem 10).
They gave also a Kleisli construction and an Eilenberg-Moore
construction for a relative monad, and showed that the Kleisli construction gives the initial object and the Eilenberg-Moore construction gives the terminal object in some suitable category. On theother hand, also for a monad in Prof , we have the notions ofKleisli object and Eilenberg-Moore object in Prof , as in the paper [27] by Street.
For a relative monad R over the Yoneda embedding y of acategory C and the corresponding monad A in Prof , the Kleisli
category for R is isomorphic to the Kleisli object for A. They
are isomorphic to the Kleisli category of the corresponding Freyd
category (without premonoidal structures).
One different point between the relative monad approach andour approach in Prof is that the Eilenberg-Moore category for R
is not necessarily equivalent to the Eilenberg-Moore object for A,
which is the same as the Kleisli object for A (because of the duality
Prof ∼= Prof op ). (However the “right adjoint” pseudo functorb(-) : Prof −→ CAT maps the Eilenberg-Moore object for A to
the Eilenberg-Moore category for R.)
Uustalu, the third author of [1], extended the correspondence
between (arr,>>>)-fragments of arrows and relative monads tothat between arrows (with first operators) and strong relative monads [28].

In Section 5, we go straight to the main result that arrows
are strong monads in Prof . Also we give a direct proof of theequivalence between ist operator and strength for a monad inProf . In Section 6, we commence a more general developmentin which strong monads in a Gray-monoid are considered. As abenefit of this generalization, we give some variants of the notion ofarrow: especially in Section 6.3, we give a “self-enriched” versionof strong monad in Prof , which corresponds to Atkey’s definitionof arrow.

2. Background: the Notion of Arrow
The following review to the notion of arrow is brief. See e.g. [19]for more illustration and examples.
The notion of arrow [17, 18] was introduced as an extensionof that of monad [5, 24, 29], and is defined in Haskell as a type
constructor class:class Arrow A wherearr :: (s → t) → A s t( )>>> :: A s t → A t u → A s u
first :: A s t → A (s, u) (t, u)
where (s, t) is the product type of types s and t.
An instance of Arrow must satisfy the following arrow laws:()()
a >>> b >>> c = a >>> b >>> c(assoc)arr (g ◦ f ) = arr f >>> arr g
arr id >>> a = a = a >>> arr id(comp)(id)

first a >>> arr (id × f ) = arr (id × f ) >>> first a(f-din)first a >>> arr π1 = arr π1 >>> a(f-π)

first a >>> arr α = arr α >>> first (first a)(f-α)
first (arr f ) = arr (f × id)()
first a >>> b = first a >>> first b

(f-η)
(f-µ)

where π1 :: (s, t) → s, α :: (s, (t, u)) → ((s, t) , u).
From first, we can define its dual:
second :: A s t → A (u, s) (u, t)second a = arr γ >>> first a >>> arr γ
where γ :: (s, t) → (t, s).
Arrows subsume monads: given a monad T , we obtain its Kleisli
arrow s → T t. Similarly, a comonad S induces its coKleisli arrow
Ss → t. And we can further fit these together: with a distributive
law between a monad and a comonad, we can construct the biKleisli
arrow Ss → T t.

3. Preliminaries
In this section we introduce the notion of profunctor. Before that,
yet, we first recall some necessary notions related to profunctors.

Terminology

3.1 End, Coend and Yoneda Lemmas

In the paper we use the term arrow exclusively for Hughes’ notion,and not for arrows between objects in categories. For the latter, we
reserve the term morphism.

Here we recall the notions of dinatural transformation, end and coend; the two forms of Yoneda lemma, i.e., end form and coend
form; and Reversing Lemma. For further details, see [20] (especially, Sec. 3.10).
Like homset functors C (−, −) : C op ×C → Set or exponentiation bifunctors on SMCCs, we sometimes come across bifunctors
with mixed variance. Dinatural transformations are between suchcontra-co-variant bifunctors F, G : C op × C → D, while naturaltransformations are between functors F, G : C → D.

OutlineIn Section 2, we briefly recall the notion of arrow. In Section 3,
we review the notions of dinatural transformation, end, coend, andprofunctor. In Section 4, we recall the results in [19] that a fragmentof arrow is a monad in Prof .

Definition 1 (Dinatural transformation) For categories C, D, andfunctors F, G : C op × C → D, a dinatural transformation α fromF to G is an indexed family of morphisms
αC : F (C, C) → G (C, C)(C ∈ |C|)

which is dinatural in C, i.e., for any morphism f : C → C ′ thefollowing diagrams commutes:
F (C, C)
hhhh3′
F (C , C) VVV+αC

F (f,C)F (C ′ ,f )F (C ′ , C ′ )αC ′/ G (C, C) G(C,f )VVVV+
G (C, C ′ )
hhh4

C∈C

/ G (C ′ , C ′ )G(f,C ′ )Two successive dinatural transformations do not necessarily
compose, in which sense this notion is not that of “morphism”
between such bifunctors. Nevertheless dinatural transformations
are useful, as we will see many times in the paper.
Note that the notion of dinatural transformation subsume that ofnatural transformation: for given functors F, G : C → D, naturaltransformations between F, G bijectively correspond to dinaturaltransformations between F ◦ π ′ , G ◦ π ′ : C op × C → D. Also
we will see many examples of dinatural transformations where thedomain functors (F above) or the codomain functors (G above) areconstant functors, as in the next definitions of end and coend.
End (resp. coend) is a kind of limit (resp. colimit) where dinatural transformations are used instead of natural transformations.
These notions play a very important role for profunctor theory.
Definition 2 (End and Coend) For categories C, D, and a functor
F : C op × C → D,∫
• an end of F is an object
F (C, C) in D with projection
C∈C
morphisms
(∫
)
(
)
( ′
)
πC ′ :F (C, C) → F C ′ , C ′C ∈ |C|C∈C∫
which form a dinatural transformation from the C∈C F (C, C)constant functor to the functor F . Then these are required to beuniversal among such data: i.e., for any object D in D and′′
any dinatural transformation (αC ′ : D∫ → F (C , C ))C ′ ,there
is a unique morphism f : D → C∈C F (C, C) such that
πC ′ ◦ f = αC ′ for all C ′ .
∫• Dually, a coend of F is an object C∈C F (C, C) in D with
injection morphisms
∫ C∈C
(
)
( ′
)
F (C, C)C ∈ |C|ιC ′ : F C ′ , C ′ →which forms an end of F op : (C op ) op × C op → D op .

The universality of an end and a coend can be written respectively as the following bijective correspondences:∫f : D → C∈C F (C, C)
(1)
( fC
)
D → F (C, C) C dinatural in C
f:
(

∫ C∈C

F (C, C) → D)
fC
F (C, C) →D C dinatural in C

Lemma 3 For a small category C and functors F, G : C op × C →Set, we have the bifunctor [F (+, −) , G (−, +)] : C op × C →Set, where + and − indicate respectively variant and covariant
arguments, and [−, +] is the exponentiation of Set.
Then, denoting the set of all dinatural transformations from F
to G by Dinat (F, G), we have a canonical isomorphism∫[]
Dinat (F, G) ∼F (C, C) , G (C, C) .
=(2)

Proof. Because of the following bijective correspondences:
[ (
)
]
∫
1 → C∈C F C, C , G (C, C)(by (1))([])
1 → F (C, C) , G (C, C) C dinatural in C
(F (C, C) → G (C, C))C dinatural in C
As noted above, natural transformations are subsumed by dinatural transformations. Hence, for functors F, G : C → Set, wehave also a canonical isomorphism∫
Nat (F, G) ∼[F C, GC]=
C∈C

where the left hand side is the set of natural transformations fromF to G. These isomorphisms are useful throughout the paper for
calculating (di)natural transformations, especially in the proof of
Theorem 14.
By the usual Yoneda lemma, for a functor F : C → Set, there
is canonically the natural isomorphism F C ∼= Nat (y (C) , F ).
Replacing the right hand side with the end isomorphic to it, wehave the Yoneda lemma, end-form:
Lemma 4 (The Yoneda lemma, end-form) For a small category
C and a functor F : C → Set, we have a canonical natural
isomorphism
∫
[ (
)
]
FC ∼
C C, C ′ , F C ′ .
=C ′ ∈C

Above, we use the exponentiation [−, −] in Set. This is called
also cotensor in enriched category theory [20], and there is its dual
notion called tensor, which is just cartesian product in the case of
Set. With this we can obtain the dual version of the above Yoneda
Lemma:
Lemma 5 (The Yoneda lemma, coend-form) For a small category
C and a functor F : C → Set, we have a canonical natural
isomorphism∫ C ′ ∈C( )()
F C′ × C C′, C ∼= FC .
Note that we can of course apply the above two lemmas also toa contravariant functor F : C op → Set.
We need also the next lemma in the proof of the main theorem.
As homset functors reverse colimits into limits in the negative
position, they reverse also coends into ends.
Lemma 6 (Reversing Lemma) For a category C and a functor
F : C op × C → Set, we have a canonical natural isomorphism[∫ C∈C] ∫[]F (C, C) , − .
F (C, C) , − ∼=C∈CThe complete and cocomplete category Set has all ends andcoends.
A typical and important example of an end is a set of dinaturaltransformations:

3.2

Profunctor

The notion of profunctor (also called distributor or module) forms
the very basis of our analysis of arrows. The notion dates back forquite a while, and its relevance to theoretical computer science has
been recently recognized [8, 12].
Here we recall the notion of profunctor, the bicategory Prof ,the embedding of Cat into Prof , and tensor product in Prof .
As mentioned in the Introduction, a profunctor is to a functor
what a relation is to a function. This analogy is used repeatedly
for illustration. For further details and illustrations for profunctors,see [4, 6].
Definition 7 (Profunctor) Let C and D be small categories. A
profunctor from C to D is a functor D op × C −→ Set. We denotesuch a profunctor by F : C −→+ D, i.e.,
F : C −→+ D,

a profunctor(3)

F : D op × C −→ Set,a functor

For successive profunctors F : C −→+ D and G : D −→+ E,
their composition G ◦ F : C −→+ E is defined—under the correspondence (3)—as the following functor:
G◦F

E op × C/ Set/ ∫ D∈D G (E, D) × F (D, C)

(E, C)(4)by C (−, −) : C op × C −→ Set .

defF∗ (−, +) = D (−, F +) : D op × C −→ Set(6)′

and maps a natural transformation σ : F =⇒ F : C −→ D to thenatural transformation D (id, σ) : F∗ =⇒ F ′ ∗ : C −→+ D.
This embedding forms a pseudofunctor [6] from the 2-category
Cat to the bicategory Prof , i.e. preserve composition and identities for 1-cells up to iso-2-cells. This embedding corresponds—via
the foregoing analogy—to the embedding of the category Set into
the category Rel of sets and relations, which maps a function to its
graph relation.
As cartesian products in Set lift to tensor products in Rel,cartesian products in Cat lift to tensor products in Prof . For
profunctors F : C −→+ C′ and G : D −→+ D′ , we define F × G :C × D −→+ C′ × D′ by the following:() def ()()(F × G) C ′ , D′ , C, D = F C ′ , C × G D′ , D(7)
It is obvious that the operator × acts also on natural transformations
between profunctors.

Its action on morphisms is the obvious one.
For a category C, we define the identity profunctor
Id++ C
C : C −→We denote by Prof the bicategory consisting of small categories as its 0-cells (objects), profunctors as its 1-cells (morphisms), and 2-cells between profunctor as its 2-cells.
Next we introduce an embedding of Cat into Prof . This is
identity on 0-cells (small categories), maps a functor F : C −→ D
to the following profunctor F∗ : C −→+ D called direct image of
F,

(5)

′

4.

Monad in Prof

Given two parallel profunctors F , F : C −→+ D, a 2-cell
between profunctors σ : F =⇒ F ′ is just a natural transformation
σ : F =⇒ F ′ where F and F ′ are regarded as the functors fromD op × C to Set.
In this short section, we review the result by Jacobs et al. [15, 19]that monads in Prof are equivalent to the (arr,>>>)-fragment ofarrows. This forms also a preliminary step toward our main result,
Theorem 14.

Now, let us illustrate the definition above using the analogy withrelations. A relation R between sets S and T is a subset of the
product set S × T , in other words, a function from S × T to the twopoints set {0, 1}. Thus, a profunctor—F : D op × C −→ Set—is a
Set-many valued relation, while a relation is two valued. Next let
us recall how the relational composition S ◦ R is defined:

4.1 Monads in Prof as Bases of Arrows(S ◦ R) (c, e)

def

⇐⇒

∃d. R (c, d) ∧ S (d, e)

Then there are obvious similarity between∫ Dcomposition for procorresponds to ∃d.,functors (4) and that for relations: coendand × to ∧. Also, 2-cells σ between profunctors F and F ′ , i.e., natural transformations (σD,C : F (D, C) −→ F ′ (D, C))D,C correspond to the inclusion order between relations:()
def
R ≤ R′ ⇐⇒ ∀c.d. R (c, d) ⇒ R′ (c, d) .
This analogy between profunctor and relation will be helpful tounderstand many notions for profunctor.
The notion of 2-category is now used in many different contexts;
in a 2-category, there is a notion of 2-cell, which is “morphism
between morphisms.” A typical example is the 2-category Cat ofcategories, functors, and natural transformations.
One might imagine that the notions of category, profunctor
between categories, and 2-cell between profunctors form a 2category. However, the composition for profunctors is not strictly
associative, because of the coends and products in the definition.
Likewise, identity profunctors are not strictly unital. Nevertheless,they hold up to canonical iso-2-cells; e.g., the iso-2-cells for theunitality can be gotten by the Yoneda lemma, coend-form. Suchnotion which is similar to that of 2-category, but whose associativity and unitality of the composition of 1-cells are required just up
to iso-2-cells, is called bicategory [6].

Many notions in category theory consist of functors and naturaltransformations, subject to some commutative diagrams. For example, an adjunction is a tuple (F, G, η, ϵ) of two functors and twonatural transformations, subject to the two triangular laws [6, Theorem 3.1.5]. Once one takes a 2-categorical view on this—functors
and natural transformations are 1-cells and 2-cells in Cat—it isstraightforward to define an adjunction in an arbitrary 2-category,or in a bicategory, in an “internal” way [27]. The notion of (internal) monad is also one of such.
Definition 8 (Monad) Let P be a bicategory, and C be a 0-cell in
P. A monad over C in P is a triple (A, η, µ) of an endo-1-cell
A : C −→ C in P and 2-cells η : IdC =⇒ A and µ : A2 =⇒ A
in P satisfying the usual commutative diagrams of associativity
and unitality.
It should be noted that this internal definition coincides with theusual one if P = Cat.
Definition 9 ((arr,>>>)-Fragment of Arrow) For a category C,
an (arr,>>>)-fragment of arrow over C consists of a mapping
Ar : |C| × |C| −→ |Set| and two families of mappings:
arrAB : C (A, B) −→ Ar (A, B)>>>ABC : Ar (A, B) × Ar (B, C) −→ Ar (A, C)
These must satisfy Axioms (assoc), (comp), and (id) in Section 2,
where we use variables f, g for morphisms in C, and use a, b, c forelements in (Ar (A, B))A,B .

The map Ar above is a mapping to |Set| rather than |C|. This isunnatural if we use the above definition of arrows to model arrows
as type constructors in Section 2. This involves a subtle size issue,

and we solve it in Section 6.3, till then we shall separate such a size
issue. Here and in the next section, we focus on the correspondence
between arrows and strong monads in Prof .
Theorem 10 [15, 19] For a small category C, the notion of monadover C in Prof is equivalent to that of (arr,>>>)-fragment ofarrow over C.
Proof. (Sketch) Given a monad (A, η, µ) in Prof over a small
category C, A is a functor from C op × C to Set; this corresponds
to the mapping Ar of a fragment of arrow, where the functorialityof A is recovered with arr and >>>. The natural transformations η
has components ηA,B : C (A, B) −→ A (A, B) since C(−, −) isan identity 1-cell in Prof . This corresponds to arr. Finally, µ is,by (4), a natural transformation with components(∫ B)µA,C :A (A, B) × A (B, C) −→ A (A, C) ,which corresponds to >>> by the universality (2) of the coend.

In the remaining sections, we use arr, >>> and η, µ interchangeably, especially in Definition 12.

5.2

first Operator for Monoidal Categories

To give the main theorem for any monoidal categories, here we
generalize the definition of first operators from that for cartesiancategories to that for monoidal categories. (This modification isused in the proof of the main result. It is not an indirect way but
a natural way even for cartesian categories; a cartesian category
seen in Prof is not a “cartesian object” but a monoidal object (seeSection 6) in Prof .)In order to give a categorical definition of first operators formonads in Prof over monoidal categories, we need to modify
Axiom (f-π) (described in Section 2), since a monoidal category
does not necessarily have projections π. For this, we use ρ :A⊗I −→ A instead of π:
Definition 12 [first Operators for Monoidal Categories] For amonoidal category (C, ⊗, I, α, λ, ρ) and a monad (A, η, µ) over C
in Prof , a first operator is a family of morphisms firstA,B,C :A (A, B) −→ A (A⊗C, B⊗C) natural in A, B ∈ C, dinatural in
C ∈ C, and satisfying Axioms (f-α), (f-η), and (f-µ) in Section 2and (f-ρ):
first a >>> arr ρ = arr ρ >>> a

5.

In this section, we present our main result (Theorem 14) that arrows
are strong monads in Prof . We give this theorem not only for
cartesian categories, but for any monoidal categories.
In order to show the main result, we first need to define thenotion of strength in Prof . Then we generalize the definitionof first operator, from that for cartesian categories to that formonoidal categories. Finally we show that these notions of strengthand first are equivalent.
5.1

(f-ρ)

Arrows as Strong Monads in ProfStrength in ProfFirst let us review strength in Cat. A strength for a monad over a
monoidal category (C, ⊗, I) is a natural transformation strA,B :T A⊗B −→ T (A⊗B) satisfying certain axioms. This 2-cell in
Cat can be also described as the following:
C×C

⇐

⊗

T ×IdC

str



C

T

/C×C
⊗


/C

In a similar way, we define the notion of strength in Prof .
Definition 11 (Strength) Let (C, ⊗, I, α, λ, ρ) be a monoidal category, and (A, η, µ) be a monad over C in Prof .
A strength for the monad A in Prof is a 2-cell str in Profin the following diagram such that it satisfies the usual four axioms
with α, ρ, η, µ (for these axioms, see Definition 20).

⊗∗

_


C



A×Id+
C

⇐

C×C

str


A

/C×C
_ ⊗∗


/C

We call a monad in Prof equipped with a strength in Prof astrong monad in Prof .
This is a key notion in the paper. It should be noted that since
the two vertical 1-cells in the above diagram are in Prof , weuse the embedding (6) of Cat into Prof , so that the functor⊗ : C × C −→ C is replaced with its direct image ⊗∗ .

Note that the naturality in A and B above are redundant:
they are derived from Axioms (f-η) and (f-µ). Also note that Axiom (f-din) in Section 2 is equivalent to the dinaturality above.
The propriety of the above definition is justified by the next
proposition:
Proposition 13 In the situation of Definition 12, if the monoidal
category C is a cartesian category, then Axiom (f-ρ) is equivalent
to Axiom (f-π).

Proof. The direction from (f-π) to (f-ρ) is trivial. For the converse,
Axiom (f-π) is gotten from (f-ρ) as the following:
A (A ×= C, B × C){{{{ (dinaturality)
first {{{{{{

A(A×C,B×!C )/ A (A × C, B × 1)
:
tt
tt
t
A(A×!C ,B×1) tt
tt
tt

first
/ A (A × 1, B × 1)
A(A×C,ρ)
t
CC
t
t
CC
tt
CC (f-ρ)A(ρ,B)
ttA(A×1,ρ) (functoriality)
CC
t
t
C!
ytt

/ A (A × C, B)
A (A × 1, B)

A (A, B)
C

A(A×!C ,B)

In the above, !C : C −→ 1 is the unique map from C to theterminal, hence ρ ◦ A×!C : A × C −→ A × 1 −→ A is equal
to the projection π1 : A × C −→ A. The upper path of the above
diagram is the left hand side of (f-π), and the lower path is the righthand side.

5.3 Arrows as Strong Monads in Prof
Now we show the main result.
Theorem 14 For a monoidal small category (C, ⊗, I, α, λ, ρ) anda monad (A, η, µ) on C in Prof , there is a bijective correspondence between first operators and strengths for (A, η, µ) in
Prof .

Proof. The following calculation of ends and coends shows thecorrespondence between strength (in LHS) and first (in RHS):()()
Nat (⊗∗ ) ◦ A × Id+
C , A ◦ (⊗∗ )
∼
=
∫
A,B,C

( by Lemma 3 )
[(
)(
(
)(
(
)
)
)]
⊗∗ ◦ A×Id+
C, (A, B) , A ◦ ⊗∗ C, (A, B)
C=

ist (arr f ) = arr ⟨f, id⟩
ist a >>> arr π1 = a()
ist a >>> b =()
ist a >>> ist arr π1 >>> b >>> arr (id×π2 )ist (ist a) = ist a >>> arr ⟨id, π2 ⟩( by Definition 7 - (4) )

′
′
)
) ((
∫ [ A∫,B( (
)((
) (
))
(
))
A′,B ′ , A,B,⊗∗ C, A′,B ′× A×Id+
C

A,B,C

) ]
∫C ′ () ( (())
A C, C ′ × ⊗∗ C ′ , A, B

( by the definitions of (−)∗ (6), tensor × (7), and Id+
C (5) )[∫ ′ ′
A ,B
(
)
(
)
(
)
C C, A′ ⊗B ′ ×A A′ , A ×C B ′ , B ,
A,B,C
]
∫ C′
(
( ′
)
′)
A C, C ×C C , A⊗B

=
∫

∼
=
∫

[∫

( by Lemma 5 on B ′ , C ′ )
]
A
(
)
(
)
C C, A′ ⊗B ×A A′ , A , A (C, A⊗B)
′

A,B,C

∼
=
∫
A,B,C,A′∼=∫( by Lemma 6, then Currying )[ () [ ( ′ )]]′C C, A ⊗B , A A , A , A (C, A⊗B)
( by Lemma 4 on C )A,B,A′[ ( ′ )()]
A A , A , A A′ ⊗B, A⊗B∼=( by Lemma 3 )
( (
)
( ′
))
′
NatA′ ,A DinatB A A , A , A A ⊗B, A⊗B
The remaining is to prove the equivalences between the axioms for strength and those for first: the four axioms for strengthwith α, ρ, η, and µ correspond respectively to (f-α), (f-ρ), (f-η),and (f-µ). The proofs of these equivalences are tedious but straightforward.
In this way we can characterize simply the notion of arrow
only with basic structures of the bicategory Prof . This simplicity
and rich structures of Prof make it easy to calculate, in Prof ,properties and structures on arrows, as in the paper [2]. Besides,
this characterization provides a better justification of the axioms ofarrows, and provides us clean understanding of the notion of arrow.
5.4

B ∈ C, dinatural in A ∈ C, and satisfying the following axioms:

On ist Operators

On a cartesian category as a base of an arrow, there is an alternative
to a first operator, i.e., an ist operator [15, 19].
Applying the theorem in the previous subsection to cartesiansmall categories, we see that strengths are equivalent to first
operators, hence also to ist operators. However, we give a direct
proof of correspondences between strengths in Prof and ist
operators. The proof shows how the notion of ist operator depends
on cartesian products.
Definition 15 (ist Operator) For a cartesian category C and amonad (A, η, µ) over C in Prof , an ist operator is a familyof morphisms istA,B : A (A, B) −→ A (A, B×A) natural in

Theorem 16 For a cartesian small category C, and a monad(A, η, µ) on C in Prof , there is a bijective correspondence between ist operators and strengths for (A, η, µ) in Prof .
Proof. Here we concentrate only on the correspondence between(di)natural transformations of ist operators (in RHS) and strengths(in LHS):()()
Nat (×∗ ) ◦ A × Id+
C , A ◦ (×∗ )∼= ( by Lemma 3 and definitions, as in the proof of Theorem 14 )[∫ ′ ′
∫
A ,B
(
)
(
)
(
)
C C, A′ ×B ′ ×A A′ , A ×C B ′ , B ,
A,B,C
]
∫ C′
(
)
(
)
A C, C ′ ×C C ′ , A×B∼=∫( by the adjointness of the cartesian product A′ ×B ′ )[∫ ′ ′A ,B (
)
(
)
(
)
(
)
C C, A′ ×C C, B ′ ×A A′ , A ×C B ′ , B ,
A,B,C
]
∫ C′
(
( ′
)
′)
A C, C ×C C , A×B∼=∫( by Lemma 5 on A′ , B ′ , C ′ )[]A (C, A) ×C (C, B) , A (C, A×B)

A,B,C

∼
=
∫

[

[

C (C, B) , A (C, A) , A (C, A×B)]]

( by Currying )

A,B,C

∼
=
∫

( by Lemma 4 on B )[A (C, A) , A (C, A×C)

]

A,C

∼
=

(

DinatA,C)
A (C, A) , A (C, A×C)

( by Lemma 3 )The steps are almost the same as in the proof of Theorem 14,
except that we used adjointness of cartesian products for the second
isomorphism.
6.

Generalizing Arrow

In this section, we generalize the definition of strong monad byenlarging a class of ambient bicategories in which internal strong
monad is defined. So far in the paper, such an ambient bicategory is
Cat or Prof . We see first which kind of bicategories can be used
for such purpose; then we define the notion of strength in there.
By this generalization we obtain some variants of the notionof arrow. Especially in the last, we give a definition of “selfenriched” version of arrow, which is shown to be equivalent to
Atkey’s definition of arrow.

6.1 Gray Monoid
Monads in Cat are defined over any category, while strong monads
in Cat are defined only over monoidal categories. Hence when
we define strong monads in bicategories, we first have to definemonoidal objects in bicategories.
Much like we need monoidal categories as ambient categories
in which we define monoid objects, we need monoidal bicategories [13] as ambient bicategories in which we define monoidal
objects. (These phenomena of occurrences of similar kinds of inner and outer structures are called “the microcosm principles”, advocated by Baez and Dolan [14].)
We can in fact use monoidal bicategories to define monoidal
objects. However, the structural isomorphisms of a monoidal
bicategory—up to which the composition of 1-cells and also themonoidal product are associative and unital—are cumbersome andmake the essence blurred. Therefore we here use the notion ofGray monoid, which is, roughly, “strictified monoidal bicategory”.
Definition 17 (Gray monoid) A Gray monoid P is a 2-category
with the following structures:• a 0-cell I,• for each 0-cell C in P, two 2-functors LC , RC : P −→ P

satisfying the following conditions

Example 18 Let V be a cocomplete SMCC. Then, there is a notionof V-profunctor, also called V-module [20].
For V-categories C and D, a V-profunctor F from C to D is a
V-functor F : D op  C −→ V, and for parallel V-profunctors F
and F ′ , a 2-cell between V-profunctors F and F ′ is a V-naturaltransformation from F to F ′ .
Then, as the monoidal bicategory Prof , we can define a
monoidal bicategory V-Prof of small V-categories, V-profunctors,
and 2-cells between V-profunctors. The monoidal product in
V-Prof is the same as the tensor product in V-Cat, which wedenote by . In the case that V = Set, Set-Prof is Prof .
This V-Prof plays an important role in Section 6.3.
6.2

Monoidal Object and Strong MonadFirst we recall the notion of monoidal object in a Gray monoid [11].
Definition 19 (Monoidal Object) Let (P, , I) be a Gray monoid.
A monoidal object (or pseudomonoid) in (P, , I) is a 0-cell
C in P together with 1-cells ⊗ : C  C −→ C and I : I −→ C
in P and invertible 2-cells α, λ, and ρ below such that they satisfy
coherence axioms quite similar to those for monoidal categories.
(See [11], for further detail.)def

LCD = LC LD ,RCD = RD RC ,RD LC = LC RD ,

C⊗

⊗C

for all 0-cells C, D, and

C2

C @@

⊗

α



• for each 1-cells F : C −→ C′ , G : D −→ D′ , an invertible

IC/ C2 o CI C
~~
@@@@
ρ ~
@@@@ λ~~~~~~~@@@@ ⊗@@@@ ~~~~~~
 ~~

/ C2

/C

⊗

⇐

C3

LI = RI = IdP ,⇐(and define C  D = LC (D)),⇐

LC (D) = RD (C)C

2-cellIn what follows, we denote LC by C(−) and RC by (−)C.
Note that for 1-cells F : C −→ C′ and G : D −→ D′ ,CG; F D′ and F D; C′ G are not necessarily the same, so wecannot denote them simply by F G. However they are isomorphic
with the iso-2-cell cF ,G , and we can always interchange them.
In the definition of Gray-monoid, all structural isomorphismsof monoidal bicategory are replaced with identities, except for c.
Even associativity and unitality—both of the composition of 1cells and of monoidal product—are strict. By this simplicity, we
can keep definitions of monoidal object and strength accessible.
All Gray monoids form monoidal bicategories, and conversely
by the strictification theorem [13], all monoidal bicategories are
monoidally equivalent to some Gray monoids. (It is not truethat all monoidal bicategories are monoidally equivalent to somemonoidal 2-categories [13].) Hence we identify monoidal bicategory with Gray monoid.
The 2-category Cat forms a monoidal 2-category with cartesian products. The bicategory Prof forms a monoidal bicategory
with the tensor product ×, as the category Rel forms a monoidal
category with the tensor product ×.
We can generalize Prof with enriched category theory:

Definition 20 (Strong Monad in Gray-Monoid) Let (P, , I)
be a Gray-monoid, (C, ⊗, I, α, λ, ρ) be a monoidal object in(P, , I), and (A, η, µ) be a monad over C in P.
A strength for the monad A in (P, , I) is a 2-cell str
in P in the following diagram such that it satisfies the axioms (s-α), (s-ρ), (s-η), and (s-µ) below.
C2
⊗

AC

/ C2
⊗

str



C

/ C3 C⊗ / C2x;
FF
FF c xxxx
x AC
C⊗ #
AC2

C3 FF

C2

⊗C



α–1 ⊗

C

2

⊗


/C

A

C3


/C

str
A

AC2

/ C3 C⊗ / C2


strC

⊗C
α–1

⇐

satisfying certain coherence axioms such as cIdC ,IdD = idCD ,see [11] for details.
⊗ (s-α); C FF
ACxx
F⊗Fx
x str FF
 xx
#/ 
/
2

⊗

= ⊗C


/C

C

2

⇐


/ C′  D′⇐

LC′ (G)⇐C′  DRD′ (F )Monoidal objects in Cat are monoidal categories.
Monoidal objects in Prof are called promonoidal categories [9,10]. In Section 5.1, we considered only the promonoidal categories
induced from monoidal categories via the direct image embedding.
(The direct image embedding is monoidal pseudofunctor, hence
maps monoidal objects in Cat to those in Prof .)Now we define strong monads in Gray-monoids:

⇐

cF ,G
⇒

RD (F )

/ C  D′⇐

LC (G)

⇐

CD

⊗

C

A

C

CI
/ 2 AC / C2
EEEE ρC
EEEE ⊗ str ⊗
E 

/C
C

/ C2 AC / C2
EE c–1 CIwww; ⊗EE ww ρ
A

" w
CI

C EE

⇐

⇐

=

⇐

⇐

C EEE

C

A

x; C EE
xx str E⊗EE
x
= C2
E"
xxAC
/
/
2
C
C
C

⊗

/ C2 AC / C2

AC

(s-ρ)

C



C

2

⊗

(s-η)

⇐

⊗
str
A

A

We show that the above definition gives a generalization of
Atkey’s definition of arrow, from that over a cartesian category tothat over a monoidal category.
In the definition below, we use the coKleisli category of thecomonad D × (−) for each object D in a cartesian category C.
Note that if a base category is cartesian, so is its coKleisli category.
Definition 22 [3] An arrow on a cartesian category C consistsof a mapping of objects Ar : |C| × |C| −→ |C| and threetransformations all natural in D,/ C2 AC / C2
A
µC

str

⊗ = ⊗ AC
w; C HHHHA
A ww
H
w
HH 

µ
 www
#/
C
C
C

⊗

/C

⇐

str

η

A

A

⇐

AC

⇐

C2

/C

⇐

⇐

⊗

⇐

⇐

2

ηC

to J) is a strong monad over V in V′ -Prof whose underlying V′ endoprofunctor is V-small.


(s-µ)


/C

We call a monad in P equipped with a strength in (P, , I) a
strong monad in (P, , I).

By this definition with P = Prof , we can in fact define arrows
not only over monoidal categories as in Section 5 but also overany promonoidal categories; on the other hand, we have no similar
theorem to Theorem 14, because first-operators are defined only
for monoidal categories.
6.3 Self-enrichment of Arrow
In the last place, we consider a solution for the following problem
pointed out in the paper [3]: For a CCC C, let us identify types andterms in Haskell with objects and morphisms in C, respectively. An
arrow A in Haskell is a type constructor, hence maps two types toa type; i.e., A is not a functor C op × C −→ Set but a functor
C op × C −→ C.
In order to replace Set with C, a naive way is to consider strong
monads in C-Prof in Example 18. However then C is required tobe small cocomplete and small at the same time, which implies that
C must be a preorder. The use of the synthetic domain theory, which
admits non-trivial internal small cocomplete categories, is not natural just for this purpose; for it unnecessarily restricts models.
The solution that we give for this is use of cocompletion and to
distinguish “small” ones from “large” ones.
Now let V be an SMC, V′ be a sufficiently cocomplete SMCC,
and J : V −→ V′ be a symmetric strong monoidal fully faithful functor, whose leading example is the Yoneda embeddingb Then V can be a V′ -category with hom-objects
y : V −→ V.
defhomV (A, B) = JA(V′ JB. The underlying category of this′V -category V is isomorphic to the category V itself; also J canbe V′ -functor whose underlying functor is again J.
For a V′ -profunctor F : C −→+ D, we call F V-small if the′
V -functor F : D op  C −→ V′ is factorized along the V′ -functor
J : V −→ V′ :
F
/ V′
O
QQQ
QQQ
Q
J
QQQ
F◦
QQQ
(

D op  CQ

V′

Such factors of F are unique up to natural V -isomorphism, and wedenote the V′ -functor from D op  C to V by F ◦ . (Note that when
J is the Yoneda embedding, which is injective, F ◦ is uniquelydetermined.)
Definition 21 For an SMC V and an embedding J : V −→ V′
as above, a small strong monad over V in V′ -Prof (with respectarrDAB : C (D × A, B) −→ C (D, Ar (A, B))>>>DABC : C (D, Ar (A, B)) × C (D, Ar (B, C))−→ C (D, Ar (A, C))
firstDABC : C (D, Ar (A, B)) −→ C (D, Ar (A × C, B × C))
These transformations must satisfy the eight laws (assoc) – (f-µ) in
Section 2 where the equations are interpreted as equations between
C morphisms generated by the above transformations. In thoseequations, we use variables f, g for morphisms in C (D × A, B)
and a, b, c for morphisms in C (D, Ar (A, B)); and the composition ◦, identity id, product × and projection π1 are all those in the
coKleisli category noted above.

Theorem 23 For a cartesian category C, the notion of arrow overC defined in Definition 22 is equivalent to that of small strongbmonad over C in C-Prof
with respect to the Yoneda embeddingby : C −→ C.
Proof. Basically, this proof is almost the same as Proof 10 and 14.
Since a small strong monad A is decomposed as y ◦ A◦ bydefinition, it is obvious that this corresponds to Ar of an arrow ofDefinition 22:
A◦ (A, B) = Ar (A, B)
def

(8)

b
The unit η of a small strong monad A over C is a natural Cbtransformation from the identity C-profunctor
Id+
to
A,
i.e.,
a
C
family of morphisms()
ηA,B : yA→Cb yB −→ y (A◦ (A, B))b natural in A, B ∈ C. Here the presheaf yA→b yB is isoin CCmorphic to the presheaf C (− × A, B), by Yoneda lemma. On◦
the other hand, by the correspondence (8), y (A (A, B)) =C (−, Ar (A, B)). As this, η corresponds to arr.
A correspondence between µ and >>> is readily obtained as in
Proof 10.
Finally, we can easily prove that str corresponds to first,
with the full-faithfulness of y, and as in Proof 14, where we useb
C-enrichedversion of Lemma 3, 4, 5, and 6 (see [20, Sec. 3.10]).
b we can also
Example 24 Besides Yoneda embeddings C −→ C,
use the inclusion Set ,→ Ens, the codomain of which is thecategory of classes. Then we have the notion of small strong monadover Set in Ens-Prof : A : Set op × Set −→ Set.
In the paper [2], such notion is used, to obtain some endofunctors
over Set—rather than functors from Set to Ens—for which we
can consider coalgebras.
Acknowledgments
I would like to thank Ichiro Hasuo for encouraging me to write
the paper, helpful comments for early draft, and discussions, andalso thank Paul-André Melliès for teaching me profunctors, andhigher dimensional category theory. Also I am grateful to Shin-ya
Katsumata, Bart Jacobs, Pastro Craig, and Naohiko Hoshino for
useful comments and discussions.
This work is supported by the GCOE Program, JSPS; and also
by the PRESTO Research Promotion Program, JST (principal investigator: Ichiro Hasuo).

References[1] T. Altenkirch, J. Chapman, and T. Uustalu. Monads need not be
endofunctors. In C.-H. L. Ong, editor, FOSSACS, volume 6014 of
Lecture Notes in Computer Science, pages 297–311. Springer, 2010.
ISBN 978-3-642-12031-2.
[2] K. Asada and I. Hasuo. Categorifying computations into components
via arrows as profunctors. To appear in Proc. International Workshop
on Coalgebraic Methods in Computer Science (CMCS 2010)., 2010.
[3] R. Atkey. What is a categorical model of arrows? Electr. Notes Theor.
Comput. Sci, To appear.

[19] B. Jacobs, C. Heunen, and I. Hasuo. Categorical semantics for arrows.
Journal of Functional Programming, 19(3-4):403–438, 2009. ISSN
0956-7968.
[20] G. M. Kelly. Basic Concepts of Enriched Category Theory. Number 64
in LMS. Cambridge Univ. Press, 1982.
[21] P. B. Levy. Call-By-Push-Value: A Functional/Imperative Synthesis,
volume 2 of Semantics Structures in Computation. Springer, 2004.
ISBN 1-4020-1730-8.
[22] P. B. Levy, A. J. Power, and H. Thielecke. Modelling environments incall-by-value programming languages. Inf. & Comp., 185(2):182–210,
2003. ISSN 0890-5401.
[23] E. Moggi. Computational lambda-calculus and monads. In LICS,
pages 14–23. IEEE Computer Society, 1989.
[24] E. Moggi. Notions of computation and monads. Information andComputation, 93(1):55–92, 1991.
[25] M. Nygaard and G. Winskel. Domain theory for concurrency. Theor.
Comput. Sci., 316(1):153–190, 2004.

[26] J. Power and E. Robinson. Premonoidal categories and notions ofcomputation. Math. Struct. in Comp. Sci., 7(5):453–468, 1997.
[4] J. Bénabou. Distributors at work. Lecture notes by Thomas Streicher,2000.
[27] R. Street. The formal theory of monads. Journal of Pure and Applied
www.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.gz.
Algebra, 2:149–168, 1972.
[5] N. Benton, J. Hughes, and E. Moggi. Monads and effects. In
G. Barthe, P. Dybjer, L. Pinto, and J. Saraiva, editors, Advanced Lectures from Int. Summer School on Applied Semantics, APPSEM 2000
(Caminha, Portugal, 9–15 Sept. 2000), volume 2395 of Lecture Notes
in Computer Science, pages 42–122. Springer-Verlag, Berlin, 2002.
[6] F. Borceux. Handbook of Categorical Algebra 1: Basic Category Theory, volume 50 of Encyclopedia of Mathematics and Its Applications.
Cambridge University Press, Cambridge, 1994.
[7] G. Cattani, M. Fiore, and G. Winskel. A theory of recursive domains
with applications to concurrency. In Proc. of LICS ’98, 0:214–225,
1998. ISSN 1043-6871.

[8] P.-L. Curien. Operads, clones, and distributive laws. preprint,
www.pps.jussieu.fr/~curien, 2008.
[9] B. Day. On closed categories of functors. In Reports of the Midwest
Category Seminar, IV, Lecture Notes in Mathematics, Vol. 137, pages
1–38. Springer, Berlin, 1970.
[10] B. Day. On closed categories of functors. II. In Category Seminar (Proc. Sem., Sydney, 1972/1973), pages 20–54. Lecture Notes in
Math., Vol. 420. Springer, Berlin, 1974.
[11] B. Day and R. Street. Monoidal bicategories and Hopf algebroids.
Adv. Math., 129(1):99–157, 1997. ISSN 0001-8708.
[12] M. Fiore, N. Gambino, M. Hyland, and G. Winskel. The cartesianclosed bicategory of generalised species of structures. Journ. of London Math. Soc., 77:203–220, 2008.
[13] R. Gordon, A. J. Power, and R. Street. Coherence for tricategories.
Mem. Amer. Math. Soc., 117(558):vi+81, 1995. ISSN 0065-9266.
[14] I. Hasuo, B. Jacobs, and A. Sokolova. The microcosm principle
and concurrency in coalgebra. In Foundations of Software Science
and Computation Structures, volume 4962 of Lect. Notes Comp. Sci.,
pages 246–260. Springer-Verlag, 2008.
[15] C. Heunen and B. Jacobs. Arrows, like monads, are monoids.
Electr. Notes Theor. Comput. Sci, 158:219–236, 2006.
URL
http://dx.doi.org/10.1016/j.entcs.2006.04.012.
[16] T. T. Hildebrandt, P. Panangaden, and G. Winskel. A relational modelof non-deterministic dataflow. In D. Sangiorgi and R. de Simone, editors, CONCUR, volume 1466 of Lecture Notes in Computer Science,
pages 613–628. Springer, 1998. ISBN 3-540-64896-8.
[17] J. Hughes. Generalising monads to arrows. Sci. Comput. Program.,37(1-3):67–111, 2000.
[18] J. Hughes. Programming with arrows. In V. Vene and T. Uustalu,
editors, Advanced Functional Programming, volume 3622 of Lecture
Notes in Computer Science, pages 73–129. Springer, 2004. ISBN 3540-28540-7.

[28] T. Uustalu. Strong relative monads. Short contribution in International
Workshop on Coalgebraic Methods in Computer Science (CMCS2010)., 2010.
[29] P. Wadler. Monads for functional programming. In Lecture Notes
In Computer Science, Vol. 925; Advanced Functional Programming,
First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, pages 24–52, London, UK, 1995.
Springer-Verlag. ISBN 3-540-59451-5.