Skip to Main content Skip to Navigation
Conference papers

Formalising Real Numbers in Homotopy Type Theory

Gaëtan Gilbert 1, 2 
2 ASCOLA - Aspect and Composition Languages
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. In this case, the limit of a Cauchy sequence of Cauchy reals is defined through lifting it to a sequence of Cauchy sequences of rationals. This lifting requires the axiom of countable choice or excluded middle, neither of which is available in homotopy type theory. To address this, the Univalent Foundations Program uses a higher inductive-inductive type to define the Cauchy reals as the free Cauchy complete metric space generated by the rationals. We generalize this construction to define the free Cauchy complete metric space generated by an arbitrary metric space. This forms a monad in the category of metric spaces with Lipschitz functions. When applied to the rationals it defines the Cauchy reals. Finally, we can use Altenkirch and Danielson (2016)'s partiality monad to define a semi-decision procedure comparing a real number and a rational number.
Document type :
Conference papers
Complete list of metadata

Cited literature [3 references]  Display  Hide  Download
Contributor : Gaëtan Gilbert Connect in order to contact the contributor
Submitted on : Monday, January 30, 2017 - 12:40:01 PM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM


Publisher files allowed on an open archive



Gaëtan Gilbert. Formalising Real Numbers in Homotopy Type Theory. 6th ACM SIGPLAN Conference on Certified Programs and Proofs , Jan 2017, Paris, France. pp.112 - 124, ⟨10.1145/3018610.3018614⟩. ⟨hal-01449326⟩



Record views


Files downloads