Type theory and homotopy
pp. 183-201
in: P. Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm (eds), Epistemology versus ontology, Berlin, Springer, 2012Abstract
The purpose of this informal survey article is to introduce the reader to a new and surprising connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Per Martin-Löf into homotopy theory and higher-dimensional category theory.
