Definition τ_lmodule_mor : LModule_Mor _ _ _ := tpair (λ x, LModule_Mor_laws _ x) _ τ_lmodule_laws. End TauModuleMorphism. Context (IC : Initial C) (CC : Colims_of_shape nat_graph C) (HH : is_omega_cocont H). Let T := InitHSS _ CP IC CC H HH. Local Notation T_alg := (alg_from_hetsubst _ _ _ (hetsubst_from_hss _ _ _ T)). Local Notation T_mon := (Monad_from_hss _ _ _ T). Local Notation T_func := (T_mon : functor _ _). Local Notation T_hss := (T:hss _ _). Section fix_a_representation. Context (M : Monad C). Local Notation M_mod := (tautological_LModule M). Local Notation HM_mod := (lift_lmodule H _ M_mod). Context (τ_M: LModule_Mor M HM_mod M_mod). Local Definition M_alg : Alg. Proof. apply (tpair (λ x, EndC ⟦ Id_H x, x ⟧) (M:functor _ _)). apply BinCoproductArrow. - apply Monads.η. - apply τ_M. Defined.
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.SimplifiedHSS.SubstitutionSystems. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.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.SimplifiedHSS.LiftingInitial_alt. Require Import UniMath.SubstitutionSystems.GenMendlerIteration_alt. Require Import UniMath.CategoryTheory.Limits.Initial.