Univalent Foundations

Origin. Vladimir Voevodsky (2006+). Homotopy type theory. Univalence axiom. Synthetic homotopy. Foundation of mathematics.

Models. Types as spaces. Equality as paths. Univalence: equivalence = equality. Higher groupoid structure. Foundation for all mathematics.

Formalism.

Type as space: Type A = topological space (up to homotopy). Terms a : A = points. Equality a = b = paths. Higher equalities = higher paths.

Identity types: Id_A(a, b) = type of paths from a to b. May have multiple paths. Homotopy structure. Not just true/false.

Univalence axiom: (A ≃ B) ≃ (A = B). Equivalence induces equality. Isomorphic types equal. Structure-preserving.

h-levels: -2: contractible (unique up to path). -1: proposition (at most one element up to path). 0: set (discrete equality). 1: groupoid. n: n-groupoid.

Propositions as types: Proof = term. Implication = function. Conjunction = product. Disjunction = coproduct (careful!).

Function extensionality: (∀x. f(x) = g(x)) → f = g. Follows from univalence. Functions equal pointwise.

Higher inductive types: Circle S¹: base point + loop. Suspension, pushouts, etc. Synthetic homotopy theory. New constructions.

Symbols.

Metatheory. Types as spaces. Univalence. Synthetic homotopy. New foundation.

Applies to. Foundations. Homotopy theory. Proof assistants. Category theory.

Limitations. Computational univalence. Learning curve. Tool support. Controversial.

© 2026 Lingenic LLC