Homotopy type theory

In mathematical logic and computer science, homotopy type theory (HoTT) attempts to give an account of the semantics of intensional type theory using the framework of (abstract) homotopy theory, in particular Quillen model categories and weak factorization systems. Conversely, intensional type theory forms a logic (internal language) for homotopy theory.

Development

The Institute for Advanced Study held a special year for intensive work on developing homotopy type theory in the academic year 2012-2013, jointly organised by Steve Awodey, Thierry Coquand and Vladimir Voevodsky, which numerous mathematicians and computer scientists attended.

Out of this, a book, Homotopy Type Theory, was born. Unusually for a mathematics text, it was developed collaboratively and in the open on GitHub, is released under a Creative Commons license that allows people to fork their own version of the book, and is both purchasable in print and downloadable free of charge.

Also, unusually, key parts of the mathematics were implemented in the computer proof assistant Coq[1] and Agda,[2] where Agda is broadly equivalent to Coq but has a greater emphasis on functional programming than on constructing proofs through tactics. In both cases, type checking—or, viewed another way, computer proof verification—guarantees that the proofs were valid deductions, assuming that the proof assistant used was implemented correctly.

Open questions include a computational interpretation of homotopy type theory. Work is also underway to investigate new types of computer proof assistants with the goal of better supporting homotopy type theory.

Interpretation

Intensional type theory Homotopy theory
types $A$ spaces
terms $a$ maps
$a:A$ $a\in A$
dependent type $x:A\ \vdash\ B(x)\$ fibration $B \to A$
identity type $\mathrm{Id}_A(a,b)$ path space
$p:\mathrm{Id}_A(a,b)$ path $p:a\mapsto b$
$\alpha:\mathrm{Id}_{\mathrm{Id}_A(a,b)}(p,q)$ homotopy $\alpha:p\Rightarrow q$