Awesome

Yoneda for ∞-categories

:warning: This project has been ❄ frozen ❄. For ongoing simplicial HoTT formalization see http://rzk-lang.github.io/sHoTT/.

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" ¹. This formalization project could be regarded as a companion to the article "Could ∞-category theory be taught to undergraduates?" ².

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. See also other Yoneda formalizations.

We presented this work at CPP 2024 and published an overview of our formalization project in the conference proceedings as "Formalizing the ∞-Categorical Yoneda Lemma" ³. This project has been frozen to match its state as of that publication.

Checking the Formalisations Locally

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

rzk typecheck