Realistically though, when is == not (at least) an equivalence relation?
Realistically, and in this context, when the two sides are not of the same type.
In most of the cases that I care about, there is some underlying type like "string" or "integer", on which an equivalence relation exists in some formal sense. Then there are some concrete C++ types like std::basic_string<char,allocator_1> or std::basic_string<char,allocator_2> or int32_t or int64_t. operator== is defined on pairs of these concrete types in some way that approximates to the equivalence relation on the underlying formal type, but with some inevitable flakiness at the edges, such as comparison between two char*s or comparison between integers with different numbers of bits.
Sure, but these types are inherently related. It should be reasonable to write the semantics of comparisons on related types in terms of the underlying type (or more abstract type, I guess). I can convince myself that those operations on those types have precise semantics: they define an equivalence relation. We attach meaning to symbols. I doubt that many people on this list would read the expression "a == b" as "a and b are operated on by some function with the name == that has some result". I tend to read it as "a is equal to b". If I read it that way, I happen to know something extra about the operator; it's an equivalence relation. I also happen to know something about the values: an expression involving a will yield the same result as the same expression involving b (with some notable exceptions). This additional knowledge seems like a good thing. I don't see how attaching specific meaning to operations impacts implementation flexibility. It certainly impacts design choices and choices about algorithm usage, but I hope in a positive way.