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 complete.
Notice that this crucial property of the real number fails for other constructions:
Let be an Archimedean ordered field. is sequentially complete if every regular Cauchy sequence in converges. The set of HoTT book real numbers is the initial object in the category of sequentially complete Archimedean fields.
More abstractly, let be the category of Archimedean ordered fields and Archimedean ordered field homomorphisms, and let be the endofunction which takes an Archimedean ordered field to the Archimedean ordered field which is the quotient set of the set of regular Cauchy sequences in . is sequentially complete if there is an isomorphism , and the HoTT book real numbers is the initial Archimedean ordered field with an isomorphism .
The set of HoTT book real numbers is the initial object in the category of Cauchy structures and Cauchy structure homomorphisms.
As a higher inductive-inductive type:
Let be the rational numbers and let
be the positive rational numbers. The HoTT book real numbers are inductively generated by the following:
a function
a function , where is the type of rational Cauchy approximations in .
a dependent family of terms
and the premetric type family 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 regular 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 May 13, 2025 at 16:12:17. See the history of this page for a list of all contributions to it.