MA 334: Introduction to Homotopy Type Theory
Credits: 3:0
Prerequisite courses: MA 210, MA 232, MA 332
Pre-requisites :
- Algebraic Topology, Dependent Type Theory
This course introduces homotopy type theory, which provides alternative foundations for mathematics based on deep connections between type theory, from logic and computer science, and homotopy theory, from topology. This connection is based on interpreting types as spaces, terms as points and equalities as paths. Many homotopical notions have type-theoretic counterparts which are very useful for foundations.
Such foundations are far closer to actual mathematics than the traditional ones based on set theory and logic, and are very well suited for use in computer-based proof systems, especially formal verification systems.
The course will also include background material in Algebraic Topology (beyond a second course in Algebraic Topology).
Suggested books and references:
- Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Studies, Princeton 2013.
- Hatcher, A., Algebraic topology, Cambridge University Press, Cambridge, 2002.
- Tutorial for the Lean Theorem Prover