As Edward says, there is representational equality too, and we want both a constraint and a data type for it. Currently the constraint looks like
Coercible a b
but and the data type is currently called EqR. Linking them more tightly could be a Good Thing. For example, we could hav
a ~~ b
for the constraint and
a :~~: b
for the data type. I do not have strongly feelings; just pointing out the correspondences.
Simon