The Constant Domain Axiom in Toposes

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.