The category of bounded lattices #
This file defines
BddLat, the category of bounded lattices.
In literature, this is sometimes called
Lat, the category of lattices, because being a lattice is
understood to entail having a bottom and a top element.
- One or more equations did not get rendered due to their size.
The functor that adds a bottom and a top element to a lattice. This is the free functor.