proposition: Lemma final_coalg_to_mhss_has_equivalent_characteristic_formula {Z : PtdV} (f : pr1 Z --> t) (h : Z ⊗_{Act} t --> t) : primitive_corecursion_characteristic_formula CP (ϕ f) h ≃ mbracket_property_parts Mon_V H θ t η τ (pr2 Z) f h.
proof: Proof. apply weqimplimpl. - intro Hcorec. apply (pr2 (mbracket_property_single_equivalent _ _ _ _ _ _ CP _ _ _)). red. red in Hcorec. fold out t in Hcorec. rewrite ητ_is_out_inv. apply pathsinv0, (z_iso_inv_on_left _ _ _ _ out_z_iso) in Hcorec. etrans. { apply maponpaths. exact Hcorec. } clear Hcorec. unfold ϕ, final_coalg_to_mhss_step_term. etrans. { repeat rewrite assoc. do 6 apply cancel_postcomposition. rewrite assoc'. apply maponpaths. 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_right. etrans. { do 5 apply cancel_postcomposition. apply (pr2 δ). } rewrite id_left. repeat rewrite assoc'. apply maponpaths. etrans. { apply maponpaths. rewrite assoc. apply cancel_postcomposition. rewrite (assoc f out). apply pathsinv0. use changing_the_constant_Const_plus_H. apply BinCoproductIn2Commutes. } etrans. { repeat rewrite assoc. do 2 apply cancel_postcomposition. etrans. { apply pathsinv0, (functor_comp (Const_plus_H (pr1 Z))). } apply maponpaths. apply BinCoproductIn1Commutes. } repeat rewrite assoc'. apply maponpaths. etrans. { apply postcompWithBinCoproductArrow. } rewrite assoc'. apply maponpaths_2. etrans. { apply maponpaths. apply (pr122 out_z_iso). } apply id_right. - intro Hmhss. apply (pr1 (mbracket_property_single_equivalent _ _ _ _ _ _ CP _ _ _)) in Hmhss. red. red in Hmhss. fold out t. 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. { apply cancel_postcomposition. exact Hmhss. } clear Hmhss. unfold ϕ, final_coalg_to_mhss_step_term. repeat rewrite assoc'. do 2 apply maponpaths. etrans. 2: { do 2 apply maponpaths. rewrite (assoc f out). use changing_the_constant_Const_plus_H. apply BinCoproductIn2Commutes. } apply maponpaths. etrans. 2: { repeat rewrite assoc. apply cancel_postcomposition. etrans. 2: { apply (functor_comp (Const_plus_H (pr1 Z))). } apply maponpaths. apply pathsinv0, BinCoproductIn1Commutes. } apply maponpaths. etrans. { apply postcompWithBinCoproductArrow. } apply maponpaths. unfold τ. etrans. { rewrite assoc'. apply maponpaths. apply (pr222 out_z_iso). } apply id_right. - 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