Let \(T\) be a base type theory. We work in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\) and let \(X\) be a topos. We define the category \(\mathcal {S}(X,i)\) of sheaves on \(X\) of level \(i\) to be \(\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sp}}}}(x:X\vdash \mathcal {E}(i))\).