Aspects of predicative algebraic set theory II: Realizability

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