Constructive Set Theories and their Category-theoretic Models

This chapter advocates a pragmatic approach to constructive set theory, using axioms based solely on set-theoretic principles that are directly relevant to (constructive) mathematical practice. The aim is to leave the notion of set as unconstrained as possible, while remaining consistent with the ways in which sets are actually used in mathematical practice. Following this approach, the chapter presents theories ranging in power from weaker predicative theories to stronger impredicative ones. The theories considered all have sound and complete classes of category-theoretic models, obtained by axiomatizing the structure of an ambient category of classes together with its subcategory of sets. In certain special cases, the categories of sets have independent characterizations in familiar category-theoretic terms, and one thereby obtains a rich source of naturally occurring mathematical models for (both predicative and impredicative) constructive set theories.