In Aczel's Constructive Set Theory (CZF), no non-degenerate complete lattice can be proved to be a set. There are hallmark examples of complete lattices that are proper classes in CZF, including the Dedekind–MacNeille completion of a lattice/poset.

Is there a way to talk about the collection of Complete Lattices in CZF without introducing a hierarchy? This may seem like a splitting of hairs but I’m concerned about making statements about “all complete heyting algebras”. Is this concern unfounded or is there a way to avoid any potential issues with such statements?

i.e.its top and bottom elements are the same ($0=1$). Curi's argument works by showing from GUP that if a complete lattice $L$ is a set, there exists an element $a$ such that $a = \bigvee \emptyset$ and $a = \bigvee L$, so $0 = a = 1$. Therefore every complete lattice that is a set is a singleton, under GUP. $\endgroup$provethat no non-degenerate complete lattice is a set; it is onlyconsistentwith CZF that this holds. But on the other hand, classical ZF isalsoconsistent with CZF, and then a plethora of complete lattices that are sets exists. I corrected it using another formulation if you don’t like “not necessarily” for some reason. $\endgroup$