Proposition isaprop_parameterized_NNO (C : univalent_category) (T : Terminal C) (BC : BinProducts C) : isaprop (parameterized_NNO T BC). Proof. use isaprop_parameterized_NNO_if_univalent. apply univalent_category_is_univalent. Qed.
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.