Types, constructors, and propositions-as-types: proving a theorem is the same as building an element
Set theory is a pile of axioms: assertions, dropped from above, about a single membership relation. Type theory is not like that. It is a game — the positions are judgments like “a is an element of the type A”, and the moves are rules for getting new judgments from old ones. There are no axioms at all in the basic system. Everything you can assert, you can assert because you built it, and everything you build computes.
Remarkably few rules are needed, and they all follow one rhythm. Every type is introduced by the same five-part pattern; functions are primitive machines rather than sets of pairs; and — the payoff of this lesson — logic does not have to be added on top. A proposition simply is a type, and proving it simply is constructing one of its elements. This page is the minimum type theory the rest of the module stands on.
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 computation rules are not metaphors — they run. Step the ℕ-recursor gear by gear and watch double(2) unfold into succ(succ(succ(succ(0)))), watch if-then-else turn out to be the Bool eliminator, and watch what goes wrong with an equation the recursor cannot produce.
double(0) :≡ 0 double(succ(n)) :≡ succ(succ(double(n)))
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.
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 De Morgan law, proved the type-theoretic way. Click through the English proof on the left and watch each sentence fill a hole □ in the growing term on the right — assumptions become λs, case analysis forks a hole, applications close them. Then switch tabs and try the converse, which every classical logician believes, and find the hole that nothing can fill.
If A is refutable and B is refutable, then “A or B” is refutable.
□The dictionary’s last two rows — Π and Σ — deserve a picture, because it is the picture the whole module runs on. A type family B : A → 𝒰 hangs one type over each point of A, like fibers over a base. Here the family is Fin(n + 1), the finite types. Toggle the three views, and in the sections view drag to thread your own dependent function through the fibers.