Definition mor_between_NNO (N₁ N₂ : NNO TC) : N₁ --> N₂. Proof. use NNO_mor. - exact (zeroNNO TC N₂). - exact (sucNNO TC N₂). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal.