Proposition NNO_mor_unique {f g : N --> x} (fz : zeroNNO N · f = z) (gz : zeroNNO N · g = z) (fs : sucNNO N · f = f · s) (gs : sucNNO N · g = g · s) : f = g. Proof. exact (base_paths _ _ (proofirrelevance _ (isapropifcontr (isNNO_NNO N x z s)) (f ,, fz ,, fs) (g ,, gz ,, gs))). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal.