proposition: Lemma j_mon_laws : Monad_Mor_laws (T:=T_mon) (T':=M) (mor_from_algebra_mor _ j).
proof: Proof. split. - apply (nat_trans_eq_pointwise (a:= compose (C:=EndC) (μ T_mon) j_mor) (a':= compose(C:=EndC) (compose (C:=EndC) (a:=_∙_) (b:=_∙_) (c:=_∙_) (j_mor ø T_mon ) (M ∘ j_mor) ) (μ M))). apply (uniqueExists uniq_iter). + exact j_mon_square_eq1. + exact j_mon_square_eq2. - apply j_mon_η. 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