Type families are fibrations: carry a point along a path and the fiber may come back twisted
A type family P : A → 𝒰 hangs a type over each point of a base — and that picture is exact, not decorative. The family is a fibration: the base is the space A, the fiber over x is the type P(x), and gathering every fiber over its base point yields the total space Σ(x:A) P(x), the type of pairs (x, u) with u sitting in the fiber over x.
The question this lesson answers is what happens to the fibers when you move. A path p : x = y in the base induces a function transport from P(x) to P(y): pick up a point of the fiber over x, slide it along p, and it lands in the fiber over y. The reflexivity path does nothing, so transport along refl is the identity — but a path that loops around the base can bring a point home changed. A cylinder returns it untouched; a Möbius band returns it flipped; a helix shifts it up one level per lap.
Two consequences repay close attention. First, a famous gotcha: a pair (x, u) can equal a pair (x, v) in the total space even though u and v are different points of the same fiber, because the connecting path is free to wind around the base before coming home. Second, when the family is made of path types, transport becomes something every topologist knows by heart: dragging a loop’s basepoint along p conjugates it into p⁻¹ · q · p.
A base circle with three total spaces to choose from. Drag the bead around the base (or press the loop button) and watch the white marker ride the lifted path through the fibers. The cylinder — a constant family — brings it home on its gray ghost; the Möbius band brings it back flipped; the helix, whose fibers are the integers, shifts it one level per loop.
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.
The HoTT book’s Remark 2.7.1 as a puzzle. The base circle is drawn flat with its ends identified, and over every point sits a two-point fiber {u, v} — with the strands glued by a swap at the seam. Your task: connect (x, u) to (x, v) in the total space. Dragging straight down the fiber fails; there is 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.
Transport where the fibers are themselves path types. Drag the basepoint of the loop q along the path p and watch the loop trail behind on the two strands of p, arriving as the conjugate p⁻¹ · q · p — the expression readout updates live. Then switch presets: a path with a free end transports by simply growing, 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.