Predicative algebraic set theory

Steve Awodey and Michael A. Warren

In this paper the machinery and results developed in [Awodey et al., 2004] are extended to the study of constructive set theories. Specifically, we introduce two constructive set theories BCST and CST and prove that they are sound and complete with respect to models in categories with certain structure. Specifically, basic categories of classes and categories of classes are axiomatized and shown to provide models of the aforementioned set theories. Finally, models of these theories are constructed in the category of ideals.

Keywords: algebraic set theory, categorical logic, predicativity, ideal completion, dependent type theory, $\Pi$-pretopos, small maps

2000 MSC: 18B05, 18B25, 18C10, 03G30, 03E70, 03F60

Theory and Applications of Categories, Vol. 15, CT2004, No. 1, pp 1-39.

TAC Home