Derived operators in the theory of Relation.Binary.Structures.IsTotalOrder

[jamesmckinna]

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.

[jamesmckinna]

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)

[MatthewDaggitt]

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...

[jamesmckinna]

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?

[MatthewDaggitt]

Happy with either approach.

[jamesmckinna]

Closing for the time being: more thought required!