Formalizing the $\infty$-Categorical Yoneda Lemma

Nikolai Kudasov, Emily Riehl, Jonathan Weinberger

Formalized $1$-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoreti…