Lemma final_coalg_to_mhss_equation_morphism_is_factor {Z : PtdV} (f : pr1 Z --> t) : final_coalg_to_mhss_step_term f = CompletelyIterativeAlgebras.ϕ_for_cia CP I_H νH isTerminalνH (Z ⊗_{Act} t) (final_coalg_to_mhss_equation_morphism f). Proof. unfold final_coalg_to_mhss_step_term, CompletelyIterativeAlgebras.ϕ_for_cia, final_coalg_to_mhss_equation_morphism. repeat rewrite assoc'. do 3 apply maponpaths. unfold Const_plus_H, GeneralizedSubstitutionSystems.Const_plus_H. cbn. unfold BinCoproduct_of_functors_mor. etrans. { apply precompWithBinCoproductArrow. } rewrite postcompWithBinCoproductArrow. apply maponpaths_12. - cbn. rewrite id_left. rewrite assoc'. apply maponpaths. rewrite BinCoproductIn2Commutes. apply idpath. - etrans. 2: { repeat rewrite assoc'. rewrite BinCoproductIn1Commutes. apply pathsinv0, BinCoproductOfArrowsIn2. } apply idpath. Qed.
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.