The symmetric square #
This file defines the symmetric square, which is
α × α modulo
swapping. This is also known as the type of unordered pairs.
More generally, the symmetric square is the second symmetric power
data.sym.basic). The equivalence is
From the point of view that an unordered pair is equivalent to a
multiset of cardinality two (see
sym2.equiv_multiset), there is a
sym2.mem, which is a
h : a ∈ z for
z : sym2 α, then
h.other is the other
element of the pair, defined using
decidable equality, then
h.other' computably gives the other element.
Recall that an undirected graph (allowing self loops, but no multiple
edges) is equivalent to a symmetric relation on the vertex type
Given a symmetric relation on
α, the corresponding edge set is
sym2.from_rel which is a special case of
The symmetric square has a setoid instance, so
⟦(a, b)⟧ denotes a
term of the symmetric square.
symmetric square, unordered pairs, symmetric powers
Declarations about membership #
This is a predicate that determines whether a given term is a member of a term of the
symmetric square. From this point of view, the symmetric square is the subtype of
cardinality-two multisets on
Declarations about symmetric relations #
Equivalence to the second symmetric power #
The symmetric square is equivalent to length-2 vectors up to permutations.
Get the other element of the unordered pair using the decidable equality.
This is the computable version of