A proof that two things are equal is a path between them — and there can be many genuinely different proofs
Read every type as a space and every element as a point. Then a proof that a = b is a path from a to b — and two different routes around a hole are two genuinely different proofs.
Click chips to concatenate, reverse, or reset paths, and a bead walks the proof you built. Then punch a hole and watch p and q become different proofs.
Drag the points a, b, c anywhere in the space. Clicking a path chip selects it; clicking another chip that shares an endpoint concatenates it onto the end (reversed automatically if it points the wrong way), so two clicks build composites like p · q⁻¹. Reverse flips the whole expression, refl drops to the constant path at the start point, and the bead walks the current proof. With the hole punched, p and q are forced around opposite sides — two visibly different proofs that a equals b.
In most of mathematics a proof, once found, is discarded: what survives is the bare fact that the statement is true. Homotopy type theory is proof relevant — the proof is an object in its own right, an inhabitant of the type a =A b, and different inhabitants can carry different information. Every point has the trivial proof of its own equality, the constant path refl. But nothing forces refl to be alone: the identity type may have many points, just as the playground’s space had many routes from a to b once the hole appeared. Because proofs are objects, they too can be compared, and a proof that two proofs agree is again a path — one dimension up. The identity type is not a yes/no verdict; it is a whole space, and its shape records the shape of A.
Pick an expression and a lens, and read the same symbols as logic, sets, spaces, and types.
The space of paths in A from a to b — possibly empty, possibly rich.
One formal expression, four readings. The bottom row shows the same expression in all four languages at once — the point of the Rosetta stone is that a single proof in type theory is simultaneously a construction in each column.
The dictionary deserves to be spelled out, because it is the working method of the whole subject: every construction on types is simultaneously a move in logic and a construction on spaces. A proposition is a space and a proof is a point of it — to prove is to inhabit. A predicate B(x) hangs a space over each point of A, a fibration. The pair type is and and the product space; the sum type is or and the disjoint union. The dependent pair Σ is there exists — a witness with evidence — and geometrically the total space, all the fibers glued over the base. The dependent function Π is for all, and geometrically the space of sections: a continuous choice of one point in every fiber. And the last row is the deepest: the identity type is equality on one reading and the path space on the other. A single argument, written once, proves a theorem in every column at the same time.
Scrub a membrane between two proofs. Preset A reels p · p⁻¹ in to the constant path; preset B snags on a hole, so no membrane exists.
The scrubber sweeps out the intermediate paths of a membrane — a 2-path, a proof between proofs. In preset A the loop p · p⁻¹ reels in like a lasso until it becomes the constant path at a, so out-and-back is connected to staying put. In preset B the membrane between p and q would have to pass through the hole, and no intermediate path can go there: the sweep snags from either side. That failure is the whole point — when the space has a hole, p and q are genuinely different proofs of the one equality a = b.
Paths have an algebra: reverse p to get p⁻¹, concatenate p and q when the endpoints meet. But test the algebra literally and it fails. Walk out along p and back along p⁻¹: that is not literally staying put — the round trip visits b, the constant path never leaves a. What is true is subtler and better: the round trip is connected to staying put by a membrane, the lasso reeling in that the demo below animates. Every groupoid law — inverses cancel, refl is a unit, concatenation is associative — holds in exactly this sense: not by definition but up to a higher path, a 2-path that must itself be constructed and is itself an object with its own equalities. Working “up to homotopy” at every level is the discipline of the subject. And the tower is not inert bookkeeping — it has theorems of its own: by an argument of Eckmann and Hilton, two-dimensional loops can slide around one another, so at dimension two and above, composition of loops is always commutative.
Spot a mistake or have an idea?