In constructive mathematics there are many possible inequivalent definitions of real numbers. The greatest variety seems to be in Dedekind-style approaches: in addition to "the" Dedekind real numbers which satisfy locatedness (for all $q<r$ in $\mathbb{Q}$, either $x<r$ or $q<x$), there are the MacNeille, upper, and lower reals, and perhaps others. It is easy to construct models distinguishing between all these: for instance, in a topos of sheaves on a space $X$, the Dedekind reals are the sheaf of continuous $\mathbb{R}$-valued functions on $X$, the upper and lower reals are respectively the sheaves of upper and lower semicontinuous $\mathbb{R}$-valued functions on $X$, and the MacNeille reals are the sheaf of pairs of upper and lower semicontinuous functions satisfying a closeness condition. This gives me a good topological intuition for the difference between these definitions.

This question is about an analogous possible variation in Cauchy-like real numbers. Classically, a sequence $(x_n)$ of rational numbers is Cauchy if $\forall k \exists n \forall p,q>n. |x_p-x_q|<2^{-k}$. But almost without exception, constructive mathematicians define Cauchy sequences by "building a Skolem function" into the definition, assuming that there is a "modulus of Cauchy-ness" $N:\mathbb{N}^{\mathbb{N}}$ such that $\forall k \forall p,q > N_k. |x_p-x_q|<2^{-k}$. And once one has such a modulus, one can massage the sequence $(x_n)$ to make the modulus coincide with a standard one such as $N_k = k$.

My question is: what is the difference in constructive mathematics between Cauchy real numbers having a modulus of Cauchy-ness and without it? It seems to me that the no-modulus Cauchy reals sit in between the with-modulus Cauchy reals and the Dedekind reals; we shoudn't need a modulus to get locatedness, all we need is the *existence* of some point of the sequence that's closer than $\frac{|q-r|}{2}$ to the limit so we can compare it to $q$ and $r$.

I understand that someone who cares about algorithms and computation will want a modulus to compute with, but if I am a topologist and am happy with Dedekind reals, leaving out a modulus in the Cauchy reals is not *a priori* a bad thing to do. Are the no-modulus Cauchy reals any less well-behaved *intrinsically* than the with-modulus ones? Is their algebraic and order structure any different? And are there (hopefully topological) models (necessarily failing countable choice) that distinguish the no-modulus Cauchy reals from both the with-modulus ones and from the Dedekind reals?

equivalence classesof Cauchy sequences. $\endgroup$ – Mike Shulman Jan 4 '18 at 17:24equivalence classesof Cauchy sequences in defining the Cauchy reals, so the question is about comparing equivalence classes of Cauchy sequences for which there exists a modulus to equivalence classes of Cauchy sequences equipped with a modulus. But I think these are isomorphic, as long as we have the function comprehension (unique choice) principle. $\endgroup$ – Mike Shulman Jan 4 '18 at 17:49