An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof

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 the resulting awfs and the notion of path object to explain why the J-computation rule is absent from the original cubical set model. We will define an alternative path object, which can be used to implement the J-computation rule in cubical sets.