The category of lattices #
Lat, the category of lattices.
Lat doesn't correspond to the literature definition of [
(https://ncatlab.org/nlab/show/Lat) as we don't require bottom or top elements. Instead,
The free functor from
X → WithTop (WithBot X).