Lemma Kleisli_composition_laws {C : category} {T T' T'' : KleisliMonad C} (α : Kleisli_Mor T T') (α' : Kleisli_Mor T' T'') : Kleisli_Mor_laws T T'' (λ a : C, nat_trans_from_kleisli_mor α a · nat_trans_from_kleisli_mor α' a). Proof. split; intros; simpl. - rewrite assoc. set (H := Kleisli_Mor_η α). rewrite H. apply Kleisli_Mor_η. - pathvia (nat_trans_from_kleisli_mor α a · (nat_trans_from_kleisli_mor α' a · bind T'' ((f · nat_trans_from_kleisli_mor α b) · nat_trans_from_kleisli_mor α' b))). * now repeat rewrite assoc. * rewrite (Kleisli_Mor_bind α'). rewrite assoc. rewrite (Kleisli_Mor_bind α). apply pathsinv0. apply assoc. 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.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.RelativeMonads.