Derived operators in the theory of `Relation.Binary.Structures.IsTotalOrder`
jamesmckinna opened this issue · 5 comments
The conclusion I now draw from the discussion of Alex Chapman's Zulip issue is that we should move the definitions of _⊓_ and _⊔_ from Algebra.Construct.NaturalChoice.{Min|Max} to Relation.Binary.Structures.IsTotalOrder (and perhaps their properties!?).
Cf. #2247 / #2251 in the algebraic case, where no IsGroup properties were required in defining _//_/_\\_, by contrast with this case, where the min/max operators require the total property even to be definable.
Hmmm... or perhaps not? #2436 / #2440 seem to turn on the contrast between generic properties of IsTotalOrder, and hand-rolled versions in the case where there is a (more) efficient direct implementation of the operations... so some version of defaulting mechanism... a case for Relation.Binary.Bundles.Biased for the 'generic' case, but specialisable in concrete cases?
(I confess I filed this issue ignorant of the complexities of the API vs. Implementation gymnastics of MinOperator etc. but still might be worth revisiting? Cf DivMod)
Yup, I don't have a coherent story for this, aside from the fact that I deeply don't want to be adding new definitions of operators or relations in anything other than raw bundles...
Yup, I don't have a coherent story for this, aside from the fact that I deeply don't want to be adding new definitions of operators or relations in anything other than raw bundles...
Quite! In which case I might be tempted to leave this open for now, but it might well end up closed as status:won't fix until/unless we find that "coherent story" and a plan to implement? or even: close now with that label?
Happy with either approach.
Closing for the time being: more thought required!