A Constructive Small Object Argument
Paul Seip

Abstract:
The small object argument is an important tool in homotopy theory and recently also in logic. Originally proved by Quillen in 1967, it has evolved significantly over time. In recent work Bourke and Garner proved the most general version of the small object argument thus far, using the notion of cofibrant generation by a double category. Moreover, they proved that this version is sufficient to generate all interesting algebraic weak factorisation systems. However, their proof is not constructively valid. In this thesis we prove a constructive version of Bourke and Garner’s small object argument by restricting to the finitary case. We introduce the notion of a finitary algebraic weak factorisation system, and we identify conditions on a double category under which it generates a finitary AWFS. Two crucial steps in the proof are constructing the free algebra for a finitary pointed endofunctor, and constructing colimits in the category of finitary monads on a cocomplete category. We show that our result is an important step in building a constructive model of homotopy type theory based on effective Kan fibrations, a line of research recently initiated by van den Berg and Faber.