Yoneda for ∞categories¶
This is a formalization library for simplicial Homotopy Type Theory (HoTT) 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}.
Info
This project has been ❄ frozen ❄. For ongoing simplicial HoTT formalization see http://rzklang.github.io/sHoTT/.
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. Our
source files are available on github.
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 1categories
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 AgdaUnimath 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 nonunivalent 1categories 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" ^{3}. 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:

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

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 ↩

Nikolai Kudasov, Emily Riehl, Jonathan Weinberger, Formalizing the ∞Categorical Yoneda Lemma. CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and ProofsJanuary 2024Pages 274–290. https://dl.acm.org/doi/10.1145/3636501.3636945 ↩