11. Real numbers

Any foundation of mathematics worthy of its name must eventually address the construction of real numbers as understood by mathematical analysis, namely as a completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath archimedeanPlanetmathPlanetmathPlanetmathPlanetmath ordered field. There are two notions of completeness. The one by Cauchy requires that the reals be closed underPlanetmathPlanetmath limits of Cauchy sequencesMathworldPlanetmathPlanetmath, while the stronger one by Dedekind requires closureMathworldPlanetmathPlanetmath under Dedekind cutsMathworldPlanetmath. These lead to two ways of constructing reals, which we study in \autorefsec:dedekind-reals and \autorefsec:cauchy-reals, respectively. In \autorefRD-final-field,\autorefRC-initial-Cauchy-complete we characterize the two constructions in terms of universal propertiesMathworldPlanetmath: the Dedekind reals are the final archimedean ordered field, and the Cauchy reals the initial Cauchy complete archimedean ordered field.

In traditional constructive mathematics, real numbers always seem to require certain compromises. For example, the Dedekind reals work better with power setsMathworldPlanetmath or some other form of impredicativity, while Cauchy reals work well in the presence of countable choice. However, we give a new construction of the Cauchy reals as a higher inductive-inductive type that seems to be a third possibility, which requires neither power sets nor countable choice.

In \autorefsec:comp-cauchy-dedek we compare the two constructions of reals. The Cauchy reals are included in the Dedekind reals. They coincide if excluded middle or countable choice holds, but in general the inclusion might be proper.

In \autorefsec:compactness-interval we consider three notions of compactness of the closed intervalMathworldPlanetmath [0,1]. We first show that [0,1] is metrically compactPlanetmathPlanetmath in the sense that it is complete and totally boundedPlanetmathPlanetmath, and that uniformly continuous maps on metrically compact spaces behave as expected. In contrast, the Bolzano–Weierstraß property that every sequenceMathworldPlanetmathPlanetmath has a convergentMathworldPlanetmathPlanetmath subsequence implies the limited principle of omniscience, which is an instance of excluded middle. Finally, we discuss Heine-Borel compactness. A naive formulation of the finite subcover property does not work, but a proof relevant notion of inductive covers does. This sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath is basically standard constructive analysis.

The development of real numbers and analysis in homotopy type theory can be easily made compatible with classical mathematics. By assuming excluded middle and the axiom of choiceMathworldPlanetmath we get standard classical analysis: the Dedekind and Cauchy reals coincide, foundational questions about the impredicative nature of the Dedekind reals disappear, and the interval is as compact as it could be.

We close the chapter by constructing Conway’s surreals as a higher inductive-inductive type in \autorefsec:surreals; the construction is more natural in univalent type theoryPlanetmathPlanetmath than in classical set theoryMathworldPlanetmath.

In additionPlanetmathPlanetmath to the basic theory of \autorefcha:basics,\autorefcha:logic, as noted above we use “higher inductive-inductive types” for the Cauchy reals and the surreals: these combine the ideas of \autorefcha:hits with the notion of inductive-inductive type mentioned in \autorefsec:generalizationsPlanetmathPlanetmath. We will also frequently use the traditional logical notation described in \autorefsubsec:prop-trunc, and the fact (proven in \autorefsec:piw-pretopos) that our “sets” behave the way we would expect.

Note that the total space of the universal cover of the circle, which in \autorefsubsec:pi1s1-homotopy-theory played a role similar to “the real numbers” in classical algebraic topology, is not the type of reals we are looking for. That type is contractible, and thus equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to the singleton type, so it cannot be equipped with a non-trivial algebraic structurePlanetmathPlanetmath.

Title 11. Real numbers