Geodesic
Predicative algebraic set theory
Theory and applications of categories, CT2004, Tome 15 (2005), pp. 1-39

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

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.

Classification : 18B05, 18B25, 18C10, 03G30, 03E70, 03F60
Keywords: algebraic set theory, categorical logic, predicativity, ideal completion, dependent type theory, $\Pi$-pretopos, small maps 
@article{TAC_2005_15_a0,
     author = {Steve Awodey and Michael A. Warren},
     title = {Predicative algebraic set theory},
     journal = {Theory and applications of categories},
     pages = {1--39},
     publisher = {mathdoc},
     volume = {15},
     year = {2005},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2005_15_a0/}
}
TY  - JOUR
AU  - Steve Awodey
AU  - Michael A. Warren
TI  - Predicative algebraic set theory
JO  - Theory and applications of categories
PY  - 2005
SP  - 1
EP  - 39
VL  - 15
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_2005_15_a0/
LA  - en
ID  - TAC_2005_15_a0
ER  - 
%0 Journal Article
%A Steve Awodey
%A Michael A. Warren
%T Predicative algebraic set theory
%J Theory and applications of categories
%D 2005
%P 1-39
%V 15
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_2005_15_a0/
%G en
%F TAC_2005_15_a0
Steve Awodey; Michael A. Warren. Predicative algebraic set theory. Theory and applications of categories, CT2004, Tome 15 (2005), pp. 1-39. http://geodesic.mathdoc.fr/item/TAC_2005_15_a0/