Formalizing the ∞-categorical Yoneda lemma
summary
Formalizes the ∞-categorical Yoneda lemma inside a new proof assistant called Rzk proof assistant (open source, VS Code plugin) using Riehl–Shulman’s simplicial extension of HoTT. Delivers a formal equivalence: evaluation at the identity maps uniform families of fiberwise maps to elements of the fiber, for covariant families over Segal (∞-)categories. Publishes code and artifacts; the formalization subsumes classical 1‑categorical cases and mechanizes the lifting/transport arguments that make the higher proof go through.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 2:11Category theory in computation
- 6:48Infinity categories
- 9:01Formalizing infinity theory
- 11:29Yoneda lemma in type theory
- 14:18Simplicial extensions in type theory
- 18:19Pre-infinity categories
- 22:16Covariant type families
- 24:26Yoneda lemma proof
- 26:56Contributions
- 29:51Comparison with proof assistants
- 31:19Naturality in base category
- 32:43Strictness vs infinity
- 34:08Q&A
related talks
01h 08mType Arithmetic and the Yoneda Lemma
41mWhat You Needa Know About Yoneda
26m2-Functoriality of Initial Semantics, and Applications
25mCubical Synthetic Homotopy Theory
23mWhy Are Proofs Relevant in Proof-Relevant Models?
02h 24mCategory Theory Track
37mEquivalence Hypergraphs: E-Graphs for Monoidal Theories
23mFormalizing Monoidal Categories and Actions for Syntax with Binders