Homotopy Type Theory and Univalent Foundations

Homotopy Type Theory is the synthesis of constructive dependent type theory with homotopy theory, discovered independently around 2005–2009 by Steve Awodey & Michael Warren (categorical/model-theoretic side) and Vladimir Voevodsky (the univalent perspective). Its central interpretive move is to read the identity type Id_A(a,b) not as a mere proposition but as the space of paths from a to b, so that a type carries the structure of a weak ∞-groupoid. This matters because it provides a logic in which the principle "isomorphic things are equal" — long an informal mathematical habit — becomes a formal theorem via the Univalence Axiom, and in which higher inductive types let one build spaces (circles, spheres, quotients, truncations) directly inside the logic. The surprising fact: the seemingly innocuous identity type, governed only by the rule that to prove something about all paths it suffices to handle reflexivity, secretly encodes all of homotopy theory.

The Core Insight

Formal Statement

Dependent 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).

Dependent Function and Pair Types

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

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).

The 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:

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:

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

Types as ∞-Groupoids

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.

Univalence Axiom — Voevodsky

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

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

Equivalence

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:

and A ≃ B :≡ ∑_{f:A→B} isequiv(f).

The Homotopy Type Hierarchy

Truncation Levels

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

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.

Why It Holds / Derivation

Function 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.

1. 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.

1. 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).

1. 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.

1. Therefore (f = g) ≃ ∏_x (f x = g x). ∎

The 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 ℤ ≃ ℤ.

1. 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.

1. 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⁻¹).

1. Show encode and decode are mutually inverse by path induction / circle induction, establishing (base = base) ≃ ℤ.

1. Since ℤ is a set, base = base is a set, and its group structure under concatenation is the integers. Hence π₁(S¹) ≃ ℤ. ∎

The identity type as a path space, and truncation levels

<svg viewBox="0 0 760 380" xmlns="http://www.w3.org/2000/svg">
  <rect width="760" height="380" fill="#0a0e17"/>
  <text x="20" y="30" fill="#e2e8f0" font-size="17" font-family="serif">Types as spaces: paths, 2-paths, and levels</text>

  <!-- left: path space -->
  <circle cx="120" cy="170" r="6" fill="#d4a853"/>
  <text x="98" y="160" fill="#e2e8f0" font-size="14">a</text>
  <circle cx="320" cy="170" r="6" fill="#d4a853"/>
  <text x="328" y="160" fill="#e2e8f0" font-size="14">b</text>

  <path d="M120 170 C 180 90, 260 90, 320 170" stroke="#d4a853" stroke-width="2.5" fill="none"/>
  <path d="M120 170 C 180 250, 260 250, 320 170" stroke="#94a3b8" stroke-width="2" fill="none"/>
  <text x="205" y="80" fill="#e2e8f0" font-size="13">p : a = b</text>
  <text x="200" y="280" fill="#e2e8f0" font-size="13">q : a = b</text>
  <path d="M210 120 C 225 145, 225 195, 210 220" stroke="#e2e8f0" stroke-width="1.3" fill="none" stroke-dasharray="4 3"/>
  <text x="232" y="175" fill="#e2e8f0" font-size="12">α : p = q  (2-path)</text>

  <!-- right: tower -->
  <line x1="500" y1="330" x2="500" y2="50" stroke="#94a3b8" stroke-width="1.5"/>
  <polygon points="500,42 495,56 505,56" fill="#94a3b8"/>
  <text x="510" y="60" fill="#e2e8f0" font-size="12">∞-type  (e.g. 𝒰)</text>

  <circle cx="500" cy="300" r="4" fill="#d4a853"/>
  <text x="512" y="305" fill="#e2e8f0" font-size="12">(−2)  contractible</text>
  <circle cx="500" cy="255" r="4" fill="#d4a853"/>
  <text x="512" y="260" fill="#e2e8f0" font-size="12">(−1)  proposition</text>
  <circle cx="500" cy="210" r="4" fill="#d4a853"/>
  <text x="512" y="215" fill="#e2e8f0" font-size="12">0   set (UIP)</text>
  <circle cx="500" cy="165" r="4" fill="#d4a853"/>
  <text x="512" y="170" fill="#e2e8f0" font-size="12">1   groupoid</text>
  <circle cx="500" cy="120" r="4" fill="#d4a853"/>
  <text x="512" y="125" fill="#e2e8f0" font-size="12">2   2-groupoid</text>

  <text x="20" y="360" fill="#94a3b8" font-size="12">Each level: "identity types are one level lower." Higher = more nontrivial path structure.</text>
</svg>

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.

Building 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.

Worked Examples

Transport along a univalence path

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.

Counting elements of an identity type in the universe

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.

Common Misconceptions

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.

Naive 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.

Connections

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.

Real-World Applications

1. UniMath / Foundations library — Voevodsky's Coq formalization providing a univalent foundation library for verified mathematics from the ground up.
2. Cubical Agda — a production proof assistant implementing cubical type theory; univalence computes, enabling fully constructive synthetic homotopy theory and verified data-type transport.
3. The HoTT Book (2013) — collaboratively written at the IAS Special Year, itself formalized; a model of open, community mathematics.
4. Verified program transport / data refinement — univalence lets one transport theorems and programs along equivalences of data structures (e.g. proving a property for a list representation and transporting it to a vector representation) with formal guarantees; relevant to certified compilers and the CompCert lineage of verified-software methodology.
5. Synthetic homotopy theory results — machine-checked proofs of π₄(S³) = ℤ/2ℤ, the Blakers–Massey theorem (with a novel generalization later useful in modal homotopy theory), and the Serre spectral sequence groundwork.
6. Directed and cohesive type theories — extensions (cohesive HoTT, Schreiber's program) aiming at synthetic differential geometry and foundations for mathematical physics / gauge theory.
7. Database and concurrency theory — directed/higher type-theoretic ideas inform models of rewriting and concurrent computation (homotopical interpretations of trace spaces).

Historical Development

• 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.

Subtleties & Limits

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).

See Also