proposition: Lemma nat_ob_NNO {C : category} (BC : BinCoproducts C) (hsC : has_homsets C) (TC : Terminal C) : nat_ob _ BC TC → NNO TC.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.NNO UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Limits.Coproducts