Definition I_H : functor V V := Const_plus_H I_{Mon_V}.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.FunctorCoalgebras. Require Import UniMath.CategoryTheory.coslicecat. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Adamek. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.CompletelyIterativeAlgebras. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.CoproductsInActegories. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Require Import UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems. Require Import UniMath.SubstitutionSystems.ActionScenarioForGenMendlerIteration_alt. Require Import UniMath.SubstitutionSystems.SigmaMonoids. Import BifunctorNotations. Import MonoidalNotations. Theorem SigmaMonoidFromInitialAlgebra_is_initial : isInitial _ σ. Definition SigmaMonoidFromInitialAlgebraInitial : Initial (SigmaMonoid θ) := σ,,SigmaMonoidFromInitialAlgebra_is_initial.