[ draft ] add Galois connections and residuated lattices.

[sstucki]

This PR is not ready to be merged. I think the contents are useful, but there are some problems with the organization of the code (what goes into which module etc.) and I need some help/feedback to address these. In particular:

1. I don't know where the definition and properties of Galois connections should go. They involve both relations/orders and (monotone) functions, so maybe Relation.Binary? If so, where exactly? For now, I put them under Function.

2. Currently, the definition of Galois connection and their properties are in the same file. Following the rest of the stdlib, the properties should probably go into a separate file, but I'm not sure where (depends on point 1).

3. There are definitions for (right-)residuated pomonoids and (right-)residuated semilattices. I put them all in the same file, in the Algebra.Ordered hierarchy, but maybe the semilattices should go into Relation.Binary.Lattice hierarchy?

4. Residuated structures and bundles currently live in the same file. To be consistent with the library, these should be split, but I'm not sure where the resulting modules should live (depends on point 3).

5. The definitions of the residuated structures are biased in several ways:

   • only right-residuated cases are covered explicitly, the left-residuated ones are represented by flipping the operation;
   • for the semilattices, only the join-version is covered, the meet-version is dual;
   • only the multiplication is assumed to be monotone, and only in its first argument, all other monotonicity properties can be derived.

   In theory, this is sufficient, but it may be nicer to have unbiased versions for symmetry. But I don't know how much symmetry is enough symmetry and where to put the biased versions, etc. (This all depends on points 3 and 4).

6. Finally, there are properties of the residuated structures, in separate modules, but these may be in the wrong place too (depends on 3).

[MatthewDaggitt]

@sstucki reviewing this PR has triggered a shift in my thinking about the design of the library. All of your questions result from there being no natural place to put this stuff. In https://github.com/agda/agda-stdlib/issues/1763 I've just proposed creating a new top-level Order module which I think would solve all of these problems you've listed.

Given that, can we wait to see how the discussion around the proposal plays out?

[sstucki]

Given that, can we wait to see how the discussion around the proposal plays out?

Absolutely. I am not in a rush with this one. I think the contents are useful, so I decided to share them, but I fully expect this one to require a lot of work and discussion before it can be merged (including work on loosely related issues). So please prioritize whatever else you deem useful.

[JacquesCarette]

Good stuff! Also: all my comments are already preemptively raised in the PR description.

Opinions:

1. I think Function is a horrible place for the definition of Galois connection. The new Order (if that comes to pass) would be way better.
2. I have the same feeling about 'symmetry'. It's annoying to have to duplicate things, but I think it's even more annoying as a user to work with something that's biased "the wrong way" for one's application.

[jamesmckinna]

Suggest taking this out of v2.0, at least until a resolution (how, exactly?) of #1763 ?

[MatthewDaggitt]

Closing. See discussion https://github.com/agda/agda-stdlib/pull/1759 for details.