Lemma j_mon_square_eq2 : # L (alg_map Id_H T_alg) · ((j_mor ø T_mon : EndC ⟦_∙_, _∙_⟧) · (M ∘ j_mor : EndC ⟦_∙_, _∙_⟧) · μ M) = (ψ : nat_trans _ _) `T_alg ((j_mor ø T_mon : EndC ⟦_∙_, _∙_⟧) · (M ∘ j_mor : EndC ⟦_∙_, _∙_⟧) · μ M). Proof. apply coprod_iter_eq; intro x. - etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. etrans; [ apply assoc |]. apply cancel_postcomposition. apply j_mon_η. } etrans. { apply cancel_postcomposition. eapply pathsinv0. apply (nat_trans_ax (Monads.η M )). } etrans; [| apply id_right ]. rewrite <- assoc. apply cancel_precomposition. apply Monad_law1. - etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. apply j_mor_rep. } rewrite <- assoc. apply cancel_precomposition. eapply pathsinv0. apply (nat_trans_ax τ_M). } etrans. { repeat rewrite <- assoc. apply cancel_precomposition. apply cancel_precomposition. apply (LModule_Mor_σ _ τ_M ( x)). } repeat rewrite assoc. apply cancel_postcomposition. etrans. { repeat rewrite <- assoc. apply cancel_precomposition. etrans; [ apply assoc |]. apply cancel_postcomposition. apply (θ_nat_2_pw _ _ _ j_ptd). } etrans. { repeat rewrite assoc. apply cancel_postcomposition. apply cancel_postcomposition. apply (θ_nat_1_pw _ _ j_mor (ptd_from_mon T_mon)). } repeat rewrite <- assoc. apply cancel_precomposition. rewrite functor_comp. rewrite functor_comp. repeat rewrite assoc. apply cancel_postcomposition. rewrite <- functor_comp. etrans; [ apply functor_comp_pw |]. apply functor_cancel_pw. apply nat_trans_eq_alt. intro y. etrans. { apply cancel_postcomposition. etrans. { apply cancel_precomposition. apply functor_id. } apply id_right. } apply cancel_precomposition. apply id_left. 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.