[003N] -- Synthetic topos theory

[003N] Observation

Let $$T$$ be a base type theory. We work in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $X_{1}$ be a topos, and let $X_{2}(x)$ be a topos under assumption $x:X_{1}$ . Then we have the following equivalences.

\mathcal {S}((x:X_{1})\times X_{2}(x),i)

\simeq

{[002Y]}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X_{1})}(\mathord {\textnormal {\textsf {Sp}}})}(y:X_{2}(\mathord {\textnormal {\textsf {w}}}_{X_{1}})\vdash \mathcal {E}(i))

\simeq

{definition}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X_{1})}({}\vdash \mathcal {S}(X_{2}(\mathord {\textnormal {\textsf {w}}}_{X_{1}}),i))