Add a concrete, precise type for symmetries?

[kindaro]

There is a way to define symmetries of finite sets not as pairs of hopefully inverse functions, but as concrete values. The magic of generalized algebraic data types lets us do it precisely. This is my draft. There are some property checks too.

It is not too hard to understand how to encode any permutation with this type. With a suitable notation, maybe it will even look good. Another advantage is that there is no «hopefully» — this definition is precise.