AI 中文总结
本文发展2-拓扑斯理论，证明任意2-拓扑斯含直觉主义ZF模型，无适当大小限制时会出现Burali-Forti型悖论，还借助拓扑斯草图构造集合论全域，并与代数集合论建立联系。
AI 中文摘要
本文继续发展初等2-拓扑斯理论，这是一种基于范畴2-范畴公理化的基础理论。我们证明任意2-拓扑斯都包含直觉主义ZF集合论的模型，并利用这一点说明：若不施加适当的大小限制，则可从2-拓扑斯公理推导出Burali-Forti型悖论。该集合论全域是一般构造的特例，此一般构造给出任意有限高阶理论在2-拓扑斯中的内部模型范畴，而该构造又借助“拓扑斯草图”概念完成。作为构造的副产品，我们还与“代数集合论”建立联系，引入从“类范畴”构造集合论全域的新方法。
英文摘要
This paper continues the development of (elementary) 2-topos theory, a foundational theory based on an axiomatization of the 2-category of categories. We prove that any 2-topos contains a model of intuitionistic ZF set theory, and we use this to show that, if appropriate size restraints are not imposed, then a Burali-Forti type paradox can be deduced from the 2-topos axioms. The set-theoretic universe is produced as a special case of a general construction giving an internal category of models in a 2-topos of an arbitrary finite higher-order theory, which in turn is carried out using a notion of "topos sketch". As a byproduct of our construction, we also make contact with the subject of "algebraic set theory", introducing a novel approach to the construction of set-theoretic universes from a "category of classes".
Comments105 pages
