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

by ANDREW SWAN, JLA 2016

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.

def moved {A : Type} (f : A → A) : Set A

Equations

• moved f = {a : A | f a ≠ a}

def perm (A : Type) : Set (A → A)

Equations

• perm A f = (Function.Bijective f ∧ Finite ↑(moved f))

theorem perm_comp {A : Type} (f : ↑(perm A)) (g : ↑(perm A)) : ↑f ∘ ↑g ∈ perm A

theorem id_perm {A : Type} : id ∈ perm A