fact: Definition boolean_algebra (X : hSet) := ∑ L : bounded_lattice X, is_boolean L.
imports: UniMath.Foundations.Preamble UniMath.Algebra.Monoids UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.OrderTheory.Lattice.Complement UniMath.OrderTheory.Lattice.Distributive UniMath.OrderTheory.Lattice.Heyting