Path induction says every path with a free end reels in to reflexivity — so why can’t every loop?
To prove something about every path, it is enough to prove it for refl — as long as one end is free. A rope with a free end always reels in; hold both ends around a pole and it snags. That gap is where homotopy lives.
With both ends pinned, a loop around the pole pulls taut and sticks. Switch to one end free, tangle the rope, and press Shrink: it always reels in.
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.
Scatter paths from a basepoint, then contract them all at once. Turn the hole on and try again — contraction still works.
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¹) = ℤ.
Pick symmetry, transitivity, or transport. Slide the path back to refl, prove the easy case, and watch it spread to 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.
Spot a mistake or have an idea?