Equality on unordered pairs

Let t:Set be a type with an equivalence relation eq:t->t->Prop. We can represent unordered pairs of elements of as elements of the cartesian product t*t, considering the pairs (x,y) and (y,x) as equivalent.
Moreover, if eq is decidable, the equivalence on t*t induced induced by eq and satisfying the property above is decidable too.
Express this construction by a functor taking as argument an arbitrary module M:DecidableType (see Coq's standard library).

Solution

Follow this link
Going home