Formalizing the ∞-Categorical Yoneda Lemma

Explore groundbreaking research in the formalization of ∞-category theory through this 34-minute conference talk from CPP 2024. Delve into the first-ever formalization of the ∞-categorical Yoneda lemma, a fundamental theorem in category theory, using the Rzk proof assistant. Learn how Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger leverage Riehl–Shulman's simplicial extension of homotopy type theory to achieve this milestone in synthetic ∞-category theory. Discover the potential applications of this work in fields ranging from algebraic topology to theoretical physics, and gain insights into future plans for formalizing more advanced concepts in ∞-category theory, including limits, colimits, and adjunctions.

[CPP'24] Formalizing the ∞-categorical Yoneda lemma