Univalent Foundations

Origin. Vladimir Voevodsky proposed the programme from about 2005, first in circulation as "A very short note on homotopy λ-calculus" (2006), and named it univalent foundations. The precedents are Hofmann and Streicher's groupoid model (1998) and Awodey and Warren's homotopy-theoretic reading of identity types (2009). Voevodsky's own contributions are the definition of h-levels, the univalence axiom, the simplicial set model, and the Coq library Foundations (2010), continued as UniMath. The special year at the Institute for Advanced Study (2012–13) produced Homotopy Type Theory: Univalent Foundations of Mathematics (2013).

Models. The programme is a proposal about what the foundation of mathematics should be, not a technique inside an existing one. Its claim is that the primitive notion of sameness should be equivalence rather than set-theoretic equality, so that isomorphic structures are literally identical and no transport lemma has to be proved by hand. Types are read as homotopy types, identity types as path spaces, and the h-level hierarchy recovers propositions and sets as the bottom two levels of a structure that continues upward. Voevodsky's stated motivation was mechanical checkability of his own work.

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, precisely: There is a canonical map idtoeqv : (A = B) → (A ≃ B) defined by path induction from the identity equivalence. Univalence asserts that this map is itself an equivalence. It is an axiom about a universe: U is univalent. The inverse is written ua : (A ≃ B) → (A = B). The slogan "equivalence is equality" is the statement that idtoeqv is an equivalence, not that the two types are the same.

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. The indexing starts at -2 so that "n-type" agrees with the topologist's n-truncated space.

The simplicial model: Types interpret as Kan complexes, contexts as fibrations. Universes come from Voevodsky's universal Kan fibration. Gives consistency of the axiom relative to ZFC with two inaccessible cardinals.

Structure identity principle: Transporting along ua carries structure across an equivalence. Isomorphic groups, rings, categories satisfy the same properties by a theorem rather than by convention. For categories the right notion is the univalent (saturated) one, where isomorphism of objects is identity of objects.

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.

Symbol	Unicode	Name	Meaning
≃	U+2243	Equivalence	A ≃ B: a map with contractible fibres
→	U+2192	Arrow	A function type, or a map
∀	U+2200	Universal	Quantifier in the statement of function extensionality
‖	U+2016	Double vertical line	Delimiter of the propositional truncation ‖A‖
¹	U+00B9	Superscript one	Dimension of the circle S¹
λ	U+03BB	Lambda	Abstraction; the "homotopy λ-calculus" of the 2006 note
∞	U+221E	Infinity	The (∞,1)-toposes in which univalence holds
=	—	Identity type	The type of paths, not a judgement
Id_A	—	Identity type	The same, written with the type explicit
UA	—	Univalence axiom	The assertion that idtoeqv is an equivalence
idtoeqv	—	Canonical comparison	(A = B) → (A ≃ B), defined by path induction
ua	—	Inverse of idtoeqv	Turns an equivalence into a path
‖A‖	—	Propositional truncation	The (-1)-truncation, forgetting which witness
U	—	Universe	The type of types the axiom is asserted about
S¹	—	Circle	The higher inductive type with a base point and a loop
h-level	—	Truncation level	Contractible at -2, proposition at -1, set at 0

Metatheory. Univalence is not a conservative addition: it implies function extensionality, a result of Voevodsky's, and it is inconsistent with Streicher's axiom K and with uniqueness of identity proofs, since a univalent universe is provably not a set. Consistency is model-theoretic. Voevodsky's simplicial set model, written up by Kapulkin and Lumsdaine as "The simplicial model of univalent foundations (after Voevodsky)", interprets types as Kan complexes and universes by a universal Kan fibration, giving consistency relative to ZFC with two inaccessible cardinals. Shulman (2019) generalized this to show univalence holds in every Grothendieck (∞,1)-topos, so the axiom is not an artefact of simplicial sets. Bezem, Coquand and Huber (2014) gave a constructive cubical set model, which is the basis for the cubical type theories in which univalence computes. The structure identity principle is a theorem in this setting: Ahrens, Kapulkin and Shulman (2015) proved the Rezk completion turns any precategory into a univalent one.

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

Limitations. Univalence is stated as an axiom and has no computation rule, so canonicity fails: a closed term of natural number type built with ua need not reduce to a numeral, and the theory loses the property that makes type theory a programming language. Cubical type theories restore computation at the cost of a different, more complicated syntax, and univalence in the original formulation is not the same theory. The consistency proof is not constructive and consumes two inaccessible cardinals, so the foundation is not self-supporting in the way set theory is usually taken to be. Several natural constructions are unavailable: semisimplicial types cannot be defined internally, which is why two-level and cubical variants were introduced, and the law of excluded middle for arbitrary types contradicts univalence, so classical reasoning is confined to the h-propositions.