Natural Transformations as Rewrite Rules and Monad Composition

Eklund et al. (2002) present a graphical technique aimed at simplifying theverification of various category-theoretic constructions, notably thecomposition of monads. In this note we take a different approach involvingstring rewriting. We show that a given tuple $(T,\mu,\eta)$ is a monad if andonly if $T$ is a terminal object in a certain category of strings and rewriterules, and that this fact can be established by proving confluence of therewrite system. We illustrate the technique on the monad composition problem.We also give a characterization of adjunctions in terms of rewrite categories