Relation.Binary.Bundles.Preorder declares the 'wrong' symbol for the ordering relation!!!

[jamesmckinna]

Preorders are rarely Symmetric, unless they arise already from instances of Setoid/IsEquivalence.

So... why in the name of all that is holy do we declare them with a field name _∼_ which is (notationally/syntactically/formally) symmetric.

Consequences:

• the converse (treated in Relation.Binary.Properties.Preorder) can't have a 'flipped' notation, so we have to make do with the (semantically) flipped definition of the converse relation;
• the (underlying relation of the) converse of a Poset is declared in Relation.Binary.Properties.Poset, when that could simply be a renaming of the converse from Relation.Binary.Properties.Preorder, were that to be able to have a notation (qua definition, or else as syntax declaration);
• my head exploded while working on Add _≮_ and _≰_ to bundles in the binary relation hierarchy. #1214 / [fixes #1214] Add negated ordering relation symbols systematically to Relation.Binary.* #2095 as a result...

Refactoring PROPOSAL: that we rename (and appropriately deprecate, groan) the infix symbol/definition _∼_ to be _≲_, which becomes _≤_ in Poset, etc... and whose Relation.Binary.Properties.Preorder.InducedEquivalence be given by @laMudri 's Relation.Binary.Construct.Interior.Symmetric from #2071 applied to _≲_...

Just sayin'.

[laMudri]

I agree that _∼_ is a bad name and plain old _≤_ would be much better. Unfortunately, I think this is inevitably a breaking change because of all the record { _∼_ = Leq }-like code which exists. At least the error message you get out of that should be somewhat instructive.

[Taneb]

I agree that it's a breaking change. And I think that means if this is something we want to do, we ought to do it now. We're not going to have another major version increment any time soon

[jamesmckinna]

Two/three things to say to this:

• yes, as a major breaking change, I think it's important to do it sooner rather than later (thanks @Taneb !);
• I'm nearly done with the corresponding one for negated symbols, [fixes #1214] Add negated ordering relation symbols systematically to Relation.Binary.* #2095 which exposed to me the larger problem concerning flipped symbols as a whole; out of sheer rage last night I started work on it, but rolled back before I went completely berserk, but a follow-up PR in the spirit of my current one would be... very desirable I think ;-)
• regarding symbols, actually I think that there is value in distinguishing between the Preorder version of the symbol and the Poset version (and that there should be a third one by convention used for your Prosets @laMudri , I think, even if they never actually get materialised as Bundle in their own right...), and chose, somewhat arbitrarily, the one above. But it's a small(er) hill on which to die... perhaps.

[jamesmckinna]

Aaaargh... this may be worse than I hoped/thought/feared. Some great subtleties to do with renaming symbols in the signature of the module of a record, without being able to rename the corresponding defined field/method in a record in the record signature... as a result of which, exported sub-derived records retain the old definition name, even though they can be renamed on opening qua modules... blimey!

[JacquesCarette]

Agree with changing to _≲_ now.

[jamesmckinna]

Closing this now after merge of #2099 . But NB discussion above about deprecation!