Homotopy type theory

In mathematical logic and computer science, homotopy type theory (HoTT) refers to various lines of development of intensional 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 higher-categorical models for such type theories; the use of type theory as a logic (or internal language) for abstract homotopy theory and higher category theory; 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.

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 1998 paper of Hofmann and Streicher called "The groupoid interpretation of type theory", 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 category of sets being homotopically 0-dimensional).

...
Wikipedia