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