Formalizing colimits in Cat
Mario Carneiro, Emily Riehl
math.CT
Mar 26, 2025 · v1
TL;DR
Formalizes the homotopy category functor and cocompleteness of Cat in Lean's Mathlib to support future infinity-category work.
Abstract
Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite $\infty$-category theory has not been formalized. To support future work on formalizing $\infty$-category theory in Lean's mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that Cat has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete.
Problem
Formalizing infinity-category theory requires prerequisite constructions in 1-category theory that have not been available in proof assistants. In particular, the cocompleteness of the category of categories (Cat) and the properties of the nerve functor were not formalized.
Approach
The authors formalize in Lean's Mathlib the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. They prove the adjunction is reflective, which yields that Cat has colimits. The formalization works within Lean's existing simplicial set and category theory infrastructure.
Results
This is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete, laying groundwork for future formalization of infinity-category theory.
