[[!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. category: redirected to nlab