Definition Kleisli_to_functor {C : category} (T: KleisliMonad C) : C ⟶ C. Proof. use make_functor. - use make_functor_data. + exact (RelMonad_from_Kleisli T). + apply r_lift. - apply is_functor_r_lift. Defined.
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.