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.