Definition iso_between_NNO (N₁ N₂ : NNO TC) : z_iso N₁ N₂. Proof. use make_z_iso. - apply mor_between_NNO. - apply mor_between_NNO. - abstract (split ; apply mor_between_NNO_inv). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal.