Lemma nat_ob_rec_z (N : nat_ob) {X : ob C} : ∏ (f : 1 --> X) (g : X --> X), nat_ob_z N · nat_ob_rec N f g = f. Proof. intros f g. pose (inlN := BinCoproductIn1 (bc 1 N)). pose (succ := nat_ob_s N). pose (diagram := maponpaths (fun x => inlN · x) (algebra_mor_commutes F (pr1 N) _ (InitialArrow N (make_F_alg f g)))). rewrite (F_compute2 _) in diagram. rewrite (BinCoproductArrowEta C 1 X (bc _ _) _ _) in diagram. rewrite (precompWithBinCoproductArrow C (bc 1 N) (bc 1 X) (identity 1) _ _ _) in diagram. rewrite (BinCoproductIn1Commutes C 1 N (bc 1 _) _ _ _) in diagram. rewrite (id_left _) in diagram. rewrite assoc in diagram. rewrite (BinCoproductArrowEta C 1 N (bc _ _) _ _) in diagram. refine (_ @ (BinCoproductIn1Commutes C _ _ (bc 1 _) _ f g)). rewrite (!BinCoproductIn1Commutes C _ _ (bc 1 _) _ 0 succ). unfold nat_ob_rec in *. exact diagram. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. 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.whiskering. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Arithmetic.NNO. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.Coproducts.