Proposition Kleisli_to_Monad_to_Kleisli {C : category} (T : KleisliMonad C) : Monad_to_Kleisli (Kleisli_to_Monad T) = T. 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.
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.