What a number is for, not what it is
You already know what a number is — or you feel like you do. This book turns on a different and more useful question: not what a number is, but what it is for.
Think back over the number systems you were handed, one at a time, and notice why each new one showed up. You start with the counting numbers, which are all you need until you try to take 3 − 5 and fall off the bottom. So the negatives get invented, and now subtraction always works. Then 1 ÷ 2 falls between the whole numbers, and the fractions get invented, and now division always works. Then √2 isn't any fraction, and the irrationals fill the gaps. Then √−1 isn't anywhere on the line at all, and the imaginary numbers appear.
Every rung of that ladder is the same move. An operation you already trusted — subtracting, dividing, taking a root — ran off the edge of the numbers you had. And instead of banning the operation, we widened the world until the operation fit back inside it. The numbers didn't come first and the operations second. It was the other way around: the operations were the pressure, and each new kind of number was what had to exist to relieve it.
So ask what actually distinguishes those systems from one another. It is tempting to say they contain different kinds of stuff — but that is not the working difference. The working difference is which operations you can perform without falling out. You can subtract freely in the integers and not in the counting numbers; you can divide freely in the fractions and not in the integers. A number system is pinned down not by what its members look like but by the operations it is closed under.
That is the definition this book runs on.
It is a small shift in wording and a large shift in stance. The usual order is: here are the objects, and here is what you may do to them. The order here is reversed: here are the operations we refuse to let fail, and the type is whatever must exist to keep them working. "What a number is for" comes first; "what a number is" is downstream of it.
One thing to settle before we build on this, because the reframing can sound like a challenge to something it isn't. Classical type theory — the kind that underpins proof assistants and modern foundations — is powerful precisely because it multiplies types: finer distinctions, exact bounds, which theorems apply to which objects, what belongs to which group. None of that is being corrected or thrown out here.
Nearly everything in this book is prior art — known mathematics — looked at from a different angle. The claim is never that the operational view is more true, only that it is a different lens on the same objects, and that for some readers and some problems it makes the picture click in a way the usual framing doesn't. The goal is to add a perspective to the shared understanding of mathematics, not to unseat one. Where something genuinely new is being said, it will be marked plainly; most of the time we are re-describing what is already known, and the whole value is in the re-description.
Reversing the order has a consequence that is easy to say and surprisingly hard to sit with. If a value's job is to keep operations total and reversible, then a value does not have to be a tidy number on a line — it only has to carry whatever is needed to do that job. Some of the most important values in this book will not look like numbers at all. That is not a bug to be explained away; it is the direct result of the definition above, and it is the very next thing we need to make peace with.