8 min read
On this page

Homotopy Type Theory

Motivation

Homotopy Type Theory (HoTT) reinterprets Martin-Lof type theory through the lens of homotopy theory. The central insight: identity types behave like path spaces in topology. Types are spaces, terms are points, and proofs of equality are paths. Higher-dimensional structure emerges naturally.

Traditional type theory treats equality proofs as irrelevant (proof irrelevance) or collapses them (uniqueness of identity proofs / UIP). HoTT instead takes the higher structure of identity types seriously, leading to a new foundation for mathematics.

Identity Types as Paths

The identity type Id_A(a, b) (or a =_A b) classifies proofs that a and b are equal. In HoTT, elements of Id_A(a, b) are interpreted as paths from a to b in the space A.

Formation: If a, b : A, then a =_A b : Type Introduction: refl_a : a =_A a (the constant path) Elimination: J-eliminator (path induction):

J : (C : (x y : A) -> (x =_A y) -> Type) ->
    ((x : A) -> C x x refl) ->
    (x y : A) -> (p : x =_A y) -> C x y p

Path induction says: to prove something about all paths, it suffices to prove it for the reflexivity path. This is because (in the homotopy interpretation) the space of pointed paths is contractible.

Path Operations

From the J-eliminator, we derive:

  • Inverse: p^{-1} : b =_A a (path reversal)
  • Concatenation: p . q : a =_A c given p : a =_A b and q : b =_A c (path composition)
  • Transport: transport_P(p) : P(a) -> P(b) for p : a =_A b (moving along a path in a fibration)
  • ap (action on paths): ap_f(p) : f(a) =_B f(b) for f : A -> B and p : a =_A a (functorial action)

Higher Paths (Iterated Identity Types)

Paths between paths are elements of iterated identity types:

p =_{a =_A b} q : Type

These are 2-paths (homotopies between paths). This continues indefinitely:

  • 0-paths: points (elements of A)
  • 1-paths: paths (elements of a =_A b)
  • 2-paths: homotopies (elements of p =_{a=b} q)
  • n-paths: higher homotopies

This gives every type the structure of an infinity-groupoid (or more precisely, a weak omega-groupoid).

Homotopy Levels (n-Types / Truncation Levels)

Types are classified by their homotopy complexity:

  • (-2)-type (contractible): Has exactly one element up to paths. Sigma (a : A). Pi (x : A). a = x.
  • (-1)-type (mere proposition / h-prop): Any two elements are equal. Pi (x y : A). x = y. At most one element up to paths.
  • 0-type (h-set): Equality proofs between any two elements are unique. Pi (x y : A). Pi (p q : x = y). p = q. These are "ordinary" types where UIP holds internally.
  • 1-type (h-groupoid): Equality proofs form a set (equality of equality proofs is unique).
  • n-type: The (n+1)-fold iterated identity types are mere propositions.

Truncation: Given any type A, we can form its n-truncation ||A||n, which collapses all homotopy information above level n. The (-1)-truncation ||A||{-1} is the propositional truncation (mere existence: "A is inhabited" without specifying which element).

Most types in traditional mathematics are h-sets (0-types). The higher structure becomes relevant when dealing with quotient types, univalence, and abstract algebra.

The Univalence Axiom

Univalence (Voevodsky, 2006): For types A, B in a universe U:

(A =_U B) ≃ (A ≃ B)

That is, the identity type between types (in a universe) is equivalent to the type of equivalences between them. Two types are equal (as elements of the universe) if and only if they are equivalent.

Equivalence A ≃ B means there exists f : A -> B with a proof that f is an equivalence (has contractible fibers, or equivalently, has both a left and right inverse that are coherently related).

Consequences of Univalence

  1. Function extensionality follows: (Pi (x : A). f(x) = g(x)) -> f = g. This was previously an axiom.
  2. Structure identity principle: Isomorphic structures (groups, rings, etc.) are equal. No need for "transport of structure" lemmas -- equality IS isomorphism.
  3. Universe is not a set: U is at least a 1-type (has non-trivial path structure), since non-trivial automorphisms exist (e.g., Bool ≃ Bool has two elements).
  4. Proof-relevant mathematics: The path between A and B records HOW they are equivalent, not just THAT they are.

Univalence and Computation

The original univalence axiom is non-computational: it postulates an equivalence but does not specify how to compute with paths between types. This was a significant limitation, addressed by cubical type theory.

Higher Inductive Types (HITs)

Higher inductive types extend ordinary inductive types by allowing constructors that produce not just points but also paths (and higher paths).

The Circle S^1

HIT S1 :=
  | base : S1
  | loop : base = base

S1 has one point (base) and one non-trivial loop. Its fundamental group is Z (the integers), provable within HoTT.

The Interval

HIT Interval :=
  | zero : Interval
  | one : Interval
  | seg : zero = one

The interval is contractible (equivalent to Unit) but useful as a tool for constructing homotopies.

Quotient Types

HIT A/R :=
  | q : A -> A/R
  | glue : (a b : A) -> R a b -> q(a) = q(b)
  | trunc : is-set(A/R)    -- 0-truncation to make it a set

This gives a clean construction of quotients without setoids. The integers (Z = Nat * Nat / ~) and rationals can be defined this way.

Pushouts and Suspensions

General colimits (pushouts, coequalizers) are definable as HITs. The suspension of A:

HIT Susp A :=
  | north : Susp A
  | south : Susp A
  | merid : A -> north = south

Susp Bool ≃ S1. Susp S^n ≃ S^{n+1}. This enables synthetic homotopy theory.

Synthetic Homotopy Theory

HoTT enables proving results of classical homotopy theory purely within type theory:

  • pi_1(S^1) = Z: The fundamental group of the circle is the integers (Licata-Shulman, 2013). The proof uses the universal cover, defined as a type family over S1 via univalence.
  • Hopf fibration: Constructible as a type family over S^2, with fiber S^1 and total space S^3.
  • pi_n(S^n) = Z: Higher homotopy groups computed synthetically.
  • Blakers-Massey theorem: Proved in HoTT (Favonia et al.), with cleaner proofs than classical versions.

Cubical Type Theory

Cubical type theory (Cohen-Coquand-Huber-Mortberg, 2018 -- the CCHM model) provides a computational interpretation of univalence.

The Interval and Faces

Cubical type theory introduces a formal interval I with endpoints 0 and 1. Paths are functions from I:

Path A a b = (i : I) -> A [i=0 -> a, i=1 -> b]

The interval is NOT a type but a "dimension" -- terms can depend on interval variables.

Key Operations

Composition (comp): Given a path in a type that varies along a dimension, compute the endpoint. This is the computational content of transport.

Glue types: The mechanism implementing univalence. Glue types allow attaching an equivalence along a face of a cube:

Glue [phi -> (B, e)] A

where phi is a face formula, B is a type, and e : B ≃ A. When phi is true, the Glue type is B; otherwise, it is A. The boundaries are connected by the equivalence e.

Kan Operations

Types in cubical type theory must satisfy the Kan condition: every open box can be filled. This is the constructive analog of the Kan fibration condition in simplicial homotopy theory.

The filling operation (hcomp) computes: given the sides of a cube, produce the missing face. This gives computational content to:

  • Path concatenation
  • Transport
  • Univalence (via Glue types)

Implementations

  • Cubical Agda (Vezzosi-Mortberg-Abel, 2019): Full cubical type theory in Agda
  • cooltt (Sterling et al.): Research implementation
  • redtt / redPRL: Experimental cubical provers

Computational Univalence

In cubical type theory, univalence computes. Given an equivalence e : A ≃ B:

  1. ua(e) : A = B is defined using Glue types
  2. transport(ua(e), a) reduces to e(a) -- actually computes!
  3. ua(id_A) reduces to refl_A

This resolves the main criticism of the original HoTT book's axiom: proofs involving univalence now produce actual computational content rather than being stuck terms.

Canonicity

Theorem (Huber, 2018): Cubical type theory satisfies canonicity: every closed term of type Nat reduces to a numeral.

This was a major open problem for HoTT with the univalence axiom. Book HoTT does not have canonicity (univalence introduces stuck terms). Cubical type theory recovers it by giving univalence computational content.

Comparison of Approaches

| Feature | Book HoTT | CCHM Cubical | Cartesian Cubical | |---|---|---|---| | Univalence | Axiom | Theorem (computes) | Theorem (computes) | | Canonicity | No | Yes | Yes | | HITs | Postulated | Built-in | Built-in | | Interval | No | Formal I | Formal I | | Function ext. | Follows from UA | Built-in | Built-in | | Implementation | -- | Cubical Agda | redtt |

Unresolved Questions

  • Coherence: Defining semi-simplicial types and other higher-dimensional structures requires solving coherence problems (infinitely many equations).
  • Set-level mathematics: Most "ordinary" mathematics lives at the 0-type level. Is the extra HoTT machinery worth it for set-level proofs?
  • Directed type theory: HoTT captures spaces (symmetric paths). Directed HoTT would capture categories (non-symmetric morphisms). This is an active research frontier.
  • Two-level type theory: Combines an "outer" strict equality with an "inner" homotopy equality, potentially solving coherence issues.
  • Normalization: Full normalization for cubical type theory is still being established in full generality.

Significance

HoTT provides a synthetic framework for homotopy theory, an alternative foundation for mathematics (replacing set theory), and a new perspective on type theory where types have intrinsic geometric structure. The development of cubical type theory demonstrates that constructive, computational foundations can accommodate higher-dimensional structure without sacrificing decidable type checking.