Proposition is_NNO_parameterized_NNO_isaprop (y : C) (zy : T --> y) (sy : y --> y) : isaprop (∑ (u : N --> y), (parameterized_NNO_Z N · u = zy) × (parameterized_NNO_S N · u = u · sy)). Proof. use invproofirrelevance. intros g₁ g₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use is_NNO_parameterized_NNO_unique. - exact zy. - exact sy. - exact (pr12 g₁). - exact (pr22 g₁). - exact (pr12 g₂). - exact (pr22 g₂). 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.