The Cubical reals and constructive analysis work is the site’s deepest mathematical thread.

The TYPES 2026 work, “A Cubical Path from Algebra to Analysis,” develops constructive analysis in Cubical Agda by moving from algebraic foundations toward analytic structure. It connects pseudolattices, ordered commutative rings, Archimedean rings, premetric spaces, higher inductive-inductive completions, Lipschitz maps, continuity, and HoTT Book Cauchy reals.

Why It Belongs Here

This work is not a direct product. It is credibility for the kind of formalization Formal Foundry claims to do: long, careful, mathematically demanding developments where definitions have to line up across many modules.

The broader Cauchy-real formalization includes work around:

• ordered commutative rings and Archimedean structure;
• rationals and dyadics;
• completions;
• order, reciprocals, apartness, and completeness;
• pointwise and uniform continuity;
• derivatives, limits, chain rule, Rolle’s theorem, and mean value theorem;
• monotonicity criteria;
• Riemann integration with tagged partitions and refinement;
• exponential, trigonometric, roots, and constant-related infrastructure.

How It Fits

This work is best presented as deep formalization capacity rather than a product claim. It gives the site a research-depth thread behind the product and infrastructure pages.

The path from algebra to analysis matters. Real analysis is not one definition; it depends on ordered algebra, rational and dyadic structure, premetric spaces, completion, continuity, derivatives, integration, and many compatibility choices across modules.

Cubical Agda is a natural setting for this work because equality, paths, higher inductive types, and constructive mathematics shape the definitions rather than appearing only after the fact.

The generated Agda HTML includes modules around rationals, ordered rings, Cauchy reals, continuity, Lipschitz maps, derivatives, mean value reasoning, integration, exponentials, roots, trigonometric identities, and constants.

The valuable public claim is precise: Formal Foundry works with Cubical Agda formalization around constructive real analysis, contributing to and using a long, layered path from algebraic foundations toward analysis.