Types, constructors, and propositions-as-types: proving a theorem is the same as building an element
Type theory is not a pile of axioms but a game: the positions are judgments, the moves are rules, and everything you assert you had to build. Even logic comes for free — a proposition is a type, and a proof is an element of it.
Step the recursor gear by gear and watch double(2) unfold into four. Then try n + 1 = 1 + n and see why computation alone cannot prove it.
double(0) :≡ 0 double(succ(n)) :≡ succ(succ(double(n)))
Every type in the theory arrives the same way. Formation: how to name the type. Constructors: how to build its elements — and, crucially, these are the only ways elements arise. Eliminator: how to use an arbitrary element, by explaining what to do with each constructor. Computation rule: when the eliminator meets a constructor, it actually computes. And sometimes a uniqueness principle, saying every element might as well have come from a constructor.
That is the whole game. Pairs, numbers, functions, and eventually circles and spheres are all instances of one template. Functions themselves are primitive: a function is a machine λx. Φ, and applying it to an argument substitutes and simplifies — the rule called β-reduction. No graphs of ordered pairs anywhere.
The machine above shows the first kind: judgmental equality, written ≡. It holds by definition — double(2) ≡ 4 because the computation rules grind one expression into the other, and no insight, argument, or citation is involved. The system checks it mechanically, the way a calculator checks nothing.
The second kind is propositional equality: a = b is a type, and to assert it you must construct an element of that type — a proof. The statement n + 1 = 1 + n is the classic border case. It is true for every n, but the recursor for addition peels succ off only its first argument, so the two sides do not compute to a common form for a variable n. You need induction: an actual proof object, built by hand.
Hold on to this distinction — it is the hinge of the whole subject. Judgmental equality is invisible bookkeeping. Propositional equality is a type, and things of the same type have structure: elements, maps, and — as the rest of this module shows — the geometry of paths.
Click through the English proof and watch each sentence fill a hole □ in the term. Then try the converse and find the hole nothing can fill.
If A is refutable and B is refutable, then “A or B” is refutable.
□Here is the move that makes type theory a foundation rather than a programming curiosity. Read each proposition as a type — the type of its evidence — and every logical connective turns out to be a type former you already have:
| Proposition | Type |
|---|---|
| True | 𝟙 (the unit type) |
| False | 𝟘 (the empty type) |
| A and B | A × B |
| A or B | A + B |
| A implies B | A → B |
| not A | A → 𝟘 |
| for all x, P(x) | Π(x : A) P(x) |
| there exists x with P(x) | Σ(x : A) P(x) |
Proving a theorem now means building an element of the corresponding type — mathematics and programming become the same activity. But the logic you get is constructive, and that changes what “or” means. An element of A + B is inl(a) or inr(b): it carries the information of which side holds. You cannot prove a disjunction by showing that both sides failing would be absurd; you must deliver a side. That is why one direction of De Morgan’s law goes through below and the other jams.
A type family hangs one type over each point, like fibers over a base. Toggle the views, and drag to thread your own dependent function through the fibers.
Spot a mistake or have an idea?