proposition: Lemma Monad_to_Kleisli_to_Monad_raw_data {C : category} (T : Monad C) : Monad_to_raw_data (Kleisli_to_Monad (Monad_to_Kleisli T)) = Monad_to_raw_data T.
proof: Proof. apply (maponpaths (λ p, tpair _ _ p )); simpl. apply dirprod_paths. + apply dirprod_paths; repeat (apply funextsec; unfold homot; intro); simpl. * unfold r_lift, r_bind, r_eta; simpl. unfold Monads.bind. rewrite (functor_comp T), <- assoc. change (# T x1 · (# T (η T x0) · μ T x0) = #T x1). now rewrite (@Monad_law2 C T x0), id_right. * unfold Monads.bind, r_bind; simpl. now rewrite (functor_id T), id_left. + apply idpath. 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