A proof that two things are equal is a path between them — and there can be many genuinely different proofs
Here is the single idea this module runs on. When type theory writes a : A, read it geometrically: A is a space, and a is a point of that space. Then ask what a proof of a = b should be, and the geometry answers for you: a path from a to b. Not a bare fact that flickers between true and false, but a thing — a route through the space, with a direction, an inverse, and a way of composing with other routes.
The moment equality becomes a path, everything classical logic flattened springs back into shape. Two paths between the same endpoints need not be interchangeable: if the space has a hole, a route around the left side and a route around the right side are genuinely different proofs of the one equality a = b. And since paths are points of their own space — the path space — we can ask when two proofs are equal, and the answer is a path between paths: a 2-path, a membrane sweeping one proof continuously into the other.
There is no top floor. Membranes have their own equality, witnessed by 3-paths, and so on forever: every type is an ∞-groupoid, an infinite tower of points, paths, and higher paths, all generated by the humble reflexivity proof. This lesson is the view from the balloon; the rest of the module climbs the tower on foot.
A blob-shaped space with three draggable points and named paths between them. Click chips to select and concatenate paths, reverse a whole expression, or drop to the constant path refl — a bead walks whatever proof you have built. Then punch a hole and watch p and q become two visibly different proofs that a equals b.
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.
The HoTT book opens with a table — one column of formal expressions, read four ways. Pick an expression and a lens: the same symbols become a logical connective, a set construction, a space, and a type. The identity type is where the four readings stop agreeing about how much structure there is — and that disagreement is the subject of this module.
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.
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.
Two proofs of one equality, and a scrubber that sweeps the intermediate paths of a membrane between them. Preset A reels the loop p · p⁻¹ in to the constant path — the 2-path behind the cancellation law. Preset B punches a hole between p and q: the sweep snags against it from either side, and no 2-path exists. This is exactly why there can be genuinely different proofs of one equality.
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.