Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

TL;DR

This paper formalizes the construction of real numbers in Homotopy Type Theory using Cubical Agda, avoiding traditional compromises and enabling machine-assisted constructive analysis.

Contribution

It provides a formal, executable implementation of HoTT's real numbers in Cubical Agda, eliminating the need for postulates or universe-level adjustments.

Findings

Code type-checks without postulates or holes

Provides a foundation for machine-assisted constructive analysis

Avoids classical and setoid construction compromises

Abstract

Real numbers in constructive mathematics have always seemed to require compromises of one form or another. Classical proofs of Cauchy completeness require countable choice, Bishop's setoid construction introduces persistent bookkeeping overhead on every definition and theorem, and Dedekind cuts force cumbersome universe-level tracking in predicative type theory. The Homotopy Type Theory (HoTT) book presents an alternative construction of the Cauchy real numbers as a higher inductive-inductive type family, avoiding all three compromises. We formalize the HoTT book reals in Cubical Agda, a proof assistant whose native support for higher inductive types allows the construction to be expressed directly. The code type-checks without postulates or holes, providing a foundation for further machine-assisted work in constructive analysis.