Type Theory and Homotopy

The purpose of this survey article is to introduce the reader to a connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Martin-Lof into homotopy theory, resulting in new examples of higher-dimensional categories