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.