proposition: Lemma unkleislify_kleislify (M : Monad C) : unkleislify (kleislify M) = M.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.KTriples UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful