An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof #
On page 2 of the paper, Perm(𝔸) is the set of all finite permutations of 𝔸, i.e., the set of permutations π such that π a = a for all but finitely many a. We show that Perm(𝔸) is closed under composition and contains the identity.