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