Skip to content

Yoneda lemma for ∞-categories

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.

Formalizations were contributed by Fredrik Bakke, Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger.

See more about the project at https://github.com/emilyriehl/yoneda.

  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 ↩