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