Type theory and homotopy
Category Theory
2010-10-12 v1 Logic
Abstract
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-L\"of into homotopy theory, resulting in new examples of higher-dimensional categories.
Cite
@article{arxiv.1010.1810,
title = {Type theory and homotopy},
author = {Steve Awodey},
journal= {arXiv preprint arXiv:1010.1810},
year = {2010}
}
Comments
20 pages