⚠️ 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" 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. 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.
Install the
rzk proof assistant. Then run the following command from the root of
our repository:
rzk typecheckFootnotes
-
Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 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 ↩