[003G] -- Synthetic topos theory

[003G] Observation

Let $$T$$ be a type theory. We work in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ and let $$X$$ be a topos. Then we have the following equivalences.

\mathcal {S}(X,i)

\simeq

{[003F]}

\mathord {\textnormal {\textsf {Model}}}^{X}(\mathcal {E}(i))

\simeq

{[002S]}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}({}\vdash \mathcal {U}(i))