Path induction says every path with a free end reels in to reflexivity — so why can’t every loop?
The identity type has exactly one constructor: refl, the trivial path from a point to itself. Its eliminator, path induction, says what eliminators always say — an arbitrary element is handled by handling each constructor — which here reads: to prove something about every path p : x = y, it suffices to prove it for refl. That sounds like a paradox. A space can teem with wildly different paths; loops around a hole cannot be straightened out. How can one lonely constructor account for all of them?
The resolution hides in a quantifier. Path induction applies when the endpoint y is free — quantified along with the path, pinned down by nothing. The type of “paths out of a with the far end wherever it likes,” Σ(x : A)(a = x), is contractible: any such path can reel its free end home along itself, shrinking to refl without ever crossing anything. A loop with both ends held is a different creature — it can snag around a hole — and path induction simply does not apply to it. The theory cannot prove all loops trivial, and that gap is precisely where homotopy lives.
The HoTT book’s own image makes it physical: a rope thrown around a pole. Hold both ends in your hand and the loop is stuck — pull all you like, it tautens against the pole. Let one end go, and the rope always gathers in.
A rope in a punctured region, shortening by honest curve-shortening — each point relaxes toward its neighbors, and the pole is a hard obstacle. With both ends pinned in your hand, a loop that winds the pole pulls taut and sticks. Switch to one end free, drag the rope into any tangle you like — even snagged around the pole — and press Shrink: it reels in every time.
Drag the rope to reshape it, then press Shrink.
The rope shortens by honest curve-shortening: each point relaxes toward its neighbors, and the pole is a hard obstacle. Pinned at both ends, a loop that winds the pole tautens against it and stops. Free at one end, the same rope gathers in every time — try snagging it around the pole first.
Every type in the system follows the same five-part template, and the identity type is no exception. Formation: for a, b : A there is a type a = b. One constructor: refl_a : a = a. The eliminator is path induction: to define something for all triples (x, y, p) with p : x = y, give the answer on the diagonal — the refl case — and the rule hands you the general answer, computing back to your case when the path actually is refl. Note what the rule does not say. It does not say every path is refl — that would be a theorem about each fixed pair of endpoints, and it is false in general. It says the identity type is freely generated by refl: anything you can build uniformly over all paths at once, you can build from the generator alone. The one constructor is a seed, not a census.
The based path space itself, made visible. Scatter fills the region with paths that all start at the basepoint a, each free end landing wherever it likes; Contract reels every free end back along its own path, all at once, until the whole tangle collapses to the constant path at a. Toggle the hole on and scatter again — some paths snake or wind right around it, yet contraction still succeeds, because an end retreating along its own path never has to cross anything.
Press Scatter to fill the based path space with paths out of a.
This is the based path space Σ(x : A)(a = x): all paths out of a, with the far endpoint free. Contracting it to the constant path at a is what it means for that space to be contractible — and that contractibility is exactly why path induction is a valid rule. Turn the hole on and scatter again: some paths now snake or even wind around it, but contraction still succeeds every time, because a free end retreating along its own path never has to cross anything.
The spaghetti demo is the whole justification. Path induction is not an extra axiom imposed on spaces; it is the statement that the based path space Σ(x : A)(a = x) — pairs of an endpoint and a path reaching it — is contractible. And it visibly is: whatever a path does, its free end can slide back along the path itself, dragging the pair (endpoint, path) continuously down to (a, refl_a). No hole can obstruct this, because the retreat happens along the path, never across the region. That is the free-ended rope gathering in.
Now pin both ends. A loop is a path in the loop space a = a, where the endpoint is fixed rather than quantified, and the contraction trick dies instantly: sliding the endpoint home is forbidden, because the endpoint is not allowed to move. The loop must deform within the region while both ends stay put — and around a hole, it cannot. Path induction stays silent about any single fixed identity type; it speaks only about all of them at once. So the theory never proves that every loop equals refl, and identity types are left free to be genuinely interesting spaces. That silence is load-bearing: it is exactly the room in which the circle gets a loop that provably is not trivial. See also: the winding-number lesson, The Winding Number, where counting how often a loop wraps the hole computes π₁(S¹) = ℤ.
Path induction at work, three times. Pick symmetry, transitivity, or transport and step through the same two-beat move: slide the free endpoint back along the path until only refl remains, state the (easy) refl case — refl⁻¹ :≡ refl, refl · q :≡ q, transport(refl) :≡ id — then un-slide and watch the general construction propagate back out over every path.
Goal: every path p : x = y has an inverse p⁻¹ : y = x.
A generic path p : x = y. The endpoint y is free — nothing pins it down.