Skip to content

Latest commit

 

History

History
77 lines (63 loc) · 3.98 KB

README.md

File metadata and controls

77 lines (63 loc) · 3.98 KB
Raw

Yoneda for ∞-categories

Yoneda for ∞-categories logo

Check with latest Rzk MkDocs to GitHub Pages

⚠️ 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.

Checking the Formalisations Locally

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

rzk typecheck

Footnotes

  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 ↩

  3. 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 ↩