Working Seminar on Homotopy Type Theory

2023-24

This year's working seminar will be on Homotopy Type Theory. The main source for this is the HoTT Book.

After the first five talks, possible topics include:

• Cubical Type Theory: see Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom, and Cubical agda: a dependently typed programming language with univalence and higher inductive types describing an implementation in Agda
• LEAN as an Interactive Theorem Prover and a Functional Programming Language
• Category Theory (Chapter 9 of the HoTT Book)
• Topoi and schemes, see Blechschmidt's PhD thesis Using the internal language of toposes in algebraic geometry for a formalization of schemes using topoi
• The homotopy groups of spheres in HoTT