agda-stdlib Add `_≮_` and `_≰_` to bundles in the binary relation hierarchy.

In lib-1.3 I see _≉_ in Setoid, but I do not find ≰, ≮ (I expect they to be defined via ¬_). I grepped for it in Relation.Binary, Relation.Binary.Construct, and do not find it. Probably it needs to be in Preorder or in PartialOrder. ?

May 23 '20 12:05 mechvel

I'm not sure we have a good symbol for the negation of the order for ~. I'd therefore probably add _≰_ to PartialOrder and _≮_ to StrictPartialOrder for now.

May 26 '20 12:05 MatthewDaggitt

There is now a good symbol for \~n for negated tilde.

Sep 12 '22 13:09 MatthewDaggitt

Any (potential) interaction with any candidate solution to issue #1635?

Sep 30 '22 15:09 jamesmckinna

Hmm yes. The precedence of the candidate solution should be < 4 otherwise it will interfere with both this and the non-negated equality.

Oct 04 '22 13:10 MatthewDaggitt

Now that we have closed #1635, would precedence level = 4 suffice? Currently each of _≈_ , _≉_ , and _∼_ are declared at level 4...

Sep 15 '23 11:09 jamesmckinna

Oh, but this has turned out to be more complicated than I first realised... ... and immediately gives rise to the linked issue #2096... and hence (the need/desire for) further refactoring in the same spirit #2098 to introduced notation systematically for the flipped relations... see #2099 for an opening bid on that.

Sep 16 '23 07:09 jamesmckinna