analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A construction (UFP13, Sec. 11.3) of the type of real numbers in homotopy type theory as a higher inductive-inductive type.
As opposed to the “naive” quotient type of regular Cauchy sequences of rational numbers (i.e. the quotient type of the setoid/Bishop set by which the Cauchy real numbers are traditionally modeled in constructive analysis) this higher inductive-inductive type is sequentially modulated Cauchy complete.
Notice that this crucial property of the real number fails for other constructions:
The quotient type of regular Cauchy sequences of rational numbers is Cauchy complete only assuming that any sequence of its terms has a lift to a sequence of representing Cauchy sequences, which requires an extra axiom of countable choice (and is the reason why traditional Bishop-constructive analysis does not pass to the quotient but stays with the setoid/Bishop set).
The modulated Cauchy real numbers are not sequentially modulated Cauchy complete either, in constructive mathematics.
Let $K$ be an Archimedean ordered field. $K$ is sequentially modulated Cauchy complete if every Cauchy sequence in $K$ with a modulus of convergence converges. The set of HoTT book real numbers $\mathbb{R}_H$ is the initial object in the category of sequentially modulated Cauchy complete Archimedean fields.
More abstractly, let $\mathrm{ArchiFields}$ be the category of Archimedean ordered fields and Archimedean ordered field homomorphisms, and let $F:\mathrm{ArchiFields} \to \mathrm{ArchiFields}$ be the endofunction which takes an Archimedean ordered field $K$ to the Archimedean ordered field $F(K)$ which is the quotient set of the set of Cauchy sequences in $K$ with a modulus of convergence. $K$ is sequentially modulated Cauchy complete if there is an isomorphism $K \cong F(K)$, and the HoTT book real numbers $\mathbb{R}_H$ is the initial Archimedean ordered field with an isomorphism $\mathbb{R}_H \cong F(\mathbb{R}_H)$.
The set of HoTT book real numbers $\mathbb{R}_H$ is the initial object in the category of Cauchy structures and Cauchy structure homomorphisms.
As a higher inductive-inductive type:
Let $\mathbb{Q}$ be the rational numbers and let
be the positive rational numbers. The HoTT book real numbers $\mathbb{R}_H$ are inductively generated by the following:
a function $inj: \mathbb{Q} \to \mathbb{R}_H$
a function $lim: C(\mathbb{R}_H) \to \mathbb{R}_H$, where $C(\mathbb{R}_H)$ is the type of Cauchy approximations in $\mathbb{R}_H$.
a dependent family of terms
and the premetric type family $\sim$ is simultaneously inductively generated by the following:
a dependent family of terms
a dependent family of terms
a dependent family of terms
a dependent family of terms
a dependent family of terms
The analytic functions, such as the exponential function, the sine function, and the cosine function are well defined in the HoTT book real numbers, since all modulated Cauchy sequences converge in the HoTT book real numbers.
Survey and review:
Andrej Bauer, The real numbers in homotopy type theory, talk at Computability and Complexity in Analysis, Faro (2016) [pdf, pdf]
Auke Booij, Analysis in Univalent Type Theory (2020) [etheses:10411, pdf, pdf]
Last revised on April 2, 2023 at 00:51:28. See the history of this page for a list of all contributions to it.