Skip to content
The Lumenary
Research pathwaysFoundationsPlanned

Homotopy type theory

Homotopy type theory reads types as spaces (∞-groupoids) and equalities as paths. Voevodsky's univalence axiom identifies equivalent types, and higher inductive types make synthetic homotopy theory possible.

math.found.homotopy-type-theory

Show everything needed to reach this topic

The lesson for this topic has not been written yet. The outline below is part of the curriculum map and has not been reviewed.

Builds on

Type theory and propositions as typesAlgebraic topology

Required prerequisites, all the way down: 50

You will learn to

  • Explain identity types and their path interpretation, including transport and path induction.
  • State the univalence axiom and explain why it is incompatible with uniqueness of identity proofs for the universe.
  • Define the circle as a higher inductive type and outline the synthetic proof that its loop space is equivalent to ℤ.

Definition

  • For a, b : A, the identity type a =_A b has elements thought of as paths from a to b.
  • An equivalence of types is a function with contractible fibres, equivalently one with a two-sided homotopy inverse.
  • Univalence: for types A and B in a universe, the canonical map (A = B) → (A ≃ B) is an equivalence.
  • A higher inductive type has constructors for paths as well as points, such as base : S¹ and loop : base = base.

Theorem

  • In homotopy type theory the loop space of the circle is equivalent to ℤ (Licata and Shulman).
  • Univalence implies function extensionality.
  • Univalent type theory has a model in Kan simplicial sets (Kapulkin and Lumsdaine, after Voevodsky).

Common misconceptions

  • Thinking HoTT replaces set theory or category theory wholesale; it is one foundation among several, with its own strengths and open questions.
  • Reading univalence as a statement about sets in ZFC; it is an axiom about identity types inside type theory.
  • Identifying HoTT with ∞-category theory; they are connected through models, not the same subject.

Optional discoveries

Further reading