Let \(T\) be a type theory and let \(X\) be a topos in \(T\). Inside \(T\), the type theory of sheaves on \(X\) is referred to as \(\mathord {\textnormal {\textsf {Sh}}}(X)\).