Finished proof of inj-surj factorisation (without uniqueness)
Defined generators of simplex category