[003F] -- Synthetic topos theory

[003F] Observation

Let $$T$$ be a base type theory. We work in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $A:\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sp}}}}({}\vdash \mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i)))$ , and let $$X$$ be a topos. Then we have the following equivalences.

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sp}}}}(x:X\vdash A)

\simeq

{[002Y]}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})}({}\vdash {X}^{*}(A))

\simeq

{definition}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}({}\vdash \mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sp}}}}({}\vdash {X}^{*}(A)))

\simeq

{definition}

\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}({}\vdash \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}({X}^{*}(A)))

\simeq

{definition}

\mathord {\textnormal {\textsf {Model}}}^{X}(A)