@John, thanks for that. It strikes me that this looks very much like the comparison functor between monoids (on a set) and T-algebras, in that we start with a set + associative binary operation + unit and end up with a set + an n-ary operation for each n + a whole bunch of generalised associative laws. Would it be right to say strictification is a "categorification" of this operation on plain monoids?