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. 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.
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.