Formalizing the ∞-Categorical Yoneda Lemma
The first formalization of results from ∞-category theory in a proof assistant. Using rzk — designed to support Riehl–Shulman’s simplicial extension of homotopy type theory for synthetic ∞-category theory — we formalize the ∞-categorical Yoneda lemma. Many constructions become automatically natural or functorial thanks to the synthetic theory.
Formalizations matching published version are available at emilyriehl.github.io/yoneda/CPP-2024/.
A more complete and live formalizations in simplicial HoTT are in the sHoTT library.
Code: emilyriehl/yoneda, rzk-lang/sHoTT
Kudasov, N., Riehl, E., Weinberger, J. (2024). "Formalizing the ∞-Categorical Yoneda Lemma." Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), pp. 274–290. DOI: 10.1145/3636501.3636945.