Lemma primitive_corecursion_aux (p : ∑ h : C ⟦ x, pr1 νF ⟧, primitive_corecursion_characteristic_formula h) : p = h,, primitive_corecursion_existence. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.