Let \(T\) be a base type theory. We work in \(T\). We define the topos of types \(\mathcal {E}\) to be \(\mathcal {E}(0)\).