More elegant construction of ZariskiLattice

[MatthiasHu]

Here is an idea for an improvement in ZariskiLattice.Base .

The current set-quotient construction begins by defining a preorder (without using this name) and deriving the equivalence relation _∼_ from that: https://github.com/agda/cubical/blob/6ce70a4934db4dac521c60399183b3b6e1bcf225/Cubical/Algebra/ZariskiLattice/Base.agda#L72-L83

So the set-quotient is actually an instance of a general (not formalized yet, I think) preorder-to-poset construction. I propose to actually implement it as such and then to use the resulting poset structure to define the lattice structure more easily.

Advantages:

• Because meets and joins in a poset are unique, we only need to show mere existence and don't need to prove the well-definedness of the _∨z_ and _∧z_ operations.
• We don't need to prove any of the monoid axioms (assoc, comm, L/Rid) on _∨z_ and _∧z_ by hand, only the distributive law remains.

Prerequisites:

• the preorder-to-poset construction (perhaps in Order.Preorder.Properties)
• the poset-plus-finite-meets/joins-to-lattice construction

[MatthiasHu]

@mzeuner What do you think?

[mzeuner]

Sorry for the late reply. I guess there is a general question about whether we want a (bounded) distributive lattice to be a poset with induced joins and meets or an algebraic structure with an induced order. I went for the latter when setting everything up, but I'm not sure anymore that that was the right choice. So I'm all for trying the other approach.