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