Definition 1.8.4.1. We define:

ℤ :=: {(*n*-*m*) | *n*, *m* ∈ ℕ}

Remarks.

This is essentially the standard definition of integers as equivalence classes of pairs of natural numbers. We just use a notation that highlights the role of the two numbers in each pair. This notation is later justified by `$"Actual difference equals formal difference"`

).

Since an equality definition for each constructor is always part of a construction, we do not need to build the equivalence classes explicitly, they are implicit in the choice of the equality definition.

When defining a construction, another set can be embedded in the newly defined set, so in this case, we embed the natural numbers. Note that they are also embedded in the cardinal numbers.

References.

- https://en.wikipedia.org/wiki/Integer
- https://mathworld.wolfram.com/Integer.html
- https://proofwiki.org/wiki/Definition:Integer
- https://ncatlab.org/nlab/show/integer
- https://coq.inria.fr/library/Coq.ZArith.BinInt.html (but uses a different encoding as an inductive data type with three constructors)
- https://leanprover-community.github.io/mathlib_docs/init/data/int/basic.html#int (but uses a different encoding as an inductive data type with two constructors)