Definition NNO_mor : N --> x := pr11 (isNNO_NNO N x z s).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal.