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

https://hal.inria.fr/hal-01449326
Contributor : Gaëtan Gilbert <>
Submitted on : Monday, January 30, 2017 - 12:40:01 PM
Last modification on : Wednesday, July 21, 2021 - 7:36:02 AM

Files

p112-gilbert.pdf
Publisher files allowed on an open archive

Identifiers

Citation

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⟩

Share

Metrics

Record views

483

Files downloads

685