Boolean Lattice

A boolean lattice (or boolean algebra) is a complemented distributive lattice.
This type of algebraic structure captures essential properties of both set operations and logic operations.
The dual of BooleanLattice is involutive.
wishful-thinking
function join_unique_identity(
  lattice: BooleanLattice,
  o: lattice.Element,
  o_is_identity_of_join: (x: lattice.Element) -> Equal(
    lattice.Element,
    lattice.join(x, o),
    x,
  ),
): Equal(lattice.Element, o, lattice.bottom) {
  return equal_rewrite (lattice.Element) {
    lattice.bottom
    by equal_swap(o_is_identity_of_join(lattice.bottom))
    lattice.join(lattice.bottom, o)
    by lattice.join_is_commutative(lattice.bottom, o)
    lattice.join(o, lattice.bottom)
    by lattice.bottom_is_identity_of_join(o)
    o
  }
}
We can define order relation by lattice operations.
TODO Above is the swap of Under
TODO Under is the swap of Above
The terminology, which might be introduced by Russell and Whitehead, is very confusing.
TODO