Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866908996808474624 |
|---|---|
| author | Brough, Jackson |
| author_facet | Brough, Jackson |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_24782 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda Brough, Jackson Logic in Computer Science 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. |
| title | Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2604.24782 |