Proposition is_NNO_parameterized_NNO_unique {g₁ g₂ : N --> y} (zg₁ : parameterized_NNO_Z N · g₁ = zy) (sg₁ : parameterized_NNO_S N · g₁ = g₁ · sy) (zg₂ : parameterized_NNO_Z N · g₂ = zy) (sg₂ : parameterized_NNO_S N · g₂ = g₂ · sy) : g₁ = g₂. Proof. assert (BinProductPr2 _ (BC T N) · g₁ = BinProductPr2 _ (BC T N) · g₂) as p. { use parameterized_NNO_mor_unique. - exact zy. - exact sy. - rewrite !assoc. rewrite BinProductPr2Commutes. refine (_ @ zg₁). rewrite (TerminalEndo_is_identity (TerminalArrow T T)). rewrite id_left. apply idpath. - rewrite !assoc. rewrite BinProductOfArrowsPr2. rewrite !assoc'. apply maponpaths. exact sg₁. - rewrite !assoc. rewrite BinProductPr2Commutes. refine (_ @ zg₂). rewrite (TerminalEndo_is_identity (TerminalArrow T T)). rewrite id_left. apply idpath. - rewrite !assoc. rewrite BinProductOfArrowsPr2. rewrite !assoc'. apply maponpaths. exact sg₂. } pose proof (maponpaths (λ z, BinProductArrow _ _ (TerminalArrow _ _) (identity _) · z) p) as q. cbn in q. refine (_ @ q @ _). - rewrite !assoc. rewrite BinProductPr2Commutes. rewrite id_left. apply idpath. - rewrite !assoc. rewrite BinProductPr2Commutes. rewrite id_left. apply idpath. 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.