Formalizing the ∞-Categorical Yoneda Lemma
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
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.
Syllabus
[CPP'24] Formalizing the ∞-categorical Yoneda lemma
Taught by
ACM SIGPLAN
Related Courses
Universe or Multiverse?Stanford University via World Science U Inflationary Cosmology
Massachusetts Institute of Technology via World Science U Nature's Constituents
California Institute of Technology via World Science U Endless Universe: Beyond the Big Bang
Princeton University via World Science U Fundamental Lessons From String Theory
Harvard University via World Science U