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