Abstract
One of the main goals of this paper is to give a construction of realizability models for predicative constructive set theories in a predicative metatheory. We will use the methods of algebraic set theory, in particular the results on exact completion from van den Berg and Moerdijk (2008) [5]. Thus, the principal results of our paper are concerned with the construction of an extension of a category with small maps by a category of assemblies, again equipped with a class of maps, and to show that this extension construction preserves those axioms for a class of maps necessary to produce models of the relevant set theories in the exact completion of this category of assemblies
Original language | English |
---|---|
Pages (from-to) | 1916-1940 |
Number of pages | 25 |
Journal | Theoretical Computer Science |
Volume | 412 |
Issue number | 20 |
DOIs | |
Publication status | Published - 2011 |