Proposition mor_between_NNO_inv (N₁ N₂ : NNO TC) : mor_between_NNO N₁ N₂ · mor_between_NNO N₂ N₁ = identity _. Proof. unfold mor_between_NNO. use NNO_mor_unique. - exact (zeroNNO TC N₁). - exact (sucNNO TC N₁). - rewrite !assoc. rewrite !NNO_mor_Z. apply idpath. - apply id_right. - rewrite !assoc. rewrite NNO_mor_S. rewrite !assoc'. rewrite NNO_mor_S. apply idpath. - rewrite id_left, id_right. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal.