Proposition parameterized_NNO_from_iso (HC : is_univalent C) {N₁ N₂ : parameterized_NNO} (f : z_iso N₁ N₂) (pz : parameterized_NNO_Z N₁ · f = parameterized_NNO_Z N₂) (ps : parameterized_NNO_S N₁ · f = f · parameterized_NNO_S N₂) : N₁ = N₂. Proof. use parameterized_NNO_eq. - exact (isotoid _ HC f). - rewrite idtoiso_isotoid. exact pz. - rewrite !idtoiso_isotoid. exact ps. 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.