Type families are fibrations: carry a point along a path and the fiber may come back twisted
A type family hangs a fiber over every point of a space, and a path in the space slides points from one fiber to the next. That sliding is transport — and around a loop, it can bring a point home changed.
Drag the bead around the circle and watch the marker ride through the fibers. Try all three spaces: the cylinder, the Möbius band, and the helix.
Total space: a cylinder: base circle × fiber, no twisting. No net loops yet. Transport along refl is the identity: the marker sits exactly on its gray ghost.
Everything in the machine has a name. The projection from the total space back to the base — forget the fiber coordinate, keep the base point — is the fibration itself, and transport is its path lifting: given a path p in the base and a point u in the fiber over its start, there is a specified path in the total space that lies exactly over p and ends at transport(p, u). In classical topology a lift merely exists; here it is a concrete function the rules hand you, built by path induction from the single clause that refl transports as the identity. A dependent function f : Π(x:A) P(x) is then a section of the fibration — a choice of one point in each fiber, threading continuously through the total space. And continuity is not a hypothesis anywhere: every function automatically respects paths, because ap_f carries a path x = y to a path f(x) = f(y). In this world there is no such thing as a discontinuous map.
Over each point sit two strands, swapped at the seam. Connect (x, u) to (x, v) — dragging straight down the fiber fails, so find another way.
Task: connect (x, u) to (x, v) in the total space. Drag the white point straight down, or travel the base.
The matching chevrons show the gluing: the right end of the u-strand attaches to the left end of the v-strand and vice versa, so the two strands form one connected circle winding the base twice. That single twist is all it takes for (x, u) = (x, v) to hold in the total space while u = v fails in the fiber.
It is tempting to reason: “(x, u) = (x, v), and the first coordinates already agree, so the second coordinates must be equal too.” The demo shows exactly why that fails. A path between pairs in Σ(x:A) P(x) is not a pair of independent paths — it is a path p in the base together with a path lying over it, witnessing that u, transported along p, reaches v. Nothing forces the base path of a path from (x, u) to (x, v) to be refl_x. In the double cover it winds once around the circle, picks up the swap at the seam, and arrives at (x, v) — while inside the discrete fiber {u, v} there is no path from u to v at all. Equality in the total space is genuinely weaker than fiberwise equality: it only pins down the second coordinate up to transport along some base path. The precise statement is the characterization of paths in Σ-types: a path (w₁ = w₂) is equivalent to a base path plus an over-path, and only when you can force the base path to be refl does a fiberwise equality drop out.
Drag the loop’s basepoint along p and watch it arrive as p⁻¹ · q · p.
Nothing transported yet: the loop is still based at a.
Drag the white basepoint along p (or press Carry). The loop cannot let go of a — it trails behind, connected by the two strands of p, and arrives at x as the conjugate.
Because path types are types, they can be fibers too, and transport in these families computes to pure path algebra. Take the family of loop types, x ↦ (x = x). To move a loop q based at a over to a new basepoint x along p : a = x, the transported loop must start at x — so it first travels p backwards to reach a, goes around q, and returns along p. The result is the conjugate p⁻¹ · q · p, exactly the change-of-basepoint isomorphism between loop spaces that topology students meet for the fundamental group — except here it is not a construction anyone designed: it falls out of transport, computed by path induction. In the family x ↦ (a = x), where the fiber over x is the type of paths from a fixed a, a path q with free end at y transports along p : y = z by post-composition, q · p: the anchored end cannot move, so the free end simply grows. These little computations are workhorses — the rope-reeling picture of a free end, made algebraic — and the same mechanism, applied over the circle, will eventually count how many times a loop winds.
Spot a mistake or have an idea?