Library UniMath.CategoryTheory.NNO
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Local Open Scope cat.
Section nno.
Context {C : category} (TC : Terminal C).
Local Notation "1" := TC.
Definition isNNO (n : C) (z : C ⟦ 1, n ⟧) (s : C ⟦ n, n ⟧) : hProp.
Show proof.
Definition NNO : UU :=
∑ (n : C) (z : C ⟦ 1, n ⟧) (s : C ⟦ n, n ⟧), isNNO n z s.
Definition NNObject (n : NNO) : C := pr1 n.
Coercion NNObject : NNO >-> ob.
Definition zeroNNO (n : NNO) : C ⟦1,n⟧ := pr1 (pr2 n).
Definition sucNNO (n : NNO) : C ⟦n,n⟧ := pr1 (pr2 (pr2 n)).
Lemma isNNO_NNO (n : NNO) : isNNO n (zeroNNO n) (sucNNO n).
Show proof.
Definition make_NNO (n : C) (z : C ⟦ 1, n ⟧) (s : C ⟦ n, n ⟧)
(h : isNNO n z s) : NNO := (n,,z,,s,,h).
Definition hasNNO : hProp := ∥ NNO ∥.
End nno.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Local Open Scope cat.
Section nno.
Context {C : category} (TC : Terminal C).
Local Notation "1" := TC.
Definition isNNO (n : C) (z : C ⟦ 1, n ⟧) (s : C ⟦ n, n ⟧) : hProp.
Show 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).
- 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).
Definition NNO : UU :=
∑ (n : C) (z : C ⟦ 1, n ⟧) (s : C ⟦ n, n ⟧), isNNO n z s.
Definition NNObject (n : NNO) : C := pr1 n.
Coercion NNObject : NNO >-> ob.
Definition zeroNNO (n : NNO) : C ⟦1,n⟧ := pr1 (pr2 n).
Definition sucNNO (n : NNO) : C ⟦n,n⟧ := pr1 (pr2 (pr2 n)).
Lemma isNNO_NNO (n : NNO) : isNNO n (zeroNNO n) (sucNNO n).
Show proof.
Definition make_NNO (n : C) (z : C ⟦ 1, n ⟧) (s : C ⟦ n, n ⟧)
(h : isNNO n z s) : NNO := (n,,z,,s,,h).
Definition hasNNO : hProp := ∥ NNO ∥.
End nno.