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 concerned unfounded or is there a way to avoid any potential issues with such statements?