Equivalence of real numbers in terms of Dedekind cuts and Cauchy nets of rational numbers We work in weakly predicatively constructive mathematics, in that we accept function sets but do not accept power sets or excluded middle. More specifically, we shall assume a sequential universe hierarchy in our foundations, where the elements of every universe are (codes for) sets, and every universe $\mathcal{V}$ embeds into a successor universe $\mathcal{V}'$. While there is no global 'set of all propositions', for every universe $\mathcal{V}$ there is a 'set of all propositions of a universe' $\mathrm{Prop}_\mathcal{V}$ which lies in the next universe $\mathcal{V}'$, where 'proposition' is defined as 'set where every element is equal to every other element'.
In the following question, a Dedekind real number is a two-sided, located, open, rounded, bounded Dedekind cut. A generalised Cauchy real number is an equivalence class of Cauchy nets of rational numbers, in the same way that a Cauchy real number is an equivalence class of Cauchy sequences of rational numbers. Unlike the case with Cauchy sequences in constructive mathematics, here it doesn't matter whether the Cauchy nets come with moduli of convergence or not, because the moduli of convergence are given by a net regardless whether the foundations is classical or constructive. In addition, given a set of rational numbers $\mathbb{Q}$ in a universe $\mathcal{V}$, due to the weakly predicative nature of the foundations, both the set of Dedekind real numbers and the set of generalised Cauchy real numbers lie in the next universe $\mathcal{V}'$. This isn't the case in impredicative mathematics, as only the generalised Cauchy real numbers lie in $\mathcal{V}'$, the Dedekind real numbers lie in $\mathcal{V}$.
This paragraph appears on the nLab's article about Cauchy real numbers:

Every generalised Cauchy real number becomes a Dedekind real number in the usual way, defining lower and upper sets in terms of the order relation on generalised Cauchy real numbers. Furthermore, any two generalised Cauchy real numbers are equal as generalised Cauchy real numbers if and only if they are equal as Dedekind cuts. Conversely, any Dedekind cut is equal (as a Dedekind cut) to some generalised Cauchy real number.

However the nLab does not provide a proof that these two are equivalent. Is the nLab's statement correct, and if so, is there a proof to show the validity of the statement?
 A: This seems like something that would be in the literature somewhere, but I couldn't find a reference, so here's a proof outline. I'll sketch how to get multivalued Cauchy real from Dedekind, generalised Cauchy from multivalued Cauchy and Dedekind from generalised Cauchy. It follows that all three are equivalent. In order for this to work, the multivalued Cauchy condition on a multivalued function $C$ from $\mathbb{N}$ to $\mathbb{Q}$ needs to be that there is $N$ with $|x - y| < \epsilon$ for all $x \in C(n)$, $y \in C(m)$ with $n, m > N$ (not some $x, y$ like on the nlab page).
It follows directly from the definition of Dedekind cut that Dedekind real numbers are located and bounded. If $x$ is a Dedekind real number, there are rational numbers $p, q$ such that $p < x < q$. By induction on natural numbers $n > 1$, using locatedness, we can show that for all $n$ there merely exists a rational number $r$ such that $|x - r| < |p - q| 2^{-n}$. Hence if $x$ is a Dedekind real number, then for all $n$ the set $C(n) := \{ q \in \mathbb{Q} \;|\; x - 2^{-n} < q < x + 2^{-n}\}$ is merely inhabited. Note that $C$ defines a multivalued Cauchy sequence.
Now given any multivalued Cauchy sequence $C$ we can define a generalised real number as follows. The coproduct $\sum_{n \in \mathbb{N}} C(n)$ is a directed set taking $(n, p) \leq (m, q)$ when $n \leq m$. The second projection followed by inclusion $C(n) \hookrightarrow \mathbb{Q}$ defines a net on this directed set. This is a generalised Cauchy real number.
Finally, given any generalised Cauchy number, say $(q_i)_{i \in I}$, we define a Dedekind real as follows. We take the left cut $L$ to be those $p \in \mathbb{Q}$ such that there exists $r > p$ and $j \in I$ such that $q_i \geq r$ for all $i \geq j$. We similarly define the right cut $R$ by reversing the ordering relations in the above.
