State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

Question

I don't think a particular choice of such type theory matters much. Extensional MLTT, SetoidTT, OTT, HoTT, HOTT, CuTT -- they all support quotient types. Reals is supposed to be a Set (in HoTT terminology) so in all "higher" type-theories we just add in truncations to the HIT signature representing Reals to collapse the higher structure.

So what's the general well-established state-of-the-art here, if there is one, in a constructive setting?

Answer 1

Here are some formalizations of constructive reals that you can build on, roughly by decreasing level of "state-of-the-art". Some come equipped with a considerable amount of real analysis, which you can then help improve (rather than formalize everything from scratch):

1. Good old C-CoRN, a large Coq library of reals, algebra and analysis, based on setoids.
2. If you follow the work of Assia Mahboubi, Cyril Cohen and their coworkers, for example Formally Verified Approximations of Definite Integral and Formalization Techniques for Asymptotic Reasoning in Classical Analysis, you will find how world-experts approach formalization of analysis. (Do not dismiss some of this work just because it says it's "classical". Their approach is equally useful for constructive analysis.)
3. UniMath has a section on Dedekind reals which goes some way. It flirts with excluded middle but stops short of going to bed with it.
4. dedekind-reals, a construction of Dedekind reals in Coq with proof that they form an ordered Dedekind-complete archimedean field, and a lattice.
5. Agda standard library has a definition of Cauchy reals but nothing about their structure (as far as I can tell).
6. agda-unimath has a definition of Dedekind cuts but not much more than that.

In addition to consulting formalizatins of reals, one should also consult constructive literature. Not all constructive approaches are equally suited for formalization. For instance, Bishop's definition of Cauchy reals (which can be found in Agda's standard library) is not that practical. In general, abstract approaches tend to formalize well – this is a general feature of formalized mathematics.

Answer 2

First off, you need to distinguish between constructing the reals and defining the reals. Your question asks about the former, but:

• Classically we almost never simply construct two versions of reals and then prove they are isomorphic. What we do is we prove that our definition of reals already implies that reals are unique, up to (unique) isomorphism. So encodings don't matter that much, it is the definitions that matter.
• Constructing the reals is also a form of defining the reals, because you can always define "it is the reals iff it is isomorphic to this one I've just constructed". So the former is totally encapsulated in the latter, and we can just talk about the latter instead.

Now, we have a slick definition of what counts as a definition of the real numbers. We start with a neutral foundation, i.e. one that cannot prove or disprove the excluded middle. If a definition is equivalent to the classical reals once the excluded middle is added as an axiom, then we say this defines a notion of constructive reals. Note that adding axioms only collapses different notions of reals into one, never bifurcates them.

We immediately see that there are infinitely many versions of real numbers. This is because there are infinitely many propositions $p_i$ that are true in classical mathematics, but pairwise unprovable to be equivalent. So take the definition "A type/set is the reals if and only if $p_i$ holds and [insert the rest of the real axioms]", and you get an infinite supply of reals.

For the concrete discussion, I have nothing to add to the nLab entry.

There is one more thing I would like to point out in your question. It is not true that higher inductive types have nothing to contribute in the construction of reals, even when there are quotient types. In fact, the HoTT book gave a construction (referred to as the "HoTT reals") that is not a simple set quotient. If you insist on describing it with quotients, then consider the rationals $R_0 = \mathbb Q$, consider all the Cauchy sequences, and quotient it by an equivalence, giving $R_1 = \mathrm{Cauchy}(R_0)/\approx_0$. Now this is not Cauchy complete unless you assume some choice. So you complete it again, giving $R_2 = \mathrm{Cauchy}(R_1)/\approx_1$, and so on, giving $R_\omega = \bigcup_{k=0}^{\infty} R_k$. This is still not complete unless you assume some choice. So you do it again getting $R_{\omega+1}, R_{\omega+2}, \dots, R_{2\omega}, \dots$ Giving an infinitely ordinal-indexed tower of candidates reals. The HoTT reals just does all this in a single step: it is a higher inductive-inductive type, or quotient inductive-inductive type, which satisfies desirable properties even in the absence of countable choice.