Homotopy Type Theory: Unified Foundations of Mathematics and Computation∗

Homotopy type theory is a recently-developed unification of previously dis-parate frameworks, which can serve to advance the project of formalizing and mechanizing mathematics. One framework is based on a computational conception of the type of a construction, the other is based on a homotopical conception of the homotopy type of a space. The computational notion of type has its origins in Brouwer’s program of intuitionism, and Church’s λ-calculus, both of which sought to ground mathematics in computation (one would say “algorithm ” these days). The homotopical notion comes from Grothendieck’s late conception of homotopy types of spaces as represented by ∞-groupoids [12]. The computational perspective was developed most fully by Per Martin-Löf, leading in particular to his Intuitionistic Theory of Types [23], on which the formal system of homotopy type theory is based. The connection to homotopy theory was first hinted at in the groupoid inter-pretation of Hofmann and Streicher [14, 13].1 It was then made explicit by several researchers, roughly simultaneously.2 The connection was clinche