Propositions, sets, and groupoids are rungs of one homotopical ladder — and truncation moves you down it
Types differ in how interesting their equalities are, and sorting them by that gives a ladder — the n-types. Classical logic turns out to live on the bottom rung, and fails higher up for reasons you can draw.
Drag each type onto the lowest rung it belongs to. Wrong rungs bounce, with an explanation.
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.
Pull the lever to squash three witnesses into one point. Then try to define a function out of the squashed type — Bool jams the machine, a proposition 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.
Click one point in each fiber to build a section. On the twisted bundle the circuit comes back swapped and the section snaps; untwist it and it closes.
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.
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.
Spot a mistake or have an idea?