Homotopy type theory

In mathematical logic and computer science, homotopy type theory (HoTT hɒt) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies. This includes, among other lines of work, the construction of homotopical and models for such type theories; the use of type theory as a logic (or internal language) for abstract homotopy theory and ; the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible); and the formalization of each of these in computer proof assistants. There is a large overlap between the work referred to as homotopy type theory, and as the univalent foundations project. Although neither is precisely delineated, and the terms are sometimes used interchangeably, the choice of usage also sometimes corresponds to differences in viewpoint and emphasis. As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux. At one time the idea that types in intensional type theory with their identity types could be regarded as groupoids was mathematical folklore. It was first made precise semantically in the 1994 paper of Martin Hofmann and Thomas Streicher called "The groupoid model refutes uniqueness of identity proofs", in which they showed that intensional type theory had a model in the category of groupoids. This was the first truly "homotopical" model of type theory, albeit only "1-dimensional" (the traditional models in the being homotopically 0-dimensional). Their follow-up paper foreshadowed several later developments in homotopy type theory. For instance, they noted that the groupoid model satisfies a rule they called "universe extensionality", which is none other than the restriction to 1-types of the univalence axiom that Vladimir Voevodsky proposed ten years later.