Skip to content

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 follows the philosophy layed out in "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.

Checking the Formalisations Locally

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

rzk typecheck src/hott/* src/simplicial-hott/*

References

  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