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

TL;DR

This paper constructs a constructive algebraic weak factorisation system on 01-substitution sets, clarifying the nature of Kan fibrations and addressing the J computation rule issue in cubical set models.

Contribution

It provides a constructive proof of an algebraic weak factorisation system on 01-substitution sets, linking R-algebras to Kan fibrations with filling operations.

Findings

Constructed an algebraic weak factorisation system constructively.

Identified the relationship between R-algebras and Kan fibrations.

Suggested a fix for the missing J computation rule in cubical models.

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 factorization 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.