2-natural transformation?
symmetric monoidal (∞,1)-category of spectra
Given a monad on some category , the Kleisli category of has as objects the objects of , but a morphism in the Kleisli category is a morphism in . The monad structure induces a natural composition of such ”-shifted” morphisms.
Equivalently, the Kleisli category is the full subcategory of the Eilenberg–Moore category of on the free T-algebras (the free modules).
Let be a monad in Cat, where is an endofunctor with multiplication and unit .
A free -algebra over a monad (or free -module) is a -algebra (module) of the form , where the action is the component of multiplication transformation .
The Kleisli category of the monad the subcategory of the Eilenberg–Moore category on the free -algebras.
If is the forgetful functor and is the free algebra functor , then the Kleisli category is simply the full subcategory of containing those objects in the image of .
As another way of looking at this, we can keep the same objects as in but redefine the morphisms. This was the original Kleisli construction:
The Kleisli category has as objects the objects of , and as morphisms the elements of the hom-set , in other words morphisms of the form in , called Kleisli morphisms.
Composition is given by the Kleisli composition rule (as in the Grothendieck construction (here ).
More explicitly, this means that the Kleisli-composite of with is the morphism
This Kleisli composition plays an important role in computer science; for this, see the article at monad (in computer science).
In more general 2-categories the universal properties of Kleisli objects are dual to the universal properties of Eilenberg–Moore objects?.
In typed functional programming Kleisli composition is used to model functions with side-effects and computation. See at monad (in computer science) for more on this.
Discussion of cases where the inclusion of the Kleisli category into the Eilenberg-Moore category is a reflective subcategory is in
Discussion in internal category theory is in
Discussion of Kleisli categories in type theory is in