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)?

John explained one way of thinking about the difference, constructively, between Cauchy and Dedekind reals. What's new about the Cauchy reals in the HoTT Book is that, unlike the usual definition of Cauchy reals in constructive mathematics, they are Cauchy complete in that every Cauchy sequence of Cauchy reals converges. It may be surprising that the usual definition is insufficient to ensure this; the point is that as usually defined, each Cauchy real is an equivalence class of Cauchy sequences of rationals, so if you have a Cauchy sequence of Cauchy reals you have to choose a representing Cauchy sequence for each term in it before you can "diagonalize" to find a limit, and in general that requires countable choice. The HIT Cauchy reals circumvent this problem by "doing the quotienting at the same time as the generation by Cauchy sequneces"; you can sort of think of it as iteratively adding limits of new Cauchy sequences mutually-recursively with passing to equivalence classes of Cauchy sequences.

To my knowledge, no one has yet pursued this notion of Cauchy real number further.


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.

I don't know whether anyone is substantially working with the Cauchy reals in HoTT. In the usual foundations the Cauchy and Dedekind constructions coincide, but this relies on the axiom of (countable) choice. If we're thinking internally, then the Cauchy reals should pop up whenever we're working with the real numbers as a set, without the usual topology.

  • 2
    $\begingroup$ It's not the propositional truncation in the Cauchy reals that makes them topologically discrete; the type of Cauchy sequences is already discrete. See Theorem 8.24 in arxiv.org/abs/1509.07584. $\endgroup$ – Mike Shulman Jun 11 '16 at 9:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.