The real numbers and Conway’s surreals rebuilt as data types — the foundation Conway asked for in 1976
We have been building circles and spheres out of generators. Now turn the same machinery on the number systems themselves — and watch a forty-year-old complaint of John Conway’s get answered almost word for word.
The move that makes this possible is the one that has been running through the whole module: a higher inductive type lets you declare what exists and declare what it would mean for two of the things you declared to be the same. Constructing the reals traditionally means building Cauchy sequences and then quotienting, and constructively that quotient is where the trouble lives — recovering representatives from equivalence classes needs a choice principle. Doing both jobs in a single definition dissolves the problem entirely.
Three movements follow. The continuum as a data type; Conway’s surreals, which swallow the real numbers and the infinite ordinals at once; and the closing thought of the module — that with univalence, the space of all groups has exactly one point per isomorphism class, so every construction respects isomorphism whether its author intended that or not.
Three constructors, and the continuum follows. Ask for a precision and the approximation hands back a rational within that distance; keep asking and watch the funnel close on a point that gets welded into the line. Then run two different approximations of the same value side by side and tighten the tolerance until the path constructor fuses them into a single 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. Day zero has only zero; each later day fills the gaps between the numbers already present, so the dyadic fractions arrive in a widening binary tree. Then jump past every finite day at once and meet omega, one over omega, and their neighbours — each shown with the cut that defines it.
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.
Two presentations of the same group that look nothing alike: numbers under addition modulo four, and the rotations of a square. Match the elements to build the isomorphism, then watch what univalence does with it — the two nodes in the space of groups merge into one. Toggle back to the set-theoretic picture to see them stay stubbornly apart.
| + | 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.