Homotopy Type Theory: Univalent Foundations of Mathematics
by The Univalent Foundations Program · Institute for Advanced Study
Collaborative exposition written during the Institute for Advanced Study's Univalent Foundations year, presenting type theory as a foundation whose types behave like homotopy types. Covers identity types, the univalence axiom, higher inductive types, and formalised set and homotopy theory.
More resources on Homotopy Type Theory
homotopytypetheory.org
Official hub for Homotopy Type Theory, hosting the freely available HoTT book and accompanying course materials, tutorials, and links to related papers and community resources.
nLab: HoTT
The nLab wiki entry on homotopy type theory, a dense reference page linking identity types, univalence, higher inductive types and model-theoretic semantics to the research literature, useful for locating key papers and connecting HoTT to category theory and higher topos theory.
Introduction to Univalent Foundations of Mathematics with Agda
Learn univalent foundations of mathematics and homotopy type theory using Agda. Course by Martin Escardo.
nLab
Collaborative wiki for mathematics, physics and philosophy written from a category-theoretic viewpoint, with cross-linked entries on categories, functors, adjunctions, topos theory, higher category theory and homotopy theory. Readers can look up precise definitions, examples and references for advanced structural mathematics.