proposition: Lemma isNNO_nat : isNNO TerminalHSET natHSET (λ _, 0) S.
proof: Proof. intros X z s. use unique_exists. + intros n. induction n as [|_ n]. * exact (z tt). * exact (s n). + now split; apply funextfun; intros []. + now intros; apply isapropdirprod; apply homset_property. + intros q [hq1 hq2]. apply funextfun; intros n. induction n as [|n IH]. * now rewrite <- hq1. * cbn in *; now rewrite (toforallpaths _ _ _ hq2 n), IH. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.NNO UniMath.CategoryTheory.SubobjectClassifier UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Categories.Type.MonoEpiIso UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.covyoneda UniMath.CategoryTheory.EpiFacts UniMath.CategoryTheory.Monics UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.ElementaryTopos UniMath.CategoryTheory.PowerObject UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Categories.HSET.Univalence