Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a subtopos. Then the lex modality \(\mathord {\textnormal {\textsf {m}}}_{X}\) is accessible. (This might require additional axioms.)
Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a subtopos. Then the lex modality \(\mathord {\textnormal {\textsf {m}}}_{X}\) is accessible. (This might require additional axioms.)