Let \(T\) be a base type theory. We work in \(T\). We refer to the type of lex accessible modalities on \(\mathcal {U}(0)\) as \(\mathord {\textnormal {\textsf {LAM}}}\).