BoundedLattice is a poor match with Algebra.Lattice

[Taneb]

In Algebra.Bundles, we have the definition BoundedLattice = IdempotentCommutativeMonoid. This has different naming conventions to the definitions in Algebra.Lattice.Bundles, and is equivalent to a bounded semilattice. It also prevents us from defining a lattice with both a join and a meet bound under that name.