AI 中文总结
研究常域直觉主义逻辑在拓扑斯理论中的情况，核心方法是用特定对象取代常量预层，主要贡献是证明这些对象在任何拓扑斯中构成布尔预拓扑斯。
AI 中文摘要
常域直觉主义逻辑在预层拓扑斯中有完备语义，将类型解释为常量预层，谓词解释为任意子预层。本文指出如何将其融入拓扑斯理论，用离散locale时隐蔽且豪斯多夫的对象取代常量预层，称这些对象为“CD”，并证明它们在任何拓扑斯中构成布尔预拓扑斯。
英文摘要
Constant domain intuitionistic logic admits a complete semantics in presheaf toposes, by interpreting sorts as constant presheaves and predicates as arbitrary sub-presheaves. The goal of this note is to point out how this fits in topos theory, replacing constant presheaves with objects that are covert and Hausdorff when considered as discrete locales. We call these objects "CD" and we show that they form a Boolean pretopos in any topos.
Comments3 pages
