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}$.