Definition is_parameterized_NNO (N : C) (z : T --> N) (s : N --> N) : UU := ∏ (b y : C) (zy : b --> y) (sy : y --> y), ∃! (f : BC b N --> y), (BinProductArrow _ _ (identity _) (TerminalArrow _ _ · z) · f = zy) × (BinProductOfArrows _ _ _ (identity _) s · f = f · sy).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Arithmetic.NNO.