Typeclass for the ⊔ (\lub) notation

Typeclass for the ⊓ (\glb) notation

A semilattice_sup is a join-semilattice, that is, a partial order with a join (a.k.a. lub / least upper bound, sup / supremum) operation ⊔ which is the least element larger than both factors.

A semilattice_inf is a meet-semilattice, that is, a partial order with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation ⊓ which is the greatest element smaller than both factors.

A lattice is a join-semilattice which is also a meet-semilattice.

A distributive lattice is a lattice that satisfies any of four equivalent distribution properties (of sup over inf or inf over sup, on the left or right). A classic example of a distributive lattice is the lattice of subsets of a set, and in fact this example is generic in the sense that every distributive lattice is realizable as a sublattice of a powerset lattice.