[ refactor ] Restate, and use, the definitions of `Monotonic` etc. operations

[jamesmckinna]

Aim: towards tackling #1579

TODO:

• [x] introduce the relevant definitions and consequences
• [x] deploy in Data.Nat.* UPDATED: unsolved metas suggest some more revision is necessary :-(
• [x] deploy in Data.Integer.*
• [x] deploy in Data.Rational.*
• [ ] make the breaking changes (v3.0: separate PR once the rest is done?)

[JacquesCarette]

Thanks - these already are easier to understand.

[jamesmckinna]

How do I remove #1579 from the Development sidebar entry?

[MatthewDaggitt]

How do I remove https://github.com/agda/agda-stdlib/issues/1579 from the Development sidebar entry?

Not sure how you did it, but it's gone for me :tada:

[jamesmckinna]

Now that the abstract definitions are mostly in place, can look at the instantiations in Data.Nat etc. Still questions in mind, as ever, about implicit/explicit quantification in Left/RightMonotonic, plus dependency on Relation.Binary adding one additional layer of indirection (cf. #2573 #2566 etc.) so a nudge from reviewers would be welcome before proceeding...

[jamesmckinna]

Remark: all of the Data.X.Properties module duplicate the same abstract proof that (anti-)monotonicity implies distributivity over (lub)glb... so we should downstream lift that argument out once and for all? etc. DRY

[jamesmckinna]

So this should now be ready, modulo:

• reconsideration of Left/Right ... so no breaking changes for this PR cf. #2532
• refactoring towards _-AlmostMonotonic, on the model of #2573

[jamesmckinna]

I'll resolve the merge conflict later, meanwhile tricky questions above needing more thought... ;-)... so have converted back to DRAFT.

[jamesmckinna]

Have fixed the merge conflict, and... not sure what else to do! Maybe it can still be improved wrt implicits?

[JacquesCarette]

Just needs a second reviewer.