Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos. Suppose that the functor

\(\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}:\mathcal {U}(0)\rightarrow \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathcal {U}(0))\) is an equivalence of categories. Then \(X\) is contractible.