Propositions, sets, and groupoids are rungs of one homotopical ladder — and truncation moves you down it
Not all types are equally complicated. Some are pure truth values with nothing to say beyond yes or no; some are honest collections of distinct elements; some carry loops, and loops between loops, forever upward. Homotopy type theory organizes this zoo with a single ruler: how interesting are the equality types? Ask that question recursively and a ladder appears — the n-types — starting, oddly enough, at minus two.
The ladder comes with an elevator going down. Truncation flattens any type to a chosen rung, and its bottom floor, propositional truncation, crushes a type to the bare fact of its inhabitation. That one operator is the key to a diplomatic question: how does proof-relevant type theory relate to classical mathematics?
The answer turns out to be a matter of where on the ladder you stand. Stated at the bottom rung, the classical principles — excluded middle, the axiom of choice — are perfectly consistent optional axioms. Stated for all types, excluded middle flatly contradicts univalence, and choice fails for a reason you can draw: a twisted double cover whose fibers are all inhabited but admit no continuous selection.
Rungs from minus two up to two, and a tray of famous types. Drag each type onto the lowest rung it belongs to — wrong rungs bounce, with an explanation — and watch the cumulative bands: every rung contains all the rungs below it.
Drag each type from the tray onto its lowest rung. Wrong rungs bounce.
The translucent bands show the ladder is cumulative: every rung contains the one below it. A set is also a groupoid; a proposition is also a set. Sort all seven types to see the whole hierarchy filled in.
The whole hierarchy is generated by one definition. Start at minus two: a (−2)-type is a contractible type — one point, up to a contractible wiggle. Then recurse upward: a type is an (n+1)-type when all of its path spaces x = y are n-types. That single step produces everything. At minus one sit the mere propositions, types whose elements are all equal — pure truth values, carrying no information beyond “true.” At zero sit the sets: distinct elements allowed, but each equality is itself a mere proposition — a plain yes or no. The natural numbers live here, and provably so: equality of naturals is decidable, and Hedberg’s theorem says decidable equality forces set-ness. At one sit the groupoids, where equalities form sets — and the ladder climbs forever. It is cumulative: every n-type is also an (n+1)-type, so a proposition is a set and a set is a groupoid.
Best of all, the ladder classifies itself. The type of all n-types is an (n+1)-type: the type of propositions is a set, the type of sets is a groupoid. And the universe as a whole is not a set — univalence turns the swap equivalence on Bool into a path Bool = Bool that is different from reflexivity, two genuinely different proofs of one equality. The failure is not a defect; it is the universe honestly reporting how many ways types can be identified.
A type A with three distinct witnesses. Pull the lever to apply propositional truncation ‖−‖ and fuse them into one anonymous point. Then try to define a function out of ‖A‖ by routing the hidden witnesses to a codomain — Bool jams the machine unless the routing is constant; a proposition always goes through.
On the left: a type A with three distinct elements — three genuinely different proofs that A is inhabited. Pull the lever to apply the truncation ‖−‖.
The rule of propositional truncation: you may open the box and use the hidden witness, but only if your answer cannot depend on which witness it was. Maps into propositions always qualify; maps into Bool qualify only when they are constant.
For every rung there is a flattening operator: the n-truncation ‖A‖n is the best approximation of A living at rung n, made by freely gluing in whatever paths are needed to kill the structure above. The workhorse is the bottom case, propositional truncation ‖A‖: glue every pair of elements together and what remains is a mere proposition that remembers only one bit — whether A is inhabited — with every trace of which element erased.
The subtlety is entirely in getting information back out, and the elimination rule is a beautiful bargain: you may open the box and compute with the hidden witness — but only if your answer provably cannot depend on which witness it was. Mapping into a proposition always qualifies, since a proposition has no room to disagree. Mapping into a set like Bool qualifies exactly when the map is constant in the appropriate sense. The squash machine above is this rule made physical: route two hidden witnesses to different booleans and the machine jams, because inside ‖A‖ those witnesses are equal.
Truncation is what reconciles proof-relevant logic with the classical kind. The plain sum A + B and dependent pair Σ carry data — a proof of “or” tells you which side, a proof of “exists” hands you the element. Squash them and you get the classical connectives: A ∨ B is ‖A + B‖, and ∃ is a truncated Σ. With disjunction and existence read this way, propositions form the familiar Boolean-feeling world — classical logic is recovered at the bottom rung of the ladder.
Where you state the classical axioms then becomes everything. Excluded middle for mere propositions — every P is P ∨ ¬P — is a consistent optional axiom; so is the axiom of choice for sets. A mathematician who wants them may simply add them, and the homotopical structure upstairs survives intact. But the untruncated versions die on the ladder. A chooser Π(A : 𝒰) A + ¬A for all types would, transported around the swap loop that univalence installs on Bool, have to pick a fixed point of the swap — and the swap has none. And choice already fails one rung up: over a base that is a genuine 1-type, the twisted double cover below has every fiber inhabited yet admits no section. Classical logic is not wrong here — it is a property of the bottom rung, not of the whole ladder.
A circular base — the space of all two-element types — carrying a two-strand bundle with a half-twist. Sweep around, clicking one point in each fiber to build a section. Every fiber is inhabited, but completing the circuit the strand comes back swapped and the section snaps. Untwist the bundle and the same sweep closes fine.
Each spoke is a fiber with two points. Click one point in the highlighted fiber, then sweep around the circle picking one point per fiber — you are building a section of the bundle.
Every fiber is inhabited — two candidates over every point of the base — yet there is no choice function: no continuous way to pick one point per fiber, because following any strand around the loop brings you back swapped. The axiom of choice fails over this base.
The same twist is why untruncated excluded middle contradicts univalence: a uniform chooser, transported around the swap loop of Bool that univalence puts in the universe, would have to be a fixed point of the swap — and the swap has none.