Homotopy Type Theory and Univalent Foundations

⚡ Key Takeaways

Homotopy Type Theory (HoTT) interprets Martin-Löf dependent type theory through the lens of abstract homotopy theory: types are spaces (∞-groupoids), terms are points, and identifications `a = b` are paths. The Univalent Foundations program, initiated by Vladimir Voevodsky, augments this with the Univalence Axiom — equivalent types are equal — yielding a foundation for mathematics where isomorphic structures are literally interchangeable and proofs are computable, machine-checkable objects.

💡 The Core Insight

Propositions are types; proofs are terms; equalities are paths. In ordinary logic, `a = b` is true or false. In HoTT, the type `a = b` is a space whose points are proofs of equality (paths), paths between paths are 2-cells, and so on without bound. This single reinterpretation turns type theory into synthetic homotopy theory: you reason about spaces using only the inference rules of identity types, never mentioning topology, yet recover π₁(S¹) = ℤ as a theorem. Univalence then asserts the homotopical content of the universe itself: the path space of the universe of types is the space of equivalences.

DefinitionDependent Type Theory: Judgments and Contexts

The base system is intensional Martin-Löf type theory (MLTT). Its four basic judgment forms are:

`Γ ⊢ A : 𝒰` — in context Γ, `A` is a type (a term of a universe `𝒰`).
`Γ ⊢ a : A` — in context Γ, `a` is a term of type `A`.
`Γ ⊢ A ≡ B : 𝒰` — `A` and `B` are judgmentally (definitionally) equal types.
`Γ ⊢ a ≡ b : A` — `a` and `b` are judgmentally equal terms.

A context Γ = (x₁ : A₁, …, xₙ : Aₙ) is a telescope of typed variables where each Aᵢ may depend on earlier variables. Crucially, judgmental equality `≡` (decidable, computational) is distinct from propositional equality, the identity type `=` (a type, possibly with rich structure).

DefinitionDependent Function and Pair Types

Given a family `B : A → 𝒰`, the dependent product (Π-type) and dependent sum (Σ-type) are:

1

\quad \prod_{x:A} B(x), \qquad \sum_{x:A} B(x).

Derivation hint: Π generalizes the function space A → B (take B constant) and universal quantification ∀; Σ generalizes the product A × B and existential quantification ∃. Their formation, introduction (λ-abstraction / pairing), elimination (application / projection), and computation rules are the standard MLTT rules. A term `f : ∏_{x:A} B(x)` sends each `a : A` to `f(a) : B(a)`. A term `p : ∑_{x:A} B(x)` is a pair `(a, b)` with `a : A`, `b : B(a)`, with projections `pr₁ p : A` and `pr₂ p : B(pr₁ p)`.

DefinitionThe Identity Type

For a type `A` and terms `a, b : A`, the identity type `Id_A(a,b)`, written `a =_A b`, is formed with a single introduction rule giving reflexivity:

2

\quad \mathsf{refl}_a : a =_A a.

Derivation hint: refl is the canonical loop/constant path. There are no other constructors — all structure of identity types comes from the eliminator, not from additional points. Its eliminator is path induction (the J rule): to prove a family `C : ∏_{x,y:A}(x =_A y) → 𝒰` for all `x, y, p`, it suffices to give it for the reflexivity case:

3

\quad J : \Big(\prod_{x:A} C(x,x,\mathsf{refl}_x)\Big) \to \prod_{x,y:A}\prod_{p : x=_A y} C(x,y,p),

with computation rule `J(c, x, x, refl_x) ≡ c(x)`.

💡 The Core Insight

Path induction is deceptively powerful. From J alone one derives, for every type A:

Inversion `(p : a = b) → (b = a)` (paths are symmetric),
Concatenation `(p : a = b)(q : b = c) → (a = c)` (paths compose),
coherence laws: associativity, unit, inverse — all up to higher paths, never strictly.

These witnesses do not satisfy groupoid laws on the nose; the laws hold up to 2-paths, which satisfy their laws up to 3-paths, ad infinitum. This is exactly the structure of a weak ∞-groupoid. The Hofmann–Streicher groupoid model (1998) first showed the identity type need not be a mere proposition, foreshadowing the homotopical reading.

TheoremUnivalence Axiom — Voevodsky

For all types `A, B : 𝒰`, the canonical map

4

\quad \mathsf{idtoequiv} : (A =_{\mathcal U} B) \longrightarrow (A \simeq B)

is itself an equivalence. Equivalently, the type of equalities `A = B` is equivalent to the type of equivalences `A ≃ B`:

5

\quad (A =_{\mathcal U} B) \;\simeq\; (A \simeq B).

Derivation hint: idtoequiv is defined by path induction — it sends refl_A to the identity equivalence id_A. Univalence asserts this map has contractible fibers. "Equivalence" here is the homotopically correct notion (below); naively requiring a quasi-inverse fails to be a proposition.

DefinitionEquivalence

A map `f : A → B` is an equivalence, written `isequiv(f)`, when it has contractible fibers, or equivalently (and as a mere proposition) when there exist coherent left and right inverses:

6

\quad \mathsf{isequiv}(f) \;:\equiv\; \Big(\sum_{g:B\to A}\textstyle\prod_x g(f x)=x\Big)\times\Big(\sum_{h:B\to A}\textstyle\prod_y f(h y)=y\Big),

and `A ≃ B :≡ ∑_{f:A→B} isequiv(f)`. Derivation hint: This "half-adjoint"/bi-invertible formulation is a mere proposition (any two proofs are equal), unlike the naive "quasi-inverse" Σ_g (g∘f = id) × (f∘g = id), which carries extra higher data. Propositionality is essential so that "being an equivalence" is a property, not structure.

DefinitionTruncation Levels

Types are stratified by how much higher path structure they carry. Define contractibility and the levels `n`-type for `n ≥ -2`:

7

\quad \mathsf{isContr}(A) :\equiv \sum_{c:A}\prod_{x:A}(c = x),

8

\quad \mathsf{is\text{-}(n{+}1)\text{-}type}(A) :\equiv \prod_{x,y:A}\,\mathsf{is\text{-}}n\text{-}\mathsf{type}(x =_A y), \quad \mathsf{is\text{-}(-2)\text{-}type} :\equiv \mathsf{isContr}.

Derivation hint: A type is a (−1)-type ("mere proposition") iff all its elements are equal; a 0-type ("set") iff its identity types are propositions (UIP holds); a 1-type ("groupoid") iff identity types are sets. Going up a level means "one more dimension of trivial paths above this point." The key levels:

(−2)-type: contractible (a point up to homotopy).
(−1)-type / mere proposition `isProp(A)`: `∏_{x,y} x = y`. Logic lives here.
0-type / set `isSet(A)`: identity types are propositions. Classical mathematics lives here.
1-type / groupoid, 2-type, …, and genuinely ∞-types (e.g. the universe 𝒰 itself).

⚠️ Univalence destroys "Uniqueness of Identity Proofs"

In a univalent universe, UIP (axiom K) — the claim that every type is a set — is false. The universe 𝒰 has nontrivial path structure: by univalence, `Bool = Bool` is equivalent to `Bool ≃ Bool`, which has two elements (identity and negation), so `Bool = Bool` is not contractible. Thus 𝒰 is not a set. This is why HoTT uses intensional type theory: extensional type theory and axiom K bake in UIP and are incompatible with univalence.

ProofFunction Extensionality from Univalence

A landmark consequence: univalence implies function extensionality — pointwise-equal functions are equal. 1. Let `f, g : ∏_{x:A} B(x)`. Define `happly : (f = g) → ∏_x (f x = g x)` by path induction (refl ↦ λx. refl). Goal: `happly` is an equivalence. 2. Weak function extensionality (each fiber of a family of contractible types is contractible) follows from univalence: if each `B(x)` is contractible then `∏_x B(x)` is contractible. Proof: `∏_x B(x) ≃ ∏_x 𝟙` by univalence applied fiberwise (since `B(x) ≃ 𝟙`), and `∏_x 𝟙` is contractible. 3. Fix `f`. Consider the total space `∑_{g} ∏_x (f x = g x)`. Using step 2, one shows the map `(g, λx.refl) ↦ ...` exhibits this total space as contractible (it retracts onto the contractible `∑_g (f = g)`, the based path space). 4. A map between types is an equivalence iff it induces an equivalence on total spaces over a base; since both total spaces are contractible and `happly` respects the structure, `happly` is fiberwise an equivalence. 5. Therefore `(f = g) ≃ ∏_x (f x = g x)`. ∎

∎

ProofThe Fundamental Group of the Circle is ℤ

The circle `S¹` is the higher inductive type with a point `base : S¹` and a path `loop : base = base`. We sketch `π₁(S¹) = (base =_{S¹} base) ≃ ℤ`. 1. Define a fibration (type family) `code : S¹ → 𝒰` by circle-recursion: `code(base) :≡ ℤ`, and on the loop, `code(loop) := ua(succ)`, the univalence-image of the successor equivalence `ℤ ≃ ℤ`. 2. Define `encode : ∏_{x:S¹}(base = x) → code(x)` by transporting `0 : ℤ` along a path: `encode(p) :≡ transport^code(p, 0)`. Going around `loop` transports by `succ`, so `encode(loop^n) = n`. 3. Define `decode : ∏_{x:S¹} code(x) → (base = x)`; on the fiber over base, `decode(n) :≡ loop^n` (n-fold concatenation, with negative n using loop⁻¹). 4. Show `encode` and `decode` are mutually inverse by path induction / circle induction, establishing `(base = base) ≃ ℤ`. 5. Since ℤ is a set, `base = base` is a set, and its group structure under concatenation is the integers. Hence `π₁(S¹) ≃ ℤ`. ∎ This is "synthetic homotopy theory": no topology, no metric spaces — only the inference rules and univalence.

∎

Figure

The identity type as a path space, and truncation levels

```svg

```

mathematician · Vladimir Voevodsky | 1966–2017

Fields Medalist (2002) for his proof of the Milnor conjecture and development of motivic cohomology, Voevodsky turned, late in his career, to foundations after discovering errors in his own published work that human refereeing had missed. Around 2005–2009 he conceived Univalent Foundations: the realization that simplicial sets / Kan complexes model type theory, that the universe of types is itself a Kan complex whose path structure is the equivalence structure, and that this could be axiomatized as univalence. He built the Foundations library (later UniMath) in the Coq proof assistant and championed computer-verified mathematics. His simplicial-set model (with the resolution by Kapulkin–Lumsdaine of the coherence issues) gave the first model validating univalence, certifying its consistency relative to ZFC + inaccessibles.

🧠 Intuition

Think of a type as a space, and forget that points are "elements." Then:

A function `A → B` is a continuous map.
An equality `p : a = b` is a path; there can be many genuinely different ones (think loops around a hole).
Path induction says: to prove a statement about an arbitrary endpoint-and-path, you may assume the path is "no movement at all" (refl) and the endpoints coincide — because, homotopically, the space of paths starting at a fixed point is contractible (it deformation-retracts onto the constant path). You can always shrink one free endpoint back to the start.
Univalence says the universe 𝒰 is the "classifying space" in which the path from A to B is the same as the data of a homotopy equivalence A ≃ B. Walking from one type to another along a path is choosing an equivalence.
Truncation levels measure dimension: a proposition is a (−1)-dimensional space (empty or contractible), a set is a 0-dimensional space (discrete), and the universe is genuinely infinite-dimensional.

The slogan "equality is paths, isomorphism is equality" captures why mathematicians' informal "abuse of notation" (treating isomorphic objects as the same) becomes formally legitimate.

ExampleTransport along a univalence path

Given: The equivalence `neg : Bool ≃ Bool` swapping `true ↔ false`. By univalence, `ua(neg) : Bool =_𝒰 Bool`. Question: compute `transport^id(ua(neg), true)`.

Steps: 1. The computation rule for univalence (β-rule): `transport^(λX.X)(ua(e), x) = e(x)` for any equivalence `e`. 2. Apply with `e = neg`, `x = true`: `transport^id(ua(neg), true) = neg(true)`. 3. By definition of `neg`, `neg(true) = false`.

Answer: $\boxed{\mathsf{transport}^{\mathsf{id}}(\mathsf{ua(neg)},\ \mathsf{true}) \equiv \mathsf{false}}$ This shows the equality-path `ua(neg)` is "nontrivial": transporting along it genuinely moves data. (In a cubical implementation this even reduces computationally.)

ExampleCounting elements of an identity type in the universe

Given: The finite type `Fin 2` (two elements). Question: how many distinct elements does `Fin 2 =_𝒰 Fin 2` have, up to higher identification?

Steps: 1. By univalence (eq. [5]), `(Fin 2 = Fin 2) ≃ (Fin 2 ≃ Fin 2)`. 2. Since `Fin 2` is a set, `Fin 2 ≃ Fin 2` is equivalent to the type of bijections of a 2-element set, i.e. the symmetric group `S₂`. 3. `|S₂| = 2!` = 2 (identity and the swap), and this type is a set (a 0-type) because it sits over sets.

Answer: $\boxed{(\mathsf{Fin}\,2 =_{\mathcal U} \mathsf{Fin}\,2)\ \simeq\ S_2,\quad \text{with } 2 \text{ connected components}}$ Contrast with the classical view, where there is exactly one proof that Fin 2 equals Fin 2. Univalence makes the "automorphisms" of a type literally into its self-identifications.

⚠️ Univalence is not "everything is equal"

Univalence does not say all types are equal, nor that equivalent objects are definitionally (judgmentally) the same. It says `A = B` is equivalent to `A ≃ B` as types. Non-equivalent types (e.g. `Bool` and `𝟙`) remain unequal — their equality type is empty. And the equality is propositional, not judgmental: `transport` along it has computational content, it is not a "free" rewrite at the meta level.

CounterexampleNaive quasi-inverse is the wrong definition of equivalence

One might define "f is an equivalence" as `qinv(f) :≡ ∑_{g} (g∘f = id) × (f∘g = id)`. This is wrong for univalence because `qinv(f)` is not a mere proposition: for `f = id_S¹...` style types it carries extra higher loop data, so `qinv(f)` can be equivalent to something like `(loop space)`, having multiple elements. If one used `qinv` in defining `A ≃ B`, then `idtoequiv` could not be an equivalence because the target would have spurious extra structure. The fix (eq. [6]) is the bi-invertible or half-adjoint equivalence definition, which is provably a proposition. This subtlety is the single most common stumbling block for beginners.

⚠️ HoTT is not just "type theory with a new axiom" computationally

Adding univalence as a bare axiom to MLTT breaks canonicity: a closed term of type ℕ need no longer reduce to a numeral, because `ua` and the J-eliminator applied to `ua`-paths get "stuck." This was Voevodsky's open problem of canonicity. Cubical type theory (Cohen–Coquand–Huber–Mörtberg, 2016) solves it by replacing the identity type with paths over an interval pretype, giving univalence computational content so that everything reduces.

connection

HoTT sits at the crossroads of several fields:

Category Theory and Higher Category Theory: types model (∞,1)-categorical / ∞-groupoid structure; the syntax–semantics bridge is Categorical Logic via the initiality of the syntactic category among models.
Homotopy Theory: HoTT is "synthetic homotopy theory" — π_n(Sᵐ), the Freudenthal suspension theorem, the Blakers–Massey theorem, and the Hopf fibration have all been proved internally.
Model Categories and Quillen Model Structures: the semantic interpretation uses the model structure on simplicial sets (Kan complexes) and, more generally, ∞-Topoi (Shulman's model-topos models of univalence).
Constructive Mathematics and Intuitionistic Logic: as constructive MLTT, HoTT realizes the BHK interpretation, with propositions-as-(−1)-types refining propositions-as-types.
Proof Assistants (Coq, Agda, Lean): HoTT is implemented and used for Formal Verification of mathematics.
Set Theory (ZFC): not a rival but a comparand — univalent foundations is structural where ZFC is material; a univalent universe of sets (0-types) models structural set theory.

🔬 Where this appears

⏳ History

- 1972–1984 — Per Martin-Löf develops intuitionistic type theory (intensional and extensional variants), introducing dependent types and the identity type with its J-eliminator.

- 1994 — Hofmann & Streicher prove the independence of axiom K: the groupoid model interprets types as groupoids, showing identity types need not be propositions — the first hint of higher structure.

- 2005–2006 — Vladimir Voevodsky begins the Univalent Foundations program; identifies the simplicial-set (Kan complex) interpretation and formulates univalence; starts formalizing in Coq.

- 2006–2009 — Steve Awodey & Michael Warren give the homotopy-theoretic / weak-factorization-system semantics of identity types; Garner, Lumsdaine, van den Berg establish that identity types generate weak ∞-groupoids.

- 2009 — Voevodsky lectures on univalence; coins "univalent foundations"; the univalence axiom is stated precisely.

- 2011 — Lumsdaine & Kapulkin (building on Voevodsky, Streicher) work out the coherence theorems making the simplicial model rigorous, establishing consistency of univalence relative to ZFC + 2 inaccessibles.

- 2012–2013 — IAS Special Year on Univalent Foundations; the collaborative HoTT Book is written; higher inductive types systematized; synthetic computations of π₁(S¹), πₙ(Sⁿ), Hopf fibration.

- 2016 — Cohen, Coquand, Huber, Mörtberg introduce cubical type theory, giving univalence computational content and restoring canonicity; later realized in Cubical Agda.

- 2019 — Shulman proves univalence is modeled in every ∞-topos, vindicating the slogan that HoTT is the internal language of (∞,1)-toposes.

open-problem

Several foundational questions remain active:

Homotopy Canonicity / Normalization for full HoTT with HITs: while cubical type theory has canonicity, a general theory of higher inductive types with a clean computational and semantic account (a fully general schema with normalization) is still being refined.
Semantics of HITs: a uniform, model-independent specification of all higher inductive types and their elimination principles, with matching existence theorems in ∞-toposes, is incomplete.
The "initiality conjecture": rigorously proving that the syntactic category of HoTT is initial among its models (the precise soundness–completeness bridge) is technically heavy; substantial progress exists but a fully general, mechanized statement is ongoing.
Computational interpretation of all of univalent mathematics: integrating modalities, cohesion, and impredicativity while keeping canonicity.
Foundational status & strength: pinning down the exact proof-theoretic strength of HoTT with univalence and various HITs relative to standard set theories, and the role of resizing / propositional resizing axioms (which are not known to be computational).

Homotopy Type Theory and Univalent Foundations

Formal Statement

The Homotopy Type Hierarchy

Why It Holds / Derivation

Building Intuition

Worked Examples

Common Misconceptions

Connections

Real-World Applications

Historical Development

Subtleties & Limits

See Also