2023/09/15 by Nikolai Kudasov, Emily Riehl, Kudasov, Nikolai +3 · 3 citations
Mathematics · #Algebraic Topology (math.AT) #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2309.08340
openalex publication_date 2023/09/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
Formalized 1-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have "higher structure," rely on infinite-dimensional categories in place of 1-dimensional categories, and ∞-category theory has thusfar proved unamenable to computer formalization. Using a new proof assistant called Rzk, which is designed to support Riehl-Shulman's simplicial extension of homotopy type theory for synthetic ∞-category theory, we provide the first formalizations of results from ∞-category theory. This includes in particular a formalization of the Yoneda lemma, often regarded as the fundamental theorem of category theory, a theorem which roughly states that an object of a given category is determined by its relationship to all of the other objects of the category. A key feature of our framework is that, thanks to the synthetic theory, many constructions are automatically natural or functorial. We plan to use Rzk to formalize further results from ∞-category theory, such as the theory of limits and colimits and adjunctions.