Now we have seen both the Kleisli and Eilenberg-Moore categories, it is interesting to consider how we might construct “nice” functors between them. To do so, we fix a pair of monads $\mathbb{S} : \mathcal{C} \rightarrow \mathcal{C}$ and $\mathbb{T} : \mathcal{D} \rightarrow \mathcal{D}$, and a functor

$H : \mathcal{C} \rightarrow \mathcal{D}$

We shall then consider the Eilenberg-Moore and Kleisli constructions separately.

Eilenberg-Moore Laws

Can we construct a functor $\overline{H} : \mathcal{C}^{\mathbb{S}} \rightarrow \mathcal{D}^{\mathbb{T}}$ in some natural way? This question gives us a bit too much freedom to narrow things down, so we restrict attention to functors that interact well with the forgetful functors, in that:

$U^{\mathbb{T}} \circ \overline{H} = H \circ U^{\mathbb{S}}$

We shall call such a functor an Eilenberg-Moore lifting of $H$. The condition above means

$\overline{H}(A, \mathbb{S}(A) \xrightarrow{\alpha} A) = (H(A), \mathbb{T}(H(A)) \xrightarrow{\alpha'} H(A)) \qquad \overline{H}(h) = H(h)$

Where we must determine a suitable $\alpha'$. Applying $H$ to $\alpha$ as an obvious first step yields:

$H(\mathbb{S}(A)) \xrightarrow{H(\alpha)} H(A)$

The domain is of the wrong type. If we had a morphism

$\lambda : \mathbb{T}(H(A)) \rightarrow H(\mathbb{S}(A))$

we could form a composite of the right type:

$\mathbb{T}(H(A)) \xrightarrow{\lambda} H(\mathbb{S}(A)) \xrightarrow{H(\alpha)} H(A)$

To do this uniformly for all Eilenberg-Moore algebras, we require $\lambda$ be natural in $A$. The action of $\overline{H}$ on objects is then:

$(A,\alpha) \mapsto (H(A), H(\alpha) \circ \lambda_A)$

If we attempt to establish the resulting structure map satisfies the unit and multiplication axioms, we find that $\lambda$ must interact well with the monad structures, in that the following two axioms hold:

1. Unit axiom: $H(\eta^{\mathbb{S}}) = \lambda \circ \eta^{\mathbb{T}}_H$.
2. Multiplication axiom: $\lambda \circ \mu^{\mathbb{T}}_H = H(\mu^{S}) \circ \lambda_H \circ H(\lambda)$.

Such a $\lambda$ satisfying these axioms is referred to as an Eilenberg-Moore law. In fact, there is a bijective correspondence between:

1. Eilenberg-Moore liftings of $H$
2. Eilenberg-Moore laws $\mathbb{T} \circ H \Rightarrow H \circ \mathbb{S}$.

Verifying this is a bit fiddly, but routine once you figure out how to construct the components of an Eilenberg-Moore law from a lifting. We shall skip the details.

Kleisli Laws

We now consider how to lift $H$ to a functor $\underline{H} : \mathcal{C}_{\mathbb{S}} \rightarrow \mathcal{D}_{\mathbb{T}}$. Again, we need to constrain the problem further. In this case it turns out to be best to consider functors that interact well with the free constructions, in that:

$\underline{H} \circ F^{\mathbb{S}} = F^{\mathbb{T}} \circ H$

We shall call such a functor a Kleisli lifting of $H$. The condition above forces that:

$\underline{H}(A) = A \qquad \underline{H}(f : A \xrightarrow{f} \mathbb{S}(B)) = H(A) \xrightarrow{f'} \mathbb{T}(H(A))$

Where it remains to determine a suitable $f'$. Having seen the drill for the Eilenberg-Moore construction, an intuitive plan is to form a composite:

$H(A) \xrightarrow{H(f)} H(\mathbb{S}(A)) \xrightarrow{\lambda_A} \mathbb{T}(H(B))$

for some natural transformation $\lambda : H \circ \mathbb{S} \Rightarrow \mathbb{T} \circ H$. Of course, we need to verify that this mapping is functorial. In doing so, we find the need for the following axioms:

1. Unit axiom: $\eta^{\mathbb{T}}_H = H(\eta^{\mathbb{S}})$.
2. Multiplication axiom: $\lambda \circ H(\mu^{\mathbb{S}}) = \mu^{\mathbb{T}} \circ H(\lambda) \circ \lambda_H$.

Such a $\lambda$ is referred to as a Kleisli law. As we might expect from the previous construction, there is a bijection between:

1. Kleisli liftings of $H$.
2. Kleisli laws $H \circ \mathbb{S} \Rightarrow \mathbb{T} \circ H$.

Again, the proof requires a little bit of creativity to construct the components of a Kleisli law from a given lifting, and makes an instructive exercise.

There is also rather pleasing duality between the two results.