A constructive approach to the double-categorical small object argument

TL;DR

This paper provides an explicit, constructive method to generate algebraic weak factorisation systems using double categories, making the classical small object argument applicable in constructive mathematics and related settings.

Contribution

It introduces a constructive construction of the small object argument for algebraic weak factorisation systems via colimits of chains, extending prior theoretical work.

Findings

Explicit construction of factorisations as colimits of chains

Application to constructive settings and proof of effectiveness

Identification of effective Kan fibrations as right classes

Abstract

Bourke and Garner described how to cofibrantly generate algebraic weak factorisation systems by a small double category of morphisms. However they did not give an explicit construction of the resulting factorisations as in the classical small object argument. In this paper we give such an explicit construction, as the colimit of a chain, which makes the result applicable in constructive settings; in particular, our methods provide a constructive proof that the effective Kan fibrations introduced by Van den Berg and Faber appear as the right class of an algebraic weak factorisation system.