Lemma unkleislify_kleislify (M : Monad C) : unkleislify (kleislify M) = M. Proof. apply Monad_eq_raw_data. unfold Monad_to_raw_data. simpl. apply (pair_path_in2). apply total2_paths2. 2: apply idpath. apply total2_paths2. - apply funextsec. intro a. apply funextsec; intro b. apply funextfun; intro f. simpl. unfold map. unfold bind. unfold η. simpl. unfold Monads.bind, Monads.η. rewrite functor_comp. rewrite <- assoc. set (H:= Monad_law2 (T:=M) b). simpl in H. unfold Monads.η, Monads.μ in H. simpl in H. unfold Monads.μ. etrans. { apply cancel_precomposition. apply H. } apply id_right. - apply funextsec; intro x. set (H:= functor_id (C:=C) (C':=C) M (M x)). simpl in H. unfold μ. simpl. unfold bind, Monads.μ. simpl. unfold Monads.bind, Monads.μ. etrans. { apply cancel_postcomposition. apply H. } apply id_left. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.KTriples. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.