arXiv · 2607.13327
The Constant Domain Axiom in Toposes
Abstract
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.
Explore related subjects
Keep this discovery
Jérémie Marquès. 2026-07-14. The Constant Domain Axiom in Toposes. https://arxiv.org/abs/2607.13327
Cite the original work for its findings. Save a collection to share your selection of sources.