[003A] The category of sheaves

Sheaves on a topos are identified with morphisms to the universe of étale types.

[003B] Definition

Let $$T$$ be a base type theory. We work in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ and let $$X$$ be a topos. We define the category $\mathcal {S}(X,i)$ of sheaves on $$X$$ of level $$i$$ to be $\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sp}}}}(x:X\vdash \mathcal {E}(i))$ .

[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))