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 and , and a functor

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

## Eilenberg-Moore Laws

Can we construct a functor 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:

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

Where we must determine a suitable . Applying to as an obvious first step yields:

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

we could form a composite of the right type:

To do this uniformly for all Eilenberg-Moore algebras, we require be natural in . The action of on objects is then:

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

**Unit axiom**: .**Multiplication axiom**: .

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

- Eilenberg-Moore liftings of
- Eilenberg-Moore laws .

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 to a functor . 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:

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

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

for some natural transformation . Of course, we need to verify that this mapping is functorial. In doing so, we find the need for the following axioms:

**Unit axiom**: .**Multiplication axiom**: .

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

- Kleisli liftings of .
- Kleisli laws .

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.

## 5 thoughts on “Monads, Laws and Liftings”