Typeclass for the ⊤ (\top) notation

Typeclass for the ⊥ (\bot) notation

An order_top is a partial order with a maximal element. (We could state this on preorders, but then it wouldn't be unique so distinguishing one would seem odd.)

An order_bot is a partial order with a minimal element. (We could state this on preorders, but then it wouldn't be unique so distinguishing one would seem odd.)

A semilattice_sup_top is a semilattice with top and join.

A semilattice_sup_bot is a semilattice with bottom and join.

A semilattice_inf_top is a semilattice with top and meet.

A semilattice_inf_bot is a semilattice with bottom and meet.

A bounded lattice is a lattice with a top and bottom element, denoted ⊤ and ⊥ respectively. This allows for the interpretation of all finite suprema and infima, taking inf ∅ = ⊤ and sup ∅ = ⊥.

A bounded distributive lattice is exactly what it sounds like.