Lemma j_mon_laws : Monad_Mor_laws (T:=T_mon) (T':=M) (mor_from_algebra_mor _ j). 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Monads.LModules. Require Import UniMath.SubstitutionSystems.SubstitutionSystems. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.SubstitutionSystems.LiftingInitial_alt. Require Import UniMath.SubstitutionSystems.GenMendlerIteration_alt. Require Import UniMath.CategoryTheory.Limits.Initial.