Definition isNNO (n : C) (z : C ⟦ 1, n ⟧) (s : C ⟦ n, n ⟧) : hProp. Proof. use tpair. - exact (∏ (a : C) (q : C ⟦ 1, a ⟧) (f : C ⟦ a, a ⟧), ∃! u : C ⟦ n, a ⟧, (z · u = q) × (s · u = u · f)). - abstract (repeat (apply impred_isaprop; intros); apply isapropiscontr). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal.