Then came another course with set theory which adds a ‘belongs to’ predicate (‘∈’) and a few axioms. In set theory everything is a set as in computer machine language everything is a bit, or informal collections of them. To reason about natural numbers some representation of a natural number was required. Several were proposed historically but von Neumann’s won the day: 3 = {0, 1, 2}, etc. After proving Peano’s axioms for natural numbers to convince most that von Neumann’s constructs were really just like natural numbers the representation details were swept under the rug whereupon it was considered declassé to write 3 ⊂ 5 which is so since von Neumann’s natural numbers were really sets.
This style of hiding but not ultimately denying that natural numbers were sets was palpable. If I understand the type notions presented in this paper then their plan is to formally hide such representation details.
While each natural number was represented as a unique set, subsequent math constructs were more conveniently represented by equivalence classes where some equivalence relation was specified. These equivalence classes were typically infinite. For instance integers, including negative integers, were most conveniently represented as pairs of natural numbers. –3 = { … <5, 8>, <6, 9>, …}. This is probably not how a programmer would introduce signed integers starting with only unsigned integers, but it would work. The paper takes pairs of integers whose ratio is a rational number of interest. That was what the math foundations class did also. That requires specifying an equivalence relation between pairs. That relation must be symmetric, reflexive and transitive.
These two techniques are close to the above ideas and may even be included.
How do these ideas differ from ordinary abstraction?