Formalizing the $\infty$-Categorical Yoneda Lemma

TL;DR

This paper presents the first formalization of the $ extinfty$-categorical Yoneda lemma using a new proof assistant, Rzk, which supports synthetic $ extinfty$-category theory, enabling rigorous computer-verified results in higher category theory.

Contribution

It introduces Rzk, a novel proof assistant designed for synthetic $ extinfty$-category theory, and formalizes the Yoneda lemma within this framework, advancing formalization in higher category theory.

Findings

First formalization of $ extinfty$-categorical Yoneda lemma

Supports automatic naturality and functoriality in constructions

Lays groundwork for formalizing limits, colimits, and adjunctions in $ extinfty$-categories

Abstract

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 $\infty$-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 $\infty$-category theory, we provide the first formalizations of results from $\infty$-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 $\infty$-category theory, such as the theory of limits and colimits and adjunctions.