Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos and let \(a\) be an essential point of \(X\). By definition, the inverse image functor \({a}^{*}:\mathcal {S}(X,0)\rightarrow \mathcal {U}(0)\) has the left adjoint \({a}_{!}\) and thus corepresentable by \({a}_{!}(\mathord {\textnormal {\textsf {1}}})\). We refer to \({a}_{!}(\mathord {\textnormal {\textsf {1}}})\) as \(\mathord {\textnormal {\textsf {e}}}_{a}\).