A Formalization of Functor Quasi-Categories in Lean 4

Abstract

This thesis presents a complete formalization, in the Lean 4 proof assistant, of the result that the internal hom between quasi-categories, known as the functor quasi-category, is itself a quasi-category. Quasi-categories provide a combinatorial model for ∞-categories, and the functor quasi-category models the ∞-category of functors between them.Toward this goal, and following the proofs presented by Lurie in [15] and Rezk in [21], many non-trivial results in simplicial homotopy theory are formalized regarding simplicial sets, lifting properties, saturated collections of morphisms, and inner anodyne maps. This work represents one of the first formalizations of quasi-category theory within an interactive theorem prover. It establishes a foundation for further development of ∞-category theory in Lean and constitutes a key milestone toward the formalization of the ∞-cosmos of quasi-categories, as defined by Riehl and Verity in [24].