Rzk and formalising synthetic ∞-category theory

Tutorial · Interactions of Proof Assistants and Mathematics (ITP School) · · Regensburg, Germany

Hands-on tutorial sessions on formalising synthetic ∞-category theory in rzk, at the Interactions of Proof Assistants and Mathematics school, Regensburg, September 18–29, 2023.

Code: fizruk/itp-school-2023-demo