proposition: 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: 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.
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