Rzk and formalising synthetic ∞-category theory
An rzk demo on September 19, followed by a joint problem session with Emily Riehl on September 26, at the Interactions of Proof Assistants and Mathematics school in Regensburg, September 18–29, 2023. Riehl lectured on formalising ∞-category theory in rzk at the same school.