Proposition parameterized_NNO_mor_unique {b y : C} {zy : b --> y} {sy : y --> y} (g g' : BC b N --> y) (gz : BinProductArrow _ _ (identity _) (TerminalArrow T b · parameterized_NNO_Z) · g = zy) (gs : BinProductOfArrows _ _ _ (identity b) parameterized_NNO_S · g = g · sy) (gz' : BinProductArrow _ _ (identity _) (TerminalArrow T b · parameterized_NNO_Z) · g' = zy) (gs' : BinProductOfArrows _ _ _ (identity b) parameterized_NNO_S · g' = g' · sy) : g = g'. Proof. refine (maponpaths (λ z, pr1 z) (proofirrelevance _ (isapropifcontr (H b y zy sy)) (g ,, _ ,, _) (g' ,, _ ,, _))). - exact gz. - exact gs. - exact gz'. - exact gs'. 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.