[0028] Type theory of sheaves

Let $$T$$ be a type theory and let $$X$$ be a topos in $$T$$ . We introduce the type theory of sheaves on $$X$$ . It is a type theory internal to $$T$$ .

[002K] Notation

Let $$T$$ be a type theory and let $$X$$ be a topos in $$T$$ . Inside $$T$$ , the type theory of sheaves on $$X$$ is referred to as $\mathord {\textnormal {\textsf {Sh}}}(X)$ .

[002G] Rule

Let $$T$$ be a type theory and let $$X$$ be a topos in $$T$$ . Then the type theory of sheaves on $$X$$ is a base type theory.

[002H] Rule

Let $$T$$ be a type theory and let $$X$$ be a topos in $$T$$ . Then the type theory of sheaves on $$X$$ has all products and coproducts.