TotalOrder needs to be defined on Setoids
Closed this issue · 1 comments
Smaug123 commented
Currently TotalOrder is trichotomous on a set. We need a version that is trichotomous on a setoid instead, so that we can define the notion of an ordered group etc. (Currently any total order on a non-discrete setoid will not be trichotomous because two related members of the setoid need to compare equal.)