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.
Type de document :
Communication dans un congrès
6th ACM SIGPLAN Conference on Certified Programs and Proofs , Jan 2017, Paris, France. pp.112 - 124, 2017, <10.1145/3018610.3018614>
Liste complète des métadonnées

https://hal.inria.fr/hal-01449326
Contributeur : Gaëtan Gilbert <>
Soumis le : lundi 30 janvier 2017 - 12:40:01
Dernière modification le : jeudi 13 avril 2017 - 11:07:22

Fichiers

p112-gilbert.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

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, 2017, <10.1145/3018610.3018614>. <hal-01449326>

Partager

Métriques

Consultations de
la notice

123

Téléchargements du document

14