Synthetic topos theory
[004W] Observation

Let \(T\) be a base type theory. We work in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\) and let \(A:\mathcal {U}(0)\). By [002S], it corresponds to \(\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sp}}}}(A):\mathcal {E}(0)\) which is a topos. Then we have the following equivalences.

\(\mathcal {S}(\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sp}}}}(A),i)\)\(\simeq \) {adjointness}\(A\rightarrow \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}(\mathcal {E}(i))\)\(\simeq \) {[002S]}\(A\rightarrow \mathcal {U}(i)\)