This file defines symmetric powers of a type. The nth symmetric power consists of homogeneous n-tuples modulo permutations by the symmetric group.
The special case of 2-tuples is called the symmetric square, which is
addressed in more detail in
TODO: This was created as supporting material for
needs a fleshed-out interface.
The nth symmetric power is n-tuples up to permutation. We define it
as a subtype of
multiset since these are well developed in the
library. We also give a definition
sym.sym' in terms of vectors, and we
show these are equivalent in
Multisets of cardinality n are equivalent to length-n vectors up to permutations.