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. 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.
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.