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/1011201c5d4886d3b80411e25f2ad0d2f508eab1/Cubical/AlgebraicGeometry/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.

[anshwad10]

Cubical.Algebra.LindenbaumTarski could also use this improvement: It starts with defining a preorder Γ ⊢_⇒_, and then takes the quotient by its symmetric kernel to get a poset (it also subsequently proves that it is a lattice).

[anshwad10]

This can be closed now, as #1191 has been merged.