×

Cauchy-complete real numbers, fully constructive as a HIT

This work comes from a broader open-source collaboration, including the Formal Foundry Research Group, which contributed a substantial part of it.

Presented at TYPES 2026 · 4–8 May 2026 · Gothenburg, Sweden

The work develops Cauchy-complete real numbers constructively in Cubical Agda, using a higher inductive construction. More precisely, the completion is higher inductive-inductive: the numbers and their notion of closeness are built together. This gives us a foundation for proving properties of real numbers and computing with them.

Outline of the work

  • Shared algebraic foundations. Ordered rings provide a common language for integers, dyadic rationals, rationals and reals.
  • From closeness to completion. Premetric spaces and their higher inductive-inductive completion provide a route to Cauchy-complete spaces and the extension of Lipschitz maps.
  • Constructive analysis. The HoTT Book real-number development supports work on continuity, derivatives, integration and elementary functions.

The premetric-space development on GitHub and the conference PDFs contain the definitions and proofs.

Follow-up: computing and plotting

The subsequent cubical-analysis-tools work evaluates real-number expressions inside Agda, starting from the Cubical library’s definitions. It recovers rational approximations from those expressions and exports the results as plots and meshes.

The Takagi examples show the same function at very different scales. Every plotted value comes from computation inside the proof assistant; exporting the results to SVG makes those values visible. The lines connect the computed samples.

The Takagi function on the unit interval, showing its repeated jagged peaks.
The Takagi function 512 samples on [0, 1], computed from the constructive real-number implementation.
The small-scale Takagi residual after subtracting a straight-line trend and rescaling, revealing the same jagged structure.
A deep zoom 128 samples between ½ and ½ + 2⁻⁵⁸, with the straight-line trend removed and the axes rescaled.

From real numbers to the Hopf fibration

The tooling now produces 3D meshes, too. This interactive view shows 24 circle fibers of the Hopf fibration, projected from the three-sphere into ordinary three-dimensional space. Agda computes the coordinates and colors; WebGL displays them. Rotate the view, zoom in, or hide a family to see how the circles fit together.

Three families of eight fibers, with 64 sample points around each circle. The viewer is self-contained and runs in your browser. Open the full viewer in a new tab ↗

Computation in action

This short recording shows rational and decimal approximations being evaluated in Agda, including expressions involving roots and exponentials.

A 30-second, silent demonstration of computation with constructive real numbers. Use the player’s fullscreen control to inspect the expressions.
Skip to content

Papers

Cauchy-complete real numbers, fully constructive as a HIT

This work comes from a broader open-source collaboration, including the Formal Foundry Research Group, which contributed a substantial part of it.

Presented at TYPES 2026 · 4–8 May 2026 · Gothenburg, Sweden

The work develops Cauchy-complete real numbers constructively in Cubical Agda, using a higher inductive construction. More precisely, the completion is higher inductive-inductive: the numbers and their notion of closeness are built together. This gives us a foundation for proving properties of real numbers and computing with them.

Outline of the work

  • Shared algebraic foundations. Ordered rings provide a common language for integers, dyadic rationals, rationals and reals.
  • From closeness to completion. Premetric spaces and their higher inductive-inductive completion provide a route to Cauchy-complete spaces and the extension of Lipschitz maps.
  • Constructive analysis. The HoTT Book real-number development supports work on continuity, derivatives, integration and elementary functions.

The premetric-space development on GitHub and the conference PDFs contain the definitions and proofs.

Follow-up: computing and plotting

The subsequent cubical-analysis-tools work evaluates real-number expressions inside Agda, starting from the Cubical library’s definitions. It recovers rational approximations from those expressions and exports the results as plots and meshes.

The Takagi examples show the same function at very different scales. Every plotted value comes from computation inside the proof assistant; exporting the results to SVG makes those values visible. The lines connect the computed samples.

The Takagi function on the unit interval, showing its repeated jagged peaks.
The Takagi function 512 samples on [0, 1], computed from the constructive real-number implementation.
The small-scale Takagi residual after subtracting a straight-line trend and rescaling, revealing the same jagged structure.
A deep zoom 128 samples between ½ and ½ + 2⁻⁵⁸, with the straight-line trend removed and the axes rescaled.

From real numbers to the Hopf fibration

The tooling now produces 3D meshes, too. This interactive view shows 24 circle fibers of the Hopf fibration, projected from the three-sphere into ordinary three-dimensional space. Agda computes the coordinates and colors; WebGL displays them. Rotate the view, zoom in, or hide a family to see how the circles fit together.

Three families of eight fibers, with 64 sample points around each circle. The viewer is self-contained and runs in your browser. Open the full viewer in a new tab ↗

Computation in action

This short recording shows rational and decimal approximations being evaluated in Agda, including expressions involving roots and exponentials.

A 30-second, silent demonstration of computation with constructive real numbers. Use the player’s fullscreen control to inspect the expressions.
Download paperOpen the source PDF

Cabinet index

Explore Formal Foundry

Book a meeting Explore libraries

info@formalfoundry.aiTrusted systems. Mathematical proofs.

Search the archive

Find a page

Type to search the published content.