arXiv · 0801.2305
Aspects of Predicative Algebraic Set Theory II: Realizability
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.
Explore related subjects
Keep this discovery
Benno van den Berg, Ieke Moerdijk. 2008-01-15. Aspects of Predicative Algebraic Set Theory II: Realizability. https://arxiv.org/abs/0801.2305
Cite the original work for its findings. Save a collection to share your selection of sources.