# On the HoTT Cauchy Reals

In the Homotopy Type Theory Book there is a construction given of a kind of Cauchy reals via higher inductive type and the authors remarked, that this construction is preferred to other notions (reals as a setoid, some amount of choice, dedekind reals). I would like to have some general information on this subject:

1. Can someone explain in layman's terms (without assuming any knowledge of type theory, let alone homotopy type theory) what the general intuition behind this structure is and how it relates to other approaches to analysis (e.g. Classical, Bishop, Robinson Non-standard, Smooth differential, Computable, etc.)?
2. Is anybody really (substantially) working with these Cauchy reals? Again in relation to other kinds of analysis: Are there reasons to believe that this is really an important structure (not "just" another kind of nonstandard analysis)?

For the first question, I find the most helpful way of thinking about the difference between the Cauchy and Dedekind reals in HoTT to be in terms of their topological structure. If we think of a type in HoTT as a space, then the type of Dedekind reals is the space of reals equipped with its standard topological structure. This makes sense, since the standard topological structure of the reals is induced by the intervals that we use to define Dedekind reals, so we put that topological information in when we constructed them. The Cauchy reals, on the other hand, are the reals equipped with the discrete topology. Since the HIT of the Cauchy reals includes a propositional truncation, we're eliminating the topological information that comes from the Cauchy sequences in the definition. This interpretation also makes sense of Lemma 11.4.1 in the HoTT Book. We always expect a (continuous) function $\mathbb{R}_{c} \to \mathbb{R}_{d}$, since every function out of a discrete topological space is continuous. However, we only expect a (continuous) function going the other way when we have extra information that lets us "break" the continuity restriction, which is what Eq. 11.4.2 of the HoTT Book does. All this can be made precise using cohesive HoTT, where $\mathbb{R}_{c} = \flat\mathbb{R}_{d}$. But we're looking to stick with a layman's explanation.