Documentation

The product/composition of u and v: if w = u compose v then w `at ` i = v `at` (u `at` i).

The (left) group action of Perm on itself: if w = u act v then w `at ` (u `at` i) = v `at` i.