CS 698H: Topics in Homotopy Type Theory

The course will assume some background in HoTT, (Ch 1, 2, 5, 6.1-6.5 from HoTT book). We plan to cover in the course some of the remaining material including applications in the HoTT book.

We also plan to cover some issues in semantics of HoTT and more recent topics like cubical type theory.

Students are expected to participate proactively in the course by discussion and by offerring to give some talks.

References

1. [HoTT Book] The Univalent Foundations Program. 2013.
2. Homotopy Type Theory: Univalent Foundations of Mathematics.
3. https://homotopytypetheory.org/book.