Voevodsky’s axiom: a path between types is an equivalence, and isomorphic structures really are equal
Mathematicians treat isomorphic structures as the same thing every day.Univalence makes that official: a path between two types is an equivalence between them, so structure and theorems transfer for free.
Hover a point of B to light up its fiber. The badges show which maps are surjective, which are embeddings, and which are 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, press ua, and it becomes a path between types. Click elements to transport them across.
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.
Choose an equivalence and press transport. The multiplication table arrives on the other side cell by 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.
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.
Spot a mistake or have an idea?