Lemma kleislify_mor_law {C : category} {M M' : Monad C} (α : Monad_Mor M M') : Kleisli_Mor_laws (kleislify M) (kleislify M') (λ x : C, α x). Proof. split; simpl; intros. - apply Monad_Mor_η. - unfold bind. unfold Monad_Kleisli_data. simpl. unfold Monads.bind. rewrite functor_comp. do 2 rewrite assoc. set (H := nat_trans_ax α). simpl in H. rewrite <- H. rewrite assoc4. rewrite <-H. rewrite <- assoc4. set (H2 := Monad_Mor_μ α b). simpl in H2. do 3 rewrite <- assoc. unfold Monads.μ in H2. simpl in H2. unfold Monads.μ. simpl. do 3 rewrite assoc. rewrite assoc4. repeat rewrite <- assoc. apply cancel_precomposition. rewrite assoc. rewrite H. apply pathsinv0. apply H2. 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.