integer

import nat (+)

-- Int as a 𝕌-CODE (not a `type` item): a `type` name can only appear in
-- type position, but a `def ... : 𝕌` name is an ordinary term, usable
-- wherever a 𝕌-code is expected (e.g. the (A : 𝕌) argument of
-- equality.nova's generic combinators) — El Int in type position.
def Int : 𝕌 ≔ (ℕ ⨯ ℕ) / (p q. (p .π₁ + q .π₂ ≡ p .π₂ + q .π₁ ∈ _))
-- 0 = 0: (Z,Z) and (S Z, S Z) are the same integer
def zeroEq : class (Z , Z) ≡ class (S Z , S Z) ∈ El Int ≔ ⋆