On the tensor product of monads (an exercise in coend calculus)

back · · category-theory

Recently, Andrey Mokhov made the observation that a monad is a monoid (in the category of endofunctors) with the following tensor product:

data (:*:) f g a where
    (:*:) :: f x -> (x -> g a) -> (:*:) f g a

I was a bit surprised because I knew that a monad is a monoid with the tensor product given by functor composition. At first I didn't exactly see how to show the equivalence of the two tensors, but Bartosz's lecture on coends provided the necessary tools to show the correspondence.

The main assumptions of the following proof are that (i) we work in the category of sets and functions, \(\mathrm{Set}\), and (ii) \(F\) and \(G\) are endofunctors. The given data type is modeled in category theory by a coend of the profunctor \(\mathrm{Set}(-, G a) \times F -\):

$$(F \star G) a = \int^x \mathrm{Set}(x, G a) \times F x$$

We now show by indirect proof that \(F \star G = F \circ G\); that is, for any object \(s\) we have:

$$ \begin{align*} & \mathrm{Set}\left((F \star G) a, s \right) \\ & \cong \; \text{\{ definition of tensor product \}} \\ & \mathrm{Set}\left(\int^x \mathrm{Set}(x, G a) \times F x, s \right) \\ & \cong \; \text{\{ universal property of coends \}} \\ & \int_x \mathrm{Set}\left(\int^x \mathrm{Set}(x, G a) \times F x, s \right) \\ & \cong \; \text{\{ currying \}} \\ & \int_x \mathrm{Set}\left(\mathrm{Set}(x, G a), \mathrm{Set}(F x, s) \right) \\ & \cong \; \text{\{ contra-variant Yoneda \}} \\ & \int_x \mathrm{Set}\left(F (G a), s\right) \\ & \cong \; \text{\{ defintion of composition \}} \\ & \int_x \mathrm{Set}\left((F \circ G) a, s\right) \end{align*} $$

Further reading: