[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] If we have a Cauchy complete Archimedean ordered field $\mathbb{R}$, then we can construct the Cauchy real numbers as the set of elements of $\mathbb{R}$ which merely has a locator... Most of mathematics only requires a real numbers type $\mathbb{R}$, function types of the real numbers $\mathbb{R} \to \mathbb{R}$, and functions types of function types of the real numbers $(\mathbb{R} \to \mathbb{R}) \to (\mathbb{R} \to \mathbb{R})$ (i.e. operators). Without quotient sets one cannot just say terminal Archimedean ordered field, but one has to say terminal Cauchy complete Archimedean ordered field. We follow Booij 2020 and define the following Archimedean ordered fields: * A **real number field** is a Cauchy complete Archimedean ordered field * The **Euclidean real numbers** are the initial real number field * The **Dedekind real numbers** are the terminal real number field * The **Cauchy real numbers** are the set of real numbers in any real number field which merely has a locator If we have propositional resizing, then there are impredicative definitions of the Euclidean and Dedekind real numbers: * The Dedekind real numbers are the set of two-sided Dedekind cuts of rational numbers. * The Euclidean real numbers are the meet of all real number subfields of the Dedekind real numbers. In addition, we have a number of axioms which are analytic LPO: * The Euclidean analytic LPO says that the Euclidean real numbers are a discrete field * The Dedekind analytic LPO says that the Dedekind real numbers are a discrete field * The Cauchy analytic LPO says that the Cauchy real numbers are a discrete field category: redirected to nlab