proposition: Lemma Iteration_I_H_aux1 (av : V) (aη : I_{Mon_V} --> av) (aτ : H av --> av) (aα := av,, BinCoproductArrow (CP I_{ Mon_V} (H av)) aη aτ) (h : t --> pr1 aα) : pr21 t_Initial -->[ h] pr2 aα → τ · h = # H h · aτ × η · h = aη.
proof: Proof. intro Hyp. cbn in Hyp. split. + apply (maponpaths (fun x => BinCoproductIn2 _ · x)) in Hyp. rewrite assoc in Hyp. etrans. { exact Hyp. } etrans. { apply maponpaths. apply precompWithBinCoproductArrow. } apply BinCoproductIn2Commutes. + apply (maponpaths (fun x => BinCoproductIn1 _ · x)) in Hyp. rewrite assoc in Hyp. etrans. { exact Hyp. } etrans. { apply maponpaths. apply precompWithBinCoproductArrow. } cbn. rewrite id_left. apply BinCoproductIn1Commutes. 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