The foundations of mathematics, rebuilt out of paths — 30 interactive demonstrations of the young field where logic and topology turn out to be the same subject. A proof of equality becomes a path, a type family becomes a fibration, Voevodsky’s univalence axiom makes isomorphic structures literally equal, and a circle is defined by one point and one loop. Every idea is shown geometry-first, with the formal type theory one toggle away.
See also: Topology for the classical theory of spaces and deformations, Algebraic Topology for fundamental groups and homology the traditional way, Hopf Fibration for a deep dive into the fibration that appears in our sphere table, Category Theory for the language of universal properties, and Mathematical Logic for the proof theory this field grew out of.
A proof that two things are equal is a path between them — and there can be many genuinely different proofs
Types, constructors, and propositions-as-types: proving a theorem is the same as building an element
Path induction says every path with a free end reels in to reflexivity — so why can’t every loop?
Type families are fibrations: carry a point along a path and the fiber may come back twisted
Voevodsky’s axiom: a path between types is an equivalence, and isomorphic structures really are equal
Propositions, sets, and groupoids are rungs of one homotopical ladder — and truncation moves you down it
One point and one loop make a circle: higher inductive types build spaces from generators
Transporting the number zero around the circle proves π₁(S¹) = ℤ — with univalence doing the twisting
The homotopy groups of spheres: a periodic table of ℤs and ℤ₂s, with cells no human being knows
The real numbers and Conway’s surreals rebuilt as data types — the foundation Conway asked for in 1976