Filtral pretoposes and compact Hausdorff locales

The category of compact Hausdorff locales is a pretopos which is filtral, meaning that every object is covered by one whose subobject lattice is isomorphic to the lattice of filters of complemented elements. We show that any filtral pretopos satisfying some mild additional conditions can be embedded into the category of compact Hausdorff locales. This result is valid in the internal logic of any topos. Assuming the principle of weak excluded middle and the existence of copowers of the terminal object in the pretopos, the image of the embedding contains all spatial compact Hausdorff locales. The notion of filtrality was introduced by V. Marra and L. Reggio (Theory Appl. Categ., 2020) to characterise the category of compact Hausdorff spaces within the class of pretoposes. Our results can be regarded as a constructive extension of the aforementioned characterisation, avoiding reference to points. If the ambient logic is classical, i.e. it satisfies excluded middle, and the prime ideal theorem for Boolean algebras holds, we obtain as a corollary the characterisation of compact Hausdorff spaces in op. cit.