The real numbers and Conway’s surreals rebuilt as data types — the foundation Conway asked for in 1976
Turn the machinery of higher inductive types on the number systems themselves. Declaring what exists and when two things are equal, in one definition, builds the reals, the surreals, and a world where isomorphic groups are equal.
Ask for a precision and watch the funnel close on a point. Then tighten the tolerance until two approximations fuse into one real number.
A real number is one of two things: a rational, or the limit of a Cauchy approximation — a function that, for any precision you name, hands you a rational that close to the answer. And then a path constructor settles equality up front: two reals are equal when they are within epsilon of each other for every epsilon. No quotient afterwards, no axiom of countable choice needed to climb back out of one. What you get is the free complete metric space on the rationals, and the construction is new enough that it was unfamiliar to classical mathematicians too.
The recursion principle is the part that will feel familiar to anyone who has taken analysis. To define a function on the reals you give its values on rationals, give its behaviour on limits, and check that it respects closeness. That is precisely the old slogan — define it on the rationals and extend by continuity — except it has stopped being advice about how to organize a proof and become the literal elimination rule of the type.
Scrub through the days and watch the surreal numbers be born. Then jump past every finite day to meet omega.
One construction, one number system: the dyadic fractions arrive on finite days, every real number arrives by day ω, and the infinite ordinals keep going after that — the reals and the ordinals living side by side, with ω − 1 and 1/ω in the gaps between them.
A surreal number is a cut: a pair of collections of numbers born earlier, with everything on the left strictly below everything on the right. That is the entire definition, and it generates an astonishing range. After all the finite days come omega, larger than every integer; one over omega, positive but smaller than every ordinary fraction; omega minus one, which is a perfectly respectable number; and omega over two. The real numbers embed in this system. So do the infinite ordinals. One number line holding both.
Here is where the module closes a loop it opened at the start. In 1976 Conway observed that every set-theoretic formalization of his numbers came out curiously complicated, and said what he actually wanted was a foundation that let you create objects freely and then stipulate what equality means for them. He wrote that down and waited. Higher inductive types are, almost verbatim, the thing he asked for: his habit of defining the numbers first and their equality afterwards is exactly a path constructor, and the quotient he had to hand-roll disappears into the definition.
Match the elements of two presentations of one group, and watch univalence merge them into a single point.
| + | 0 | 1 | 2 | 3 |
|---|---|---|---|---|
| 0 | 0 | 1 | 2 | 3 |
| 1 | 1 | 2 | 3 | 0 |
| 2 | 2 | 3 | 0 | 1 |
| 3 | 3 | 0 | 1 | 2 |
| ∘ | e | r | r² | r³ |
|---|---|---|---|---|
| e | e | r | r² | r³ |
| r | r | r² | r³ | e |
| r² | r² | r³ | e | r |
| r³ | r³ | e | r | r² |
The type of groups has one point per isomorphism class, so every property and construction that can be written down automatically respects isomorphism. Note that V₄ keeps its own point: it has four elements too, but no matching of tables exists — merging is earned by isomorphism, never by size.
The structure identity principle is the general statement behind the last demo: for any reasonable notion of structure — groups, rings, ordered sets, topological spaces — isomorphic instances are equal. It is a theorem, not a convention, and it climbs a level: with the right definition of category, equivalent categories are equal too. The type of groups genuinely has one point per isomorphism class, and so every construction you can express automatically respects isomorphism. You cannot even state a property that distinguishes isomorphic groups.
That is the whole arc in one sentence. Equality became a space rather than a verdict. Univalence widened it until it matched equivalence. Higher inductive types let us declare objects and their equality in the same breath — a circle from one point and one loop, the continuum from three constructors, and a number system in which the reals and the ordinals finally sit on the same line.
See also: Category Theory for universal properties in their own right, Set Theory for the foundation this one is offered as an alternative to, and Real Analysis for the classical continuum.
Spot a mistake or have an idea?