The Kleisli category is an interesting construction, but as with the Eilenberg-Moore category, it has a deeper significance.
For a monad on category , there is a functor with:
There is also a functor with:
(Verifying that both these are legitimate functors is a useful exercise in applying the various axioms.)
In fact, . To see this, we must show a natural bijection between:
- Kleisli morphisms .
- -morphisms .
Recalling that Kleisli morphisms are -morphisms , and expanding definitions:
- A Kleisli morphism is a -morphism .
- A -morphism is a -morphism .
So the bijection holds trivially. I think we can probably guess what the monad induced by this adjunction is going to turn out to be, but lets check the details anyway.
- Endofunctor: The endofunctor is . On objects this is . On morphisms .
- Unit: The unit is the transpose of , which is .
- Multiplication: The multiplication at is , where is the transpose of . Expanding definitions slightly, is . Then is , which is simply .
Summing up, for a monad , the the monad induced by the Kleisli adjunction is itself.
We have now seen two different constructions, the Eilenberg-Moore and Kleisli constructions, and their corresponding adjunctions. Both adjunctions yield the original monad. The natural question we shall pursue next is the relationship between these two constructions and other adjunctions that induce the same monad.