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 *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*. We will use the Lean Theorem Prover in this course. Note that the latest version (Lean 3) doen not support Homotopy Type Theory (yet), so you must use Lean 2.

Basic topology and mathematical maturity will be assumed. Some familiarity with algebraic topology will be helpful, as will some familiarity with programming in a functional language. This course has a flavour very different from typical mathematics courses, so open-mindedness and willingness to learn alien concepts is essential.

- Midterm Assignment, due 01 March 2017.
- The Fin Type Family, due 10 February 2017.
- Domination and Levels, due 04 April 2014.

*Uniqueness:*Credit for implementing proofs not in the lean HoTT library, and not implemented by other students.- Mathematical substance.
- Use of HoTT concepts.

- 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.
- ProvingGround Repository: Implementations in scala of large parts of HoTT.

**Instructor:**Siddhartha Gadgil**E-mail:***siddhartha.gadgil@gmail.com***Timing:**Monday, Wednesday, Friday 9:00 a.m. to 10:00 a.m.**Venue:**Lecture hall 5 (new wing), Department of Mathematics, IISc.