Lemma primitive_corecursion_formula_with_inverse : h = ϕ · #F (BinCoproductArrow (CP _ _) h (identity _)) · (α' _ _ _ isTerminalνF). Proof. etrans. 2: { exact (maponpaths (fun x => x · α' C F νF isTerminalνF) primitive_corecursion_existence). } rewrite assoc'. etrans. 2: { apply maponpaths, pathsinv0, αα'_idA. } apply pathsinv0, id_right. 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.