Contents

Contents

Idea

A generalization of the concept of monad (in computer science). In particular, it generalizes the attitude that monads in computer science are useful insofar as they generate a Kleisli category. Thus an arrow abstracts the hom-profunctor of $\mathrm{Kl}(T)$ for a strong monad $T: \mathbf C \to \mathbf C$ as an endoprofunctor on $\mathbf C$.

Therefore, an arrow $A : \mathbf C^{op} \times \mathbf C \to \mathbf{Set}$ can be thought as a putative replacement of $\mathrm{Hom}_{\mathbf C} : \mathbf C^{op} \times \mathbf C \to \mathbf{Set}$. In fact an arrow comes equipped with a transformation $\mathrm{arr} : \mathrm{Hom}_{\mathbf C} \Rightarrow A$ that lift morphisms of $\mathbf C$ to the ‘augmented’ morphisms given by $A$, and with a transformation $\ggg : A \circ A \Rightarrow A$ that behaves like a composition operation. Then one requires that $\ggg$ is associative and that $\mathrm{arr}(1_a)$ is the unit of this operation.

These data makes $A$ a promonad? on $\mathbf C$, i.e. a monad on $\mathbf C$ in the bicategory of profunctors. Since every monad on $\mathbf{Set}$ (or on any reasonable enriching base where programmers work) is strong, arrows traditionally generalize the hom-profunctor of strong monads. The additional requirement that $A$ is a strong profunctor (and the laws it is required to satisfy) imply that an arrow is a strong monad in the bicategory of profunctors (Asada10).

Definition

Definition

An arrow $A$ on a monoidal category $\mathbf C$ is a monoid in the category of strong endoprofunctors on $\mathbf C$, i.e. it’s a functor $\mathbf C^{op} \times \mathbf C \to \mathbf{Set}$ equipped with the following structure:

1. A natural family of morphisms $\mathrm{arr} : \mathbf C(a,b) \to A(a,b)$ (the unit of the monoid),
2. A natural family of morphisms called composition $\ggg : A(a,b) \times A(b,c) \to A(a,c)$ (the multiplication of the monoid), which satisfy an associative law and for which $\mathrm{arr}_{a,a}(1_a)$ is the unit,
3. A family of morphisms called strength $s_{a,b,m} : A(a,b) \to A(m \otimes a, m \otimes b)$, which is dinatural in $m$ and natural in $a, b$, and satisfies coherence laws that make $(A, s)$ a strong profunctor.

References

Arrows originate in Section 2 of

The ‘justification’ of arrows as strong monads in $\mathbf{Prof}$ is given in