谓词代数集论II的几个方面：可实现性
Aspects of Predicative Algebraic Set Theory II: Realizability
摘要：
这是第二次在一系列文件之间的关系代数集合论和谓词形式系统。在第一部分中，我们引入了小映射的谓词范畴的概念，并得到了这样的范畴总是包含一个集合论模型的结果。在本文中，我们表明，熟悉的可实现性模型的建设性集合论CZF和IZF可以得到作为一个应用程序的这一结果。为了这个目的，我们表明，谓词范畴与小地图是封闭的内部概念的可实现性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
