A monad is an endofunctor with natural transformations and satisfying
Its Kleisli category has the same objects as , with , identity , and composite
The unit laws follow from naturality of and the two monad unit laws. For , the two triple composites reduce, using naturality of , to
they agree by the monad associativity law. Thus this is a category.
Define the free functor into a Kleisli category and the right-hand functor by
The identity and composition formulas for are
For , , and
where the last step is naturality of . Hence both mappings are functors. The hom-set identity gives the adjunction . Its unit is , and its counit at is the Kleisli arrow represented by . Applying to that counit gives , so the induced monad is the specified one.
For any inducing this same monad, with counit , define the Kleisli comparison functor
The triangular identities give , and naturality of the counit together with gives . Explicitly, naturality moves past , then moves the resulting counit past , reducing the composite to . Thus is a functor, with and , and it sends the Kleisli counit to .
An adjunction morphism here is required to commute with the left and right adjoints and preserve their adjunction structure. Such a morphism must have the above object map; every Kleisli arrow factors as its counit after , so its arrow map is forced as well. This proves initiality of the Kleisli adjunction: