Voevodsky’s axiom: a path between types is an equivalence, and isomorphic structures really are equal
Mathematicians identify isomorphic structures every single day. “The” cyclic group of order three, “the” real numbers, “the” circle — each phrase quietly treats a whole family of isomorphic objects as one thing, and every theorem proved about one copy is used on all the others without a second thought. Set theory forbids this: {0, 1, 2} with addition and {♠, ♥, ♦} with a matching table are different sets, so they are simply not equal, and the daily habit is, strictly speaking, an abuse of notation.
Univalence — the axiom Vladimir Voevodsky added to type theory, and the one that made homotopy type theory a field — turns the habit into a theorem-respecting principle. It says that a path between two types in the universe is the same thing as an equivalence between them: A equals B is equivalent to A being equivalent to B. Equivalent types may be identified, officially and safely.
Getting there takes two ideas: saying precisely what an equivalence is (the answer runs through fibers), and taking seriously that the universe of types is itself a space, whose points are types and whose paths are — by the axiom — exactly the equivalences. The payoff comes last: drag a multiplication table across a path and watch algebra transport itself.
Four maps between small types. Hover a point y of B to light up its fiber — every point of A that lands on y, each dragging the whisker path recording where it landed. The badges count fiber sizes, and the verdicts show which maps are surjective, which are embeddings, and which are full equivalences.
Hover a point y of B to light up its fiber: every point of A that lands on y, each with its whisker arrow. The badge beside each y counts its fiber.
Every fiber has exactly one point. Nothing missed, nothing doubled — over each point of B sits precisely one point of A, whisker and all.
The naive definition — “f is an equivalence if it has an inverse” — turns out to be subtly wrong, because an inverse is data, not a property. A quasi-inverse is a package: a map g together with two homotopies witnessing that the round trips are the identity, and one map can carry many genuinely different packages. Carrying the package changes the type of the thing you are holding, which wrecks the bookkeeping later. The right notion looks at fibers instead. The fiber of f over y is the type of points x of A equipped with a path f(x) = y — a point dragging a whisker. Then f is an equivalence when every fiber is contractible: exactly one point of A over each point of B, up to a contractible wiggle. This splits neatly in two, as the demo shows — every fiber inhabited makes f surjective, every fiber a proposition makes f an embedding — and, unlike having-an-inverse, being an equivalence is a mere proposition: any two proofs of it are equal, so it is a property a map simply has or lacks.
Wire a bijection between three fruits and three letters, then press ua — the wiring becomes a genuine path between two points of the universe strip at the top. Click any element to transport it along the path, run the path backwards to apply the inverse, and add a second bridge to watch path concatenation compose the equivalences.
Step 1 — wire an equivalence e : A ≃ B. Click a fruit, then the letter it should pair with, until all three are wired. Any bijection will do.
The universe 𝒰 is itself a type, so it is itself a space — one whose points are types. What could a path A = B in that space mean? One direction is free: given such a path, transport along it carries elements of A to elements of B, and this always yields an equivalence. That canonical map is called idtoeqv. Univalence is the statement that idtoeqv is itself an equivalence: paths between types correspond exactly to equivalences between them, with an inverse map ua turning any equivalence into a path.
Note the direction of the move. Univalence does not collapse different types into one; it expands what counts as an equality until equality matches equivalence. The identity type on the universe was underdetermined — nothing in the rules said how many paths it had — and the axiom resolves the ambiguity generously, in favor of how mathematics is actually practiced. And the correspondence is structural, not just a bijection: path algebra mirrors equivalence algebra exactly. The identity equivalence becomes reflexivity, concatenation becomes composition, reversal becomes inverse, and transporting along ua(f) simply applies f. Univalence has a sibling axiom, function extensionality, which plays the same expanding game one floor down: a path between two functions is exactly a pointwise family of paths between their values — and it follows from univalence.
Here is why the axiom earns its keep. A semigroup is a type A packaged with a multiplication m and a proof that m is associative — a structured type. Given an equivalence e : A ≃ B, univalence hands us the path ua(e), and transport carries the entire package across it. Chasing the definitions, the multiplication that arrives on B is exactly m′(b₁, b₂) = e(m(e⁻¹(b₁), e⁻¹(b₂))): send both arguments back with e⁻¹, multiply where you know how, carry the answer over with e. That is precisely the formula a working mathematician would write down by hand — and the associativity proof rides along automatically, with no cases to re-check. Better still, the correspondence runs both ways: an equality of semigroups, unpacked, is precisely a semigroup isomorphism — a bijection that respects multiplication. “Isomorphic” and “equal” are no longer an abuse of notation apart; theorems about one structure transfer to the other for free.
The left type {a, b, c} carries a multiplication table — preset to the cyclic group ℤ₃, and editable by clicking cells. The right type {♠, ♥, ♦} carries nothing. Choose the equivalence e, press transport, and watch the structure arrive cell by cell, each entry computed as e(m(e⁻¹(x), e⁻¹(y))) with the formula shown for the highlighted cell.
The left type has a multiplication; the right type has only three glyphs. Rewire e if you like (each click swaps two images, so e stays a bijection), edit m by clicking its cells, then press transport the structure and watch m′ get computed one cell at a time.