An algebraic weak factorisation system on 01-substitution sets: a constructive proof

Abstract

We will construct an algebraic weak factorisation system on the category of 01-substitution sets such that the R-algebras are precisely the Kan fibrations together with a choice of Kan filling operation. The proof is based on Garner's small object argument for algebraic weak factorisation systems. In order to ensure the proof is valid constructively, rather than applying the general small object argument, we give a direct proof based on the same ideas. We use this us to give an explanation why the J-computation rule is absent from the original cubical set model and suggest a way to fix this.