arxiv: 2604.24782 · v1 · submitted 2026-04-23 · 💻 cs.LO

Recognition: unknown

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

Jackson Brough

Authors on Pith no claims yet

Pith reviewed 2026-05-08 13:40 UTC · model grok-4.3

classification 💻 cs.LO

keywords real numbershomotopy type theorycubical agdaconstructive mathematicshigher inductive typescauchy realsformalization

0 comments

The pith

The HoTT book's Cauchy real numbers are fully formalized in Cubical Agda with no postulates or holes.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that the higher inductive-inductive construction of the real numbers from the Homotopy Type Theory book can be expressed directly in Cubical Agda. This approach sidesteps the countable choice required in classical Cauchy completeness proofs, the bookkeeping overhead of Bishop setoids, and the universe-level tracking demanded by Dedekind cuts in predicative settings. Because Cubical Agda supports higher inductive types natively, the entire construction type-checks without any axioms or incomplete terms. The resulting library supplies a machine-verified foundation that supports further formal work in constructive analysis.

Core claim

The Cauchy real numbers defined in the HoTT book as a higher inductive-inductive type family have been implemented in Cubical Agda; the complete formalization type-checks without postulates or holes and thereby supplies a foundation for machine-assisted constructive analysis.

What carries the argument

The higher inductive-inductive type family for the Cauchy reals, which directly encodes the numbers together with their field operations, order, and completeness properties.

If this is right

Machine-checked proofs of basic analytic facts about the reals become possible without extra axioms.
Further developments in constructive analysis can reuse the same inductive structure without reintroducing bookkeeping or choice principles.
The same direct encoding can serve as a base for formalizing additional number systems or metric spaces in Cubical Agda.
Developers gain a concrete, executable reference implementation of the HoTT reals for testing new definitions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The formalization could be extended to include integration or differential equations while preserving constructivity.
Similar higher-inductive constructions might be used to formalize other classically non-constructive objects inside type theory.
The library opens the possibility of extracting verified numerical algorithms directly from the type-theoretic definitions.

Load-bearing premise

The higher inductive-inductive construction given in the HoTT book correctly encodes the properties of the real numbers required for analysis.

What would settle it

A failure of the formalized type to satisfy Cauchy completeness or to type-check in Cubical Agda would refute the claim that the construction works as a foundation.

Figures

Figures reproduced from arXiv: 2604.24782 by Jackson Brough.

**Figure 3.1.** Figure 3.1: The higher inductive-inductive definition of the HoTT book reals and the close view at source ↗

**Figure 3.2.** Figure 3.2: A prompt given to Claude Code during the development of the reciprocal con view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper delivers a clean, axiom-free Cubical Agda encoding of the HoTT book's higher inductive-inductive reals that type-checks as stated.

read the letter

The key thing to know is that the authors transcribed the HoTT reals construction directly into Cubical Agda and got it to type-check without postulates or holes. Cubical Agda's native HIT support makes this a faithful copy of the book's definition rather than a workaround, which is the main technical achievement here. It is new in the sense that no prior report exists of this exact encoding in this system, though similar formalizations have appeared in other proof assistants or with different real-number constructions. The work does well by giving a concrete, usable base layer for constructive analysis that avoids countable choice and setoid overhead, exactly as the HoTT book intended. That supplies a foundation others can extend without starting from scratch. The soft spots are modest and expected for a formalization paper. The contribution is mostly the artifact itself; the manuscript does not appear to prove many new theorems on top of the reals or run extensive comparisons against other libraries. Impact therefore hinges on whether people actually build analysis on this code. Type-checking is solid evidence of soundness, but it still leaves open the question of whether the HoTT construction matches what working analysts need in practice. This paper is for people already working in homotopy type theory or formal verification of analysis who want a verified reals library in Cubical Agda. A reader looking for a starting point to do machine-checked constructive math will get immediate value from the code. It deserves a serious referee because clean, reproducible formalizations like this are the kind of incremental infrastructure the field needs, even when they are not mathematically novel. I would send it to peer review so the community can check the encoding details and assess its extensibility.

Referee Report

0 major / 2 minor

Summary. The manuscript presents a direct formalization in Cubical Agda of the higher inductive-inductive Cauchy real numbers construction given in the Homotopy Type Theory book. The authors state that the implementation type-checks without postulates or holes and thereby supplies a verified foundation for further machine-assisted work in constructive analysis.

Significance. If the formalization is faithful, the result is significant because it delivers a machine-checked transcription of a construction that achieves Cauchy completeness without countable choice and without the persistent bookkeeping of Bishop setoids. Cubical Agda's native HIT support makes the encoding a faithful rendering of the book's definition; the absence of postulates or holes therefore constitutes direct evidence that the intended properties are preserved. This supplies a concrete, reproducible base for verified constructive analysis in homotopy type theory.

minor comments (2)

The manuscript would be strengthened by an explicit statement of the precise Cubical Agda version and a permanent link (e.g., GitHub commit hash) to the source files, allowing readers to reproduce the type-checking claim independently.
A short table or paragraph summarizing which of the HoTT-book lemmas (e.g., the universal property of the reals or the embedding of rationals) have been proved in the formalization, and which remain as future work, would improve clarity.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending acceptance. We appreciate the recognition that a direct, postulate-free formalization of the HoTT Cauchy reals supplies a verified foundation for constructive analysis.

Circularity Check

0 steps flagged

Direct formalization of independent HoTT-book construction

full rationale

The paper's claimed result is a faithful transcription of the higher inductive-inductive Cauchy reals from the independently authored HoTT book into Cubical Agda, with the sole verification step being successful type-checking without postulates or holes. This verification is performed by the external proof assistant and does not involve any equations, parameters, or theorems derived inside the paper itself. No load-bearing step reduces to a self-definition, a fitted input renamed as prediction, or a self-citation chain; the HoTT book reference supplies the external construction being encoded. The work is therefore self-contained against external benchmarks and exhibits no circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the correctness of the HoTT book's higher inductive-inductive reals and on the soundness of Cubical Agda's native support for such types; no new free parameters or invented entities are introduced.

axioms (1)

domain assumption The HoTT book construction of Cauchy reals via higher inductive-inductive types is a valid definition of the reals in constructive mathematics.
The paper directly implements the construction given in the HoTT book.

pith-pipeline@v0.9.0 · 5412 in / 1108 out tokens · 58656 ms · 2026-05-08T13:40:00.734421+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

15 extracted references · 6 canonical work pages

[1]

Institute for Advanced Study, 2013

The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for Advanced Study, 2013. [Online]. A vailable: https : / / homotopytypetheory.org/book

2013
[2]

Bishop, Foundations of Constructive Analysis (McGraw-Hill Series in Higher Math- ematics)

E. Bishop, Foundations of Constructive Analysis (McGraw-Hill Series in Higher Math- ematics). New York: McGraw-Hill, 1967. [Online]. A vailable: https://lccn.loc.gov/ 67022952

1967
[3]

Formalising real numbers in homotopy type theory,

G. Gilbert, “Formalising real numbers in homotopy type theory,” in Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs , ser. CPP 2017, Paris, France: Association for Computing Machinery, 2017, pp. 112–124, isbn: 9781450347051. doi: 10.1145/3018610.3018614 [Online]. A vailable: https://doi. org/10.1145/3018610.3018614

work page doi:10.1145/3018610.3018614 2017
[4]

A monadic, functional implementation of real numbers,

R. O’Connor, “A monadic, functional implementation of real numbers,” Mathematical. Structures in Comp. Sci. , vol. 17, no. 1, pp. 129–159, Feb. 2007, issn: 0960-1295. doi: 10 . 1017 / S0960129506005871 [Online]. A vailable: https : / / doi . org / 10 . 1017 / S0960129506005871

2007
[5]

Cubical agda: A dependently typed program- ming language with univalence and higher inductive types,

A. Vezzosi, A. Mörtberg, and A. Abel, “Cubical agda: A dependently typed program- ming language with univalence and higher inductive types,” Proc. ACM Program. Lang., vol. 3, no. ICFP, Jul. 2019. doi: 10.1145/3341691 [Online]. A vailable:https: //doi.org/10.1145/3341691 94

work page doi:10.1145/3341691 2019
[6]

URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs

N. Kraus, “The General Universal Property of the Propositional Truncation,” in 20th International Conference on Types for Proofs and Programs (TYPES 2014) , H. Her- belin, P. Letouzey, and M. Sozeau, Eds., ser. Leibniz International Proceedings in In- formatics (LIPIcs), vol. 39, Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015, ...

work page doi:10.4230/lipics 2014
[7]

Inductive-inductive definitions,

F. Nordvall Forsberg, “Inductive-inductive definitions,” Ph.D. dissertation, Swansea University, 2013. [Online]. A vailable: https : / / cronfa . swansea . ac . uk / Record / cronfa5299

2013
[8]

Analysis in univalent type theory,

A. B. Booij, “Analysis in univalent type theory,” Ph.D. dissertation, University of Birmingham, 2020. [Online]. A vailable: https://etheses.bham.ac.uk/id/eprint/ 10411/

2020
[9]

Mines, F

R. Mines, F. Richman, and W. Ruitenburg, A Course in Constructive Algebra (Uni- versitext). Springer New York, 2012, isbn: 9781441986405

2012
[10]

30, 2025

The Agda Community, Cubical Agda library, version 0.9, Jul. 30, 2025. [Online]. A vail- able: https://github.com/agda/cubical

2025
[11]

[Online]

Anthropic, Claude code, 2025. [Online]. A vailable:https://github.com/anthropics/ claude-code

2025
[12]

Partiality, revisited,

T. Altenkirch, N. A. Danielsson, and N. Kraus, “Partiality, revisited,” in Proceedings of the 20th International Conference on Foundations of Software Science and Compu- tation Structures - Volume 10203 , Berlin, Heidelberg: Springer-Verlag, 2017, pp. 534– 95 549, isbn: 9783662544570. doi: 10.1007/978-3-662-54458-7_31 [Online]. A vailable: https://doi.org...

work page doi:10.1007/978-3-662-54458-7_31 2017
[13]

A cubical path from algebra to analysis,

L. Molena, M. J. Turek-Grzybowski, and R. Borsetto, “A cubical path from algebra to analysis,” in 31st International Conference on Types for Proofs and Programs (TYPES 2026), To appear, 2026

2026
[14]

Real numbers and other completions,

F. Richman, “Real numbers and other completions,” Mathematical Logic Quarterly , vol. 54, no. 1, pp. 98–108, Jan. 2008. doi: 10.1002/malq.200710024 [Online]. A vail- able: https://doi.org/10.1002/malq.200710024

work page doi:10.1002/malq.200710024 2008
[15]

Constructive analysis in the Agda proof assistant,

Z. Murray, “Constructive analysis in the Agda proof assistant,” Honours Bachelor’s thesis, Dalhousie University, 2022. [Online]. A vailable: https : / / arxiv . org / abs / 2205.08354 Name of Candidate: Jackson Brough Date of Submission: April 17, 2026

work page arXiv 2022