Kleisli category

In category theory, a Kleisli category is a category naturally associated to any monad "T". It is equivalent to the category of free "T"-algebras. The Kleisli category is one of two extremal solutions to the question "Does every monad arise from an adjunction?" The other extremal solution is the Eilenberg–Moore category. Kleisli categories are named for the mathematician Heinrich Kleisli.
Formal definition.
Let 〈"T", "η", "μ"〉 be a monad over a category "C". The Kleisli category of "C" is the category "C""T" whose objects and morphisms are given by
That is, every morphism "f: X → T Y" in "C" (with codomain "TY") can also be regarded as a morphism in "C""T" (but with codomain "Y"). Composition of morphisms in "C""T" is given by
where "f: X → T Y" and "g: Y → T Z". The identity morphism is given by the monad unit "η":
An alternative way of writing this, which clarifies the category in which each object lives, is used by Mac Lane. We use very slightly different notation for this presentation. Given the same monad and category formula_4 as above, we associate with each object formula_5 in formula_4 a new object formula_7, and for each morphism formula_8 in formula_4 a morphism formula_10. Together, these objects and morphisms form our category formula_11, where we define
Then the identity morphism in formula_11 is
Extension operators and Kleisli triples.
Composition of Kleisli arrows can be expressed succinctly by means of the "extension operator" (–)* : Hom("X", "TY") → Hom("TX", "TY"). Given a monad 〈"T", "η", "μ"〉 over a category "C" and a morphism "f" : "X" → "TY" let
Composition in the Kleisli category "C""T" can then be written
The extension operator satisfies the identities:
where "f" : "X" → "TY" and "g" : "Y" → "TZ". It follows trivially from these properties that Kleisli composition is associative and that "η""X" is the identity.
In fact, to give a monad is to give a "Kleisli triple" 〈"T", "η", (–)*〉, i.e. 
such that the above three equations for extension operators are satisfied.
Kleisli adjunction.
Kleisli categories were originally defined in order to show that every monad arises from an adjunction. That construction is as follows.
Let 〈"T", "η", "μ"〉 be a monad over a category "C" and let "C""T" be the associated Kleisli category. Using Mac Lane’s notation mentioned in the “Formal definition” section above, define a functor "F": "C" → "C""T" by
and a functor "G" : "C""T" → "C" by
One can show that "F" and "G" are indeed functors and that "F" is left adjoint to "G". The counit of the adjunction is given by
Finally, one can show that "T" = "GF" and "μ" = "GεF" so that 〈"T", "η", "μ"〉 is the monad associated to the adjunction 〈"F", "G", "η", "ε"〉.
Showing that "GF" = "T".
For any object "X" in category "C":
For any formula_33 in category "C":
Since formula_40 is true for any object "X" in "C" and formula_41 is true for any morphism "f" in "C", then formula_42. formula_43