Lemma nat_ob_NNO {C : category} (BC : BinCoproducts C) (hsC : has_homsets C) (TC : Terminal C) : nat_ob _ BC TC → NNO TC. Proof. intros N. use make_NNO. - exact (nat_ob_carrier _ _ _ N). - apply nat_ob_z. - apply nat_ob_s. - intros n z s. use unique_exists. + apply (nat_ob_rec _ _ _ _ z s). + split; [ apply nat_ob_rec_z | apply nat_ob_rec_s ]. + intros x; apply isapropdirprod; apply hsC. + intros x [H1 H2]. transparent assert (xalg : (FunctorAlg (BinCoproduct_of_functors C C BC (constant_functor C C TC) (functor_identity C)) ⟦ InitialObject N, make_F_alg C BC TC z s ⟧)). { refine (x,,_). abstract (apply pathsinv0; etrans; [apply precompWithBinCoproductArrow |]; rewrite id_left, <- H1; etrans; [eapply maponpaths, pathsinv0, H2|]; now apply pathsinv0, BinCoproductArrowUnique; rewrite assoc; apply maponpaths). } exact (maponpaths pr1 (InitialArrowUnique N (make_F_alg C BC TC z s) xalg)). 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.