For evil reasons of my own, I'm trying to give a presentation of a monad in primitive terms, assuming only the notion of a category. More honestly, I looked at this post and got intrigued by the notion that, in some sense, a monad is a monad simply because its Kleisli category is a category, and went on to check to what extent that is true.
I started out with this: let $\mathcal{C}$ be a category, $T:\mathrm{Ob}(\mathcal{C})\to\mathrm{Ob}(\mathcal{C})$ an object assignment, and $\mathcal{K}$ another category (with identity and composition denoted as $\eta$ and $\rhd$, respectively), such that:
- $\mathrm{Ob}(\mathcal{K})=\mathrm{Ob}(\mathcal{C})$
- $\mathcal{K}(A,B)=\mathcal{C}(A,TB)$
I then tried to derive the Kleisli triple $(T, \eta, \mu)$ (with $Tf = (\eta\circ f)\rhd \mathrm{id}$ and $\mu=\mathrm{id}\rhd\mathrm{id}$), but got quickly stumped when trying to show that $T$ is a functor. My assumptions, it seems, give no relation whatsoever between the compositions in both categories. After some trial and error, I found that adding this assumption:
- For every $f:C\to TD$, $g:B\to TC$, and $h:A\to B$ (in $\mathcal{C}$): $(f\rhd g)\circ h = f\rhd(g\circ h)$
yielded back all the monad goodness. I also checked that this property holds for the Kleisli category of every monad, so I'm not adding any extraneous restrictions here.
My question is, does this property have a name? Additionally: is it of any interest whatsoever? is it somehow trivial (for some reason I missed)?
PS: I know this is very close to the Kleisli triple construction (as in this question) which also doesn't depend in any notion beyond a category; for some reason this one feels more symmetrical to me.
This property is called "Triple Product Law" in E. Manes, Algebraic Theories, Springer-Verlag, 1976, page 26, 3.8.
It is trivial that this property holds in any Kleisli category: we have $(f \rhd g) \circ h = (f \rhd g) \rhd (\eta_B \circ h) = f \rhd (g \rhd (\eta_B \circ h)) = f \rhd (g \circ h)$.
It is also trivially wrong that this property does not hold if there is no assumption relating the respective compositions : without any assumption, you cannot deduce any property. For instance, $\mathcal{C}$ has exactly one object $*$ and exactly four morphisms ($id_{*}$, b, c, $\eta_\ast$), and, for any morphism $k$, $k \rhd k = \eta_\ast$; moreover $c \circ b = \eta_\ast$, $\eta_\ast \circ b = id_\ast$ and $c \circ c = id_\ast$. I take $f = g = c$ and $h = b$.