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.