Formalising Real Numbers in Homotopy Type Theory

TL;DR

This paper formalizes the construction of Cauchy reals within homotopy type theory using higher inductive types, avoiding classical axioms, and implements it in Coq, enabling semi-decision procedures for real-rational comparisons.

Contribution

It generalizes the construction of Cauchy reals as a free Cauchy complete metric space to arbitrary metric spaces within homotopy type theory, formalized in Coq.

Findings

Defines Cauchy reals as a monad in metric spaces

Constructs a semi-decision procedure for real-rational comparison

Formalization available in Coq proof assistant

Abstract

Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. 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. The entire construction has been formalized in the Coq proof assistant. It is available at https://github.com/SkySkimmer/HoTTClasses/tree/CPP2017 .