Pull lattice-like structures out of Algebra, into Algebra.Lattice

[laMudri]

Following this comment, here is an attempt at moving and fixing the definitions of lattice-like structures found in the Algebra part of the library. What exists now is work towards an ideal hierarchy, which was done for clarity and my own convenience. For this to be merged, I'd expect to have better backwards compatibility.

Comments welcome.

[MatthewDaggitt]

Looks mostly pretty good! I'm wondering how we can maximise backwards compatibility somehow though. I think the best bet is to keep old variants around (Algebra.Lattice.Old?), then people don't have to upgrade immediately.

Obviously there's various other files that'll need updating...

[MatthewDaggitt]

@laMudri apologies, was trying to bring this up-to-date and ended up messing up the commits. I've ended up having to force push. I'm happy to take responsibility for merging this in for v2.0.

[MatthewDaggitt]

Hmm actually this is more work then I'd first envisaged. @laMudri any chance you could help out by moving all the lattice constructions in Algebra.Construct to corresponding files in Algebra.Lattice.Construct, e.g.

agda-stdlib/src/Algebra/Construct/DirectProduct.agda

Line 93 in b09525c

semilattice : Semilattice a ℓ₁ → Semilattice b ℓ₂ →

[MatthewDaggitt]

Also a couple of quick points on some of the design decisions. I reverted your change to define IsLattice in terms of two IsSemilattice proofs. As @Taneb found in #1540, defining it in this way results in the record having two different proofs that the equality relation is an equivalence which is often undesirable. In order to keep the ease of constructing it, I've added your original version to a new Algebra.Lattice.Structures.Biased. Hope that's okay?

The second is that aren't we missing the smart constructors for the IsDistributiveLattice? Which ones were you planning on adding?

[laMudri]

If this is for version 2, can't we find a general solution to these redundancy problems? For example, I'd start by taking the isEquivalence field out of IsMagma and putting it into Magma, Monoid, Semiring, &c.

I think any further thought or effort from me on this is going to come next weekend at the earliest. I'm happy to discuss the first point earlier, though, given that I have it in mind.

[MatthewDaggitt]

If this is for version 2, can't we find a general solution to these redundancy problems? For example, I'd start by taking the isEquivalence field out of IsMagma and putting it into Magma, Monoid, Semiring, &c.

Eek that sounds rather drastic. Isn't having a well-formed equality relation part of being a magma etc.? To be honest, with the current design of Agda, I don't think you're ever going to find a solution to all redundancy problems + get 100% usability. I think the best we can probably aim for is consistency and eliminate the worst pain points.

More concretely, ignoring the duplicate equality problem, what advantage does your definition of IsLattice have over the current one + smart constructors?

[MatthewDaggitt]

Well that was unbelievably painful, let's not do that again 😢