von Neumann-Bernays-Gödel set theory (NBG) is a conservative extension of ZFC which contains "classes" (such as the class of all sets) as basic objects. "Conservative" means that anything provable in NBG *about sets* can also be proven in ZFC. The essential properties which make this true (as opposed to, say, Morse-Kelley set theory, which is not conservative) are that classes cannot be elements of other classes (in particular, powerclasses and function classes do not exist), and class comprehension is "predicative", i.e. quantified variables can range only over sets.

My question is, can the operation "ZFC → NBG" be iterated? Can we add to NBG new basic objects called (say) "2-classes" (such as the 2-class of all classes), which can contain classes as elements (but not other 2-classes), and where 2-class comprehension can use quantified variables that range over classes, but not over 2-classes? (Well, obviously, we *can*, but the real question is whether it would be conservative over NBG, hence also over ZFC.)

Background: I am wondering about this as a foundation for category theory. Most "large" categories which arise in mathematics, outside of category theory itself, can be defined in NBG (or even in ZFC, sort of, using the usual trick of representing proper classes by the first-order formulas defining them). But in category theory, we sometimes want to study things like "the category of large categories" or "the functor category between two large categories," which cannot be defined in NBG or ZFC. The usual solution is to assume a Grothendieck universe (or inaccessible cardinal), but this seems somewhat extravagant, since most of these new beasts only live "one more level up" from the classes in NBG. So I wonder whether we can get away with a further conservative extension of this sort.