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 will appear in a repository dedicated to simplicial homotopy type theory.
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.