is the category whose objects are complete lattices and whose morphisms are complete lattice homomorphisms, that is functions which preserve all joins and meets (including the bottom and top elements). is a subcategory of Pos.
is given by a variety of algebras, or equivalently by an algebraic theory, so it is an equationally presented category; however, it requires operations of arbitrarily large arity. In fact, it is not a monadic category (over Set), because it lacks some free objects. Specifically, the free complete lattice on a set , while it exists (by general abstract nonsense) as a class, is small only if has at most elements (in which case it is finite and equals the free lattice on ).
For all practical purposes, is not available in predicative mathematics. The definition goes through, but we cannot prove that has any infinite objects. (More precisely, the power class of a nontrivial small complete lattice must also be small.) Generally speaking, predicative mathematics treats infinite complete lattices only as large objects.
In impredicative constructive mathematics, it no longer holds that the free complete lattice on a set with at most elements equals the free lattice on that set. In particular, the free complete lattice on the empty set is the set of truth values, while the free lattice on the empty set is the set of decidable truth values. (I'm not sure whether the free complete lattice on or elements is even small.)
In predicative constructive mathematics, even the free complete lattice on the empty set is a proper class.