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 … constructive mathematics, realizability, computability propositions as types, proofs as programs, computational trinitarianism topos, homotopy topos type theory, homotopy type theory canonical form, univalence Bishop set, h-set decidable equality, decidable subset, inhabited set, subsingleton 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...