Let \(T\) be a type theory. We work in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\) and let \(X\) be a topos. We define the global section functor

\(\Gamma _{X}:\mathcal {S}(X,i)\rightarrow \mathcal {U}(i)\) by the following composite. \(\mathcal {S}(X,i)\)\(\simeq \) {[003G]}\(\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}({}\vdash \mathcal {U}(i))\)\(\rightarrow \) {\(\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}\)}\(\mathcal {U}(i)\) By [002R], \(\Gamma _{X}\) has a left adjoint which we call the constant sheaf functor and is denoted by \(\Delta _{X}\).