Formalization

• A project to formalize synthetic ∞-category theory in the simplicial type theory introduced in joint work with Mike Shulman is ongoing. Formalizations have been contributed by Nikolai Kudasov, Jonathan Weinberger, and myself, using the computer proof assistant Rzk developed by Nikolai. Our preliminary goal, to formalize the ∞-categorical Yoneda lemma, can be found on github and on the web. The repository also hosts a comparative formalization of the 1-categorical Yoneda lemma in Lean written by Sina Hazratpour. Further developments in simplicial homotopy theory appear in a repository dedicated to simplicial homotopy type theory which has had many contributions.

• A project to formalize formal ∞-category theory in Lean has just launched. A blueprint set up for me by Pietro Monticone describes our broader objectives and initial formalization targets. This project is co-lead by Dominic Verity and Mario Carneiro who collaborated with me on the surprisingly intricate task to construct the right adjoint to the nerve functor, resulting in some code which is on its way into Mathlib and can be found here.

• In Fall 2021, I taught a graduate topics course on homotopy type theory, following Egbert Rijke’s wonderful Introduction to Homotopy Type Theory. For this course, I wrote 10 Agda problem sets and prepared a short agda tutorial. All of the course materials can be found on the course website.