Proposition id_preserves_parameterized_NNO_eq {C : category} (T : Terminal C) (BC : BinProducts C) (N : parameterized_NNO T BC) : identity N = preserves_parameterized_NNO_mor N N _ (identity_preserves_terminal C). Proof. use is_NNO_parameterized_NNO_unique. - exact (parameterized_NNO_Z N). - exact (parameterized_NNO_S N). - apply id_right. - rewrite id_left, id_right. apply idpath. - etrans. { exact (preserves_parameterized_NNO_mor_Z N N _ (identity_preserves_terminal C)). } cbn. etrans. { apply maponpaths_2. refine (!_). apply (functor_on_terminal_arrow _ (identity_preserves_terminal _)). } cbn. etrans. { apply maponpaths_2. exact (TerminalEndo_is_identity (TerminalArrow T T)). } apply id_left. - exact (preserves_parameterized_NNO_mor_S N N _ (identity_preserves_terminal C)). 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.