Definition 1.8.4.1.  We define:
ℤ :=: {(n-m) | n, m ∈ }
(n-m) = (n'-m')  :⇔  n + m' = n' + m  (n, m ∈ , n', m' ∈ )
Reflexivity.  No proof.
Symmetry.  No proof.
Transitivity.  No proof.
 ⊆: ℤ viax = (x-0)
Well-definedness.  Let x, y ∈  such that (x-0) = (y-0). Then x = y:
(x-0) = (y-0)defx + 0 = y + 0defx = y
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.