著者

西村 泰一

巻号頁・発行日

2016

---

Homotopy Type Theory lies at the crossroads of computer science, mathematical logic and homotopy theory. It was found out in the first decade of this century that dependent type theory is no other than the internal language for (abstract) homotopy theory, just as the Mitchell-Benabou language is the internal language for topos theory. It is pleasing to note that the Freudenthal suspension theorem, the Blakers-Massey homotopy excision theorem, Whitehead's principle for n-types, the van Kampen theorem, and some other famous theorems are given new proofs within homotopy type theory.