Transporting the number zero around the circle proves π₁(S¹) = ℤ — with univalence doing the twisting
This is the first real theorem of synthetic homotopy theory, and it is the one that convinced people the subject was going somewhere. The fundamental group of the circle is the integers. Classically it takes a chapter of point-set topology; here it takes a two-line definition and a transport — and the proof computes.
Half of the statement is easy. The circle is one point and one loop, so wrapping is free: go around once, twice, backwards, not at all. That already gives an integer’s worth of loops. The hard half is showing that none of them secretly coincide and that there are no others hiding. And the obvious approach dies immediately — path induction needs a free endpoint, while a loop has both ends pinned to the same point.
The way through is the universal cover. Classically it is a helix hovering above the circle, winding endlessly up and down, each of its points dropping straight onto the circle below. The fiber over any point is a stack of integers, one per level. Walk counterclockwise around the circle and the point riding above you climbs exactly one level; walk clockwise and it descends. What this lesson shows is that the helix is not an analogy we import — it is something the type theory builds for itself, out of univalence.
Build a loop word out of loop and loop⁻¹, or drag the bead around the base circle directly, and watch the lifted bead climb and descend the helix in lockstep. The counter is not a separate calculation — it is literally the result of transporting the number zero along the path you built. Cancellations happen on their own. Then flip the forget univalence switch and watch the cover fall apart.
The violet bead lives on the base circle; the amber bead is its lift in the cover, and the cyan markers are the integers — the fiber over the basepoint. Press loop or loop⁻¹ to append letters, or grab the bead and drag it around the base circle yourself: each full counterclockwise turn past the basepoint climbs one level (succ), each clockwise turn descends (pred). Cancelling loop·loop⁻¹ never moves the lift — transport is homotopy-invariant. Drag elsewhere to orbit the camera.
Here is the whole construction. Define a family of types over the circle by the circle’s own recursion principle, which asks for exactly two things: a value at the base point, and a loop at that value. For the value, take the integers. For the loop — and this is the entire trick — take the path that univalence builds out of the successor equivalence. Read the second line aloud and it says: going around the loop shifts the fiber up by one.
Now decoding is just transport. Feed a loop into encode by transporting the integer zero along it: each traversal of loop applies successor, each traversal of loop reversed applies predecessor, and a word like loop · loop⁻¹ · loop pushes zero through successor, predecessor, successor to arrive at one. Transport is computing the winding number, cancellations included. Going the other way, decode sends an integer to that many wraps. The two are inverse, so the loop space of the circle is exactly the integers — and because the integers form a set, with no interesting paths between their paths, the circle has no higher homotopy at all.
Draw any closed curve around the puncture and the winding number appears. Then drag the curve’s handles and try to change it. Stretch it, crumple it, loop it around itself — the integer will not budge. The only way to change it is to pull the curve across the puncture, which is exactly the move a homotopy is not allowed to make.
Load a preset or draw a closed loop freehand around (or away from) the puncture; the winding number is computed live as the total angle the curve sweeps around the hole, divided by 2π. Then grab any handle and deform the loop as wildly as you like — the integer never moves, and any edit that would cross the puncture is refused. Two loops in the punctured plane are homotopic exactly when their winding numbers agree: the integer is a complete invariant.
It is worth sitting with the failed attempt, because it explains the shape of the real proof. You want to show that loop is not refl. Path induction is the tool for proving things about paths, so you reach for it — and it refuses to apply. Path induction works on the family of paths from a fixed start to a free end; the free endpoint is what lets a path slide back along itself into refl. A loop has both ends nailed to the base point, so the family you would need to induct over is not the one the rule gives you. No amount of cleverness rearranges this: if you could prove every loop was refl, every type would be a set, and the whole theory would collapse.
The encode-decode method sidesteps the problem by never trying to analyze the loop from the inside. Instead it maps out of the circle into a family whose fibers are something concrete and well understood — the integers — and reads the answer off there. You are not proving facts about paths directly; you are building a machine whose readings the paths cannot help but produce.
The same method, on a type where the answer is already familiar. A code family over pairs of natural numbers, defined by double recursion: lit on the diagonal, empty everywhere else. Click a cell to unfold the recursion one step at a time and watch the Peano axioms drop out — zero is never a successor, and successor is injective.
Click any cell to unfold code(m, n). Lit cells are the unit type — the two numbers are equal. Dark cells are the empty type — nothing can connect them.
Start: code(5, 5).
Pick any cell in row 0 or column 0 other than the corner. The recursion stops immediately at code(succ m, 0) ≡ 0. The code is the empty type, so there is no path — and that is the Peano axiom, derived rather than assumed.
Every diagonal step throws away one successor from each side and leaves the code unchanged. So code(succ m, succ n) and code(m, n) are the same type: the numbers agree after the peel exactly when they agreed before it.
This is the same trick as the winding number. Build a family of codes over the type you care about, then transport a starting token along a path and see where it lands. Here the token lands in the unit type or the empty type; over the circle it lands on an integer.
There is a final twist worth savoring. Univalence is not decoration in this proof — it is the load-bearing beam. Without it, the assumption that every type is a set stays perfectly consistent, and in such a world the circle’s loop would be equal to refl and this group would collapse to nothing. That is what the forget univalence switch in the first demo is dramatizing: strip the axiom away and the cover has no way to twist, so the levels fall apart into disconnected circles and the counter has nothing to count.
So this theorem does double duty. It computes a homotopy group, and it functions as a litmus test: the fundamental group of the circle is nontrivial exactly when the universe you are working in has nontrivial paths. One little theorem about a circle, reporting on the character of the entire foundation.