Bernays–Gödel type theory

We study the type-theoretical analogue of Bernays–Gödel set-theory and its models in categories. We introduce the notion of small structure on a category, and if small structure satisfies certain axioms we can think of the underlying category as a category of classes. Our axioms imply the existence of a co-variant powerset monad on the underlying category of classes, which sends a class to the class of its small subclasses. Simple fixed points of this and related monads are shown to be models of intuitionistic Zermelo–Fraenkel set-theory (IZF).