Abstract
The type of real numbers is constructed from the positive rationals
using the method of Dedekind cuts. This development, briefly described
in papers by the authors, follows the textbook presentation by
Gleason. It's notable that the first formalisation of a
significant piece of mathematics, by Jutting in 1977, involved a
similar construction.