fact: Definition distributive_lattice : UU := ∑ (X : hSet) (L : lattice X), is_distributive L.
imports: UniMath.Foundations.Preamble UniMath.Algebra.Monoids UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.OrderTheory.Lattice.Complement