proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.FunctorCoalgebras UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.Adamek UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.CompletelyIterativeAlgebras UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.CoproductsInActegories UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems UniMath.SubstitutionSystems.ActionScenarioForGenMendlerIteration_alt UniMath.SubstitutionSystems.SigmaMonoids