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