proposition: Lemma primitive_corecursion_existence : primitive_corecursion_characteristic_formula h.
proof: Proof. etrans. { apply assoc'. } etrans. { apply maponpaths. exact (! pr2 (@TerminalArrow (CoAlg_category F) (νF,,isTerminalνF) X_coproduct_νF_coalgebra)). } cbn. etrans. { apply assoc. } etrans. { apply maponpaths_2. apply BinCoproductIn1Commutes. } do 2 apply maponpaths. apply pathsinv0. exact (base_paths _ _ (TerminalArrowUnique (νF,, isTerminalνF) _ X_coproduct_νF_coalgebra_morphism_into_νF)). Qed.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total