Definition Monad_to_Kleisli {C : category} : Monad C → KleisliMonad C := λ T, (functor_on_objects T ,, (pr1 (η T) ,, @bind C T)) ,, @Monad_law2 C T ,, (@η_bind C T ,, @bind_bind C T).
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monads.KTriples. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.RelativeMonads.