proposition: Proposition Kleisli_to_Monad_to_Kleisli {C : category} (T : KleisliMonad C) : Monad_to_Kleisli (Kleisli_to_Monad T) = T.
proof: Proof. apply subtypePath. - intro. do 2 try apply isapropdirprod; do 5 try (apply impred; intro); apply homset_property. - apply (maponpaths (λ p, tpair _ _ p )); simpl. apply dirprod_paths. * apply idpath. * repeat (apply funextsec; unfold homot; intro). simpl; unfold Monads.bind; simpl; unfold r_lift. now rewrite (r_bind_r_bind T), <- assoc, (r_eta_r_bind T (T x0)), id_right. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monads.KTriples UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.RelativeMonads