Proposition parameterized_NNO_eq {N₁ N₂ : parameterized_NNO} (p : (N₁ : C) = N₂) (pz : parameterized_NNO_Z N₁ · idtoiso p = parameterized_NNO_Z N₂) (ps : parameterized_NNO_S N₁ · idtoiso p = idtoiso p · parameterized_NNO_S N₂) : N₁ = N₂. Proof. induction N₁ as [ N₁ [ z₁ [ s₁ H₁ ] ] ]. induction N₂ as [ N₂ [ z₂ [ s₂ H₂ ] ] ]. cbn in *. induction p ; cbn in *. rewrite id_right in pz. rewrite id_left, id_right in ps. induction pz, ps. do 3 apply maponpaths. apply isaprop_is_parameterized_NNO. 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.