Aspects of Predicative Algebraic Set Theory II: Realizability

TL;DR

This paper explores how realizability models of constructive set theories like CZF and IZF can be derived within predicative algebraic set theory, demonstrating the closure of predicative categories with small maps under realizability.

Contribution

It extends the framework of predicative algebraic set theory by showing realizability models can be constructed within it, linking algebraic and realizability approaches.

Findings

Realizability models of CZF and IZF can be obtained from predicative categories.

Predicative categories with small maps are closed under an internal notion of realizability.

The approach unifies algebraic set theory with realizability models.

Abstract

This is the second in a series of papers on the relation between algebraic set theory and predicative formal systems. In part I, we introduced the notion of a predicative category of small maps and obtained the result that such categories always contain a model of set theory. In the present paper, we show that the familiar realizability models of the constructive set theories CZF and IZF can be obtained as an application of this result. For this purpose, we show that predicative categories with small maps are closed under an internal notion of realizability.