Let \(T\) be a base type theory. We work in \(T\). We say a topos \(X\) is a subtopos (of \(\mathord {\textnormal {\textsf {1}}}\)) if the counit of the constant sheaf and global section adjunction for \(X\) is an equivalence. We write \(\mathord {\textnormal {\textsf {SubTop}}}\) for the type of subtoposes.