[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Archimedean ordered rational integral domains... Given a commutative ring $R$, we could define the type of power series on $R$ as simply the sequence type $\mathbb{N} \to R$, with power series multiplication defined as convolution of sequences. Maybe we could just work with rational numbers, and sequences of functions of rational numbers as procedures for computation... 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... I don't believe in the entire field of topology; topology requires object classifiers, which are necessarily impredicative. We might as well just head towards the concept that pointwise continuous functions are uniformly continuous. Why even bother with that? Every function used in school is smooth. Just define directly smooth functions. 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