proposition: Lemma final_coalg_to_mhss_equation_morphism_has_equivalent_characteristic_formula {Z : PtdV} (f : pr1 Z --> t) (h : Z ⊗_{Act} t --> t) : cia_characteristic_formula CP I_H (CompletelyIterativeAlgebras.Xinv _ _ isTerminalνH) (final_coalg_to_mhss_equation_morphism f) h ≃ mbracket_property_parts Mon_V H θ t η τ (pr2 Z) f h.
proof: Proof. apply weqimplimpl. - intro Hcia. apply (pr2 (mbracket_property_single_equivalent _ _ _ _ _ _ CP _ _ _)). red. red in Hcia. rewrite ητ_is_out_inv. etrans. { apply maponpaths. exact Hcia. } clear Hcia. unfold final_coalg_to_mhss_equation_morphism. etrans. { repeat rewrite assoc'. apply maponpaths. repeat rewrite assoc. do 5 apply cancel_postcomposition. etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Act Z)). } etrans. { apply maponpaths. apply (pr222 out_z_iso). } apply (functor_id (leftwhiskering_functor Act Z)). } rewrite id_left. etrans. { repeat rewrite assoc. do 4 apply cancel_postcomposition. apply (pr2 δ). } rewrite id_left. repeat rewrite assoc'. apply maponpaths. unfold GeneralizedSubstitutionSystems.Const_plus_H. cbn. unfold BinCoproduct_of_functors_mor. rewrite precompWithBinCoproductArrow. etrans. 2: { apply pathsinv0, precompWithBinCoproductArrow. } rewrite postcompWithBinCoproductArrow. apply maponpaths_12. + rewrite assoc'. rewrite BinCoproductIn2Commutes. do 2 rewrite id_right. apply pathsinv0, id_left. + repeat rewrite assoc'. etrans. { apply maponpaths. apply BinCoproductIn1Commutes. } rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductOfArrowsIn2. } rewrite assoc'. apply idpath. - intro Hmhss. apply (pr1 (mbracket_property_single_equivalent _ _ _ _ _ _ CP _ _ _)) in Hmhss. red. red in Hmhss. rewrite ητ_is_out_inv in Hmhss. rewrite assoc' in Hmhss. apply (z_iso_inv_to_left _ _ _ (_,,bincoprod_functor_lineator_strongly Mon_PtdV CP Act δ (pr1 Z,, pr2 Z) (I_{ Mon_V},,H t))) in Hmhss. apply (z_iso_inv_to_left _ _ _ (functor_on_z_iso (leftwhiskering_functor Act (pr1 Z,, pr2 Z)) out_z_iso)) in Hmhss. etrans. { exact Hmhss. } clear Hmhss. unfold final_coalg_to_mhss_equation_morphism. repeat rewrite assoc'. do 3 apply maponpaths. unfold GeneralizedSubstitutionSystems.Const_plus_H. cbn. unfold BinCoproduct_of_functors_mor. rewrite precompWithBinCoproductArrow. etrans. { apply precompWithBinCoproductArrow. } rewrite postcompWithBinCoproductArrow. apply maponpaths_12. + rewrite assoc'. rewrite BinCoproductIn2Commutes. do 2 rewrite id_right. apply id_left. + repeat rewrite assoc'. etrans. 2: { apply maponpaths. apply pathsinv0, BinCoproductIn1Commutes. } rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn2. } rewrite assoc'. apply idpath. - apply V. - apply isaprop_mbracket_property_parts. 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