#
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.

http://www.tac.mta.ca/tac/volumes/15/1/15-01.dvi

http://www.tac.mta.ca/tac/volumes/15/1/15-01.ps

http://www.tac.mta.ca/tac/volumes/15/1/15-01.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/15/1/15-01.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/15/1/15-01.ps

TAC Home