I think the "Eudoxus reals" construction is worth thinking about too. It builds directly on integers instead of building on top of the rationals. https://ncatla

I think the "Eudoxus reals" construction is worth thinking about too. It builds directly on integers instead of building on top of the rationals. https://ncatlab.org/nlab/show/Eudoxus+real+number https://ncatlab.org/nlab/show/Eudoxus+real+number I wish history recorded how Eudoxus got to this. There was a paper speculating (iirc) that the Greeks started by thinking about continued fractions as a way to deal with incommensurables, and then realized you don't need that much machinery to define them. (You get continued fractions by running Euclid's algorithm on incommensurable input.)