Kleisli Category - Formal Definition

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 as above, we associate with each object in a new object, and for each morphism in a morphism . Together, these objects and morphisms form our category, where we define

Then the identity morphism in is