Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a subtopos. Then the constant sheaf and global section adjunction for \(X\) yields a lex modality on \(\mathcal {U}(0)\). We refer to the lex modality as \(\mathord {\textnormal {\textsf {m}}}_{X}\).