proposition: Lemma j_mon_η : ∏ a : C, (Monads.η T_mon) a · j_mor a = (Monads.η M) a.
proof: Proof. intro a. etrans; [ apply assoc' |]. etrans. { apply cancel_precomposition. apply (nat_trans_eq_pointwise (algebra_mor_commutes _ _ _ j) a). } etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. apply BinCoproductIn1Commutes. } etrans; [ apply assoc' |]. etrans. { apply cancel_precomposition. apply BinCoproductIn1Commutes. } apply id_left. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.Notation UniMath.CategoryTheory.Monads.LModules UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.whiskering UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.Presheaf UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt UniMath.SubstitutionSystems.GenMendlerIteration_alt UniMath.CategoryTheory.Limits.Initial