Mathematical Science III

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\u27s principle for n-types, the van Kampen theorem, and some other famous theorems are given new proofs within homotopy type theory.数理科学IIIA（春学期)数理科学IIIB（秋学期