Does a Kleisli triple need naturality conditions?

757 Views Asked by At

I'm reading a paper by Eugenio Moggi entitled "Notions of Computation and Monads". It introduces the concept of a “Kleisli triple” on a category $\mathcal C$, which is $(T, \eta, -^*)$, where:

  • $T$ is an object map on $\mathcal C$,
  • $\eta_A : A \to TA$,
  • For $f : A \to TB$, $f^* : TA \to TB$;

satisfying laws:

  • $\eta_A^* = 1_{TA}$
  • $f^* \circ \eta_A = f$
  • $f^* \circ g^* = (f^* \circ g)^*$

It then goes on to claim that these definitions give a monad. However, there doesn't seem to be anything requiring even $\eta$ to be a natural transformation, let alone the $\mu$ that you can define from the triple. Furthermore, when I searched around for more on Kleisli triples, this seems to be a common theme – no-one is concerned with naturality.

Are the naturality conditions all just implicit? Are they too obvious to write down? Or are they truly unnecessary?

3

There are 3 best solutions below

3
On BEST ANSWER

Here's another approach: (I write composition from left to right.)

Consider first the subcategory $\tilde{\mathcal C}\subseteq \mathcal C$ with objects $TA$ for all $A$ and with all arrows of the form $f^*$ (for $f:A\to TB$).

Then, consider the category $\mathcal T$ which consist of the disjoint union of $\mathcal C$ and $\tilde{\mathcal C}$, plus arrows from the left to the right, $A\dashrightarrow TX$ as original arrows of $\mathcal C$. All compositions are coming from $\mathcal C$. (It is (the collage of) a profunctor $\mathcal C\not\to\tilde{\mathcal C}$.)

If $T$ was also given on the arrows, then, for any $f:A\to B$ we should have a commutative diagram (also to ensure naturality of $\eta$) $$\matrix{A &\overset{\eta_A}\longrightarrow &TA \\ \!\!\!f\downarrow &&\ \,\ \downarrow Tf \\ B &\underset{\eta_B}\longrightarrow &TB } $$

The main thing is that $\eta_A$ will be a reflection of $A$ to $TA$ on the right side (that's why we had to take the subcategory $\tilde{\mathcal C}$), in particular will be epimorphism. Now, the above diagram can define $Tf$ as $$Tf:=(f\eta_B)^* $$ The universal property (i.e. reflections) guarantee that it will be indeed a functor. All the other details can be seen similarly. Note that for $h:A\to TB$, the $\eta_A h^*=h$ is heavily used.

For naturality of $\mu\ $ (defined as $\mu_A:=(1_{TA})^*:TTA\to TA$), you can apply that $\eta_A$ is epimorphic (in $\mathcal T$, that is, w.r.t. $\tilde{\mathcal C}$), and so $$ \matrix{A &\overset{\alpha}\longrightarrow &TX \\ \!\!\!f\downarrow &\scriptstyle\#&\ \,\ \downarrow h^* \\ B &\underset{\beta}\longrightarrow &TY } \ \implies \quad \matrix{TA &\overset{\alpha^*}\longrightarrow &TX \\ \!\!\!\!\!Tf\downarrow &\scriptstyle\#&\ \,\ \downarrow h^* \\ TB &\underset{\beta^*}\longrightarrow &TY } $$ Now apply this to $X=A,\ Y=B,\ u:A\to B,\ h^*=Tu=f,$ and $\alpha=1_{TA},\ \beta=1_{TB}$.

0
On

I must eat my words, it seems – although the first couple of articles I read ignored naturality, I've come across a set of notes that cover it.

The key is the observation that naturality conditions are defined in terms of the action of $T$ on morphisms, which is defined in terms of the other components of the triple as $Tf = (\eta_A \circ f)^*$. It's that which makes everything work out, although I think it's a bit of an omission of Moggi's not to at least acknowledge it.

As an example, here's the naturality of $\eta$: \[Tf\circ \eta_A = (\eta_B \circ f)^* \circ \eta_A = \eta_B \circ f\]

0
On

As you point out, a monad can be formed from a Kleisli triple where the naturality of $\eta$ and $\mu$ of the monad follow from the Kleisli laws and the identity $T f = (\eta_A \circ f)^\ast$, and also $\mu = \mathrm{id}_A^\ast$. We could equivalently view $(-)^\ast$ as a natural transformation $(-)^\ast_{A,B} \colon \mathcal{C}(A, T B) \rightarrow \mathcal{C}(T A, T B)$, where (for all $f \colon X \rightarrow A$, $g \colon B \rightarrow Y$): $$ \require{AMScd} \begin{CD} \mathcal{C}(A, T B) @>{\ast_{A,B}}>> \mathcal{C}(T A, T B) \\ @V{\mathcal{C}(f, T g)}VV @VV{\mathcal{C}(T f, T g)}V \\ \mathcal{C}(X, T Y) @>>{\ast_{X,Y}}> \mathcal{C}(T X, T Y) \end{CD} $$ That is, if $h \colon A \rightarrow T B$, then $T g \circ h^\ast \circ T f = (T g \circ h \circ f)^\ast$. This again follows from the Kleisli laws and the definition of the morphism mapping $T f = (\eta_A \circ f)^\ast$.