This is a formalization library for simplicial Homotopy Type Theory (sHoTT) with the aim of proving the Yoneda lemma for ∞-categories following the paper "A type theory for synthetic ∞-categories" [1]. This formalization project could be regarded as a companion to the article "Could ∞-category theory be taught to undergraduates?" [2].

The formalizations are implemented using rzk, an experimental proof assistant for a variant of type theory with shapes developed by Nikolai Kudasov. Formalizations were contributed by Fredrik Bakke, Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger. The formalizations can be viewed as markdown files rendered at emilyriehl.github.io/yoneda/ using syntax highlighting supplied by Nikolai.

Another aim of this project is to compare the proof of the Yoneda lemma for ∞-categories in simplicial HoTT with proofs of the Yoneda lemma for 1-categories in other proof assistants. To that end Sina Hazratpour has contributed a formalization in Lean3 extracted from materials he prepared to teach Introduction to Proofs at Johns Hopkins, which can be found here.

We also contributed a proof of the Yoneda lemma for precategories to the Agda-Unimath library. Here we prove the Yoneda lemma for pre-∞-categories, since the univalence/completeness condition is not required for this result. By analogy, precategories are the non-univalent 1-categories in HoTT.

Install the rzk proof assistant. Then run the following command from the root of this repository:

rzk typecheck src/hott/* src/simplicial-hott/*

1. Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 2017. https://arxiv.org/abs/1705.07442

2. Emily Riehl. Could ∞-category theory be taught to undergraduates? Notices of the AMS. May 2023. https://www.ams.org/journals/notices/202305/noti2692/noti2692.html