Commit 2020-07-06 16:58 f06e4e00

feat(data/sym2) Defining the symmetric square (unordered pairs) (#3264) This adds a type for the symmetric square of a type, which is the quotient of the cartesian square by permutations. These are also known as unordered pairs. Additionally, this provides some definitions and lemmas for equalities, functoriality, membership, and a relationship between symmetric relations and terms of the symmetric square. I preferred sym2 over unordered_pairs out of a combination of familiarity and brevity, but I could go either way for naming.