Lemma j_mon_square_eq1 : # L (alg_map Id_H T_alg) · ((μ T_mon : EndC ⟦_, _⟧) · j_mor) = (ψ : nat_trans _ _) `T_alg ((μ T_mon : EndC ⟦_, _⟧) · j_mor). Proof. apply coprod_iter_eq; intro x. - etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. apply (Monad_law1 (T:=T_mon)). } apply id_left. - etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. apply (LModule_Mor_σ _ τT). } etrans; [ apply assoc' |]. etrans; [ apply assoc' |]. etrans; [| apply assoc ]. apply cancel_precomposition. rewrite functor_comp. etrans; [| apply assoc ]. apply cancel_precomposition. apply j_mor_rep. 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.