proposition: Lemma primitive_corecursion_aux (p : ∑ h : C ⟦ x, pr1 νF ⟧, primitive_corecursion_characteristic_formula h) : p = h,, primitive_corecursion_existence.
proof: Proof. use total2_paths_f. - assert (q : (pr1 p = BinCoproductIn1 (CP x (pr1 νF)) · (BinCoproductArrow (CP _ _) (pr1 p) (identity _)))). { apply pathsinv0, BinCoproductIn1Commutes. } etrans. 1: exact q. simpl. apply maponpaths. transparent assert ( f : ( CoAlg_category F ⟦ X_coproduct_νF_coalgebra, νF⟧)). { exists ( BinCoproductArrow (CP x (pr1 νF)) (pr1 p) (identity (pr1 νF))). cbn. etrans. 1: apply postcompWithBinCoproductArrow. etrans. 2: apply pathsinv0, postcompWithBinCoproductArrow. use (BinCoproductArrowUnique _ _ _ (CP x (pr1 νF)) (F (pr1 νF))). - etrans. 1: apply BinCoproductIn1Commutes. exact (! pr2 p). - etrans. 1: apply BinCoproductIn2Commutes. etrans. 1: apply assoc'. etrans. { apply maponpaths. etrans. 1: apply pathsinv0, functor_comp. apply maponpaths. apply BinCoproductIn2Commutes. } etrans. { apply maponpaths. apply functor_id. } exact (id_right _ @ ! id_left _). } exact (base_paths _ _ (TerminalArrowUnique (νF,, isTerminalνF) X_coproduct_νF_coalgebra f)). - apply homset_property. 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