Proposition NNO_mor_Z : zeroNNO N · NNO_mor = z. Proof. exact (pr121 (isNNO_NNO N x z s)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal.