Proposition isaprop_parameterized_NNO_if_univalent (HC : is_univalent C) : isaprop parameterized_NNO. Proof. use invproofirrelevance. intros N₁ N₂. use (parameterized_NNO_from_iso HC). - exact (iso_between_NNO (parameterized_NNO_to_NNO N₁) (parameterized_NNO_to_NNO N₂)). - apply (NNO_mor_Z _ (parameterized_NNO_to_NNO N₁)). - apply (NNO_mor_S _ (parameterized_NNO_to_NNO N₁)). 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.