つくばリポジトリ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,
