A Formalization of the Algebraic Small Object Argument in UniMath

Abstract

Model categories, introduced by Quillen in 1967, form the cornerstone of modern homotopy theory, providing a language and tools for this branch of mathematics. They consist of two interacting weak factorization systems. Quillen defined a transfinite construction to generate weak factorization systems and thereby model structures on a category, given sufficiently well-behaved classes of maps: the small object argument. Weak factorization systems, lacking algebraic structure, suffer some defects from a categorical point of view. Grandis and Tholen introduced the notion of natural weak factorization system to rectify these issues. Garner pointed out some problematic aspects of the small object argument: that it is not convergent, that it is not related to other known transfinite constructions and that it satisfies no universal property. He refined the small object argument to generate natural weak factorization systems in a more algebraically coherent way. In this thesis, we elaborate, rephrase and formalize Garner’s ‘algebraic’ small object argument. The formalization is written using the Coq proof checker, using the UniMath library. This is a formalization framework based on Homotopy Type Theory (HoTT). The formalization provides an air-tight confirmation of the theory through computer verified proofs. We fill in the details in Garner’s construction, add much needed intuition and redefine parts of the construction to be more direct and accessible. We rephrase the theory in more modern language, using constructions like displayed categories and a modern, less strict notion of monoidal categories, so that it is fit for formalization. We point out the interaction between the theory and the HoTT foundations, and describe some of the constructive issues we come across.