The Constant Domain Axiom in Toposes

Jérémie Marquès

The Constant Domain Axiom in Toposes

Logic 2026-07-14 v1 Category Theory

Authors: Jérémie Marquès

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.

Keywords

constant domain axiom toposes presheaf semantics intuitionistic logic Boolean pretopos covert objects

Cite

@article{arxiv.2607.13327,
  title  = {The Constant Domain Axiom in Toposes},
  author = {Jérémie Marquès},
  journal= {arXiv preprint arXiv:2607.13327},
  year   = {2026}
}

Comments

3 pages