  Using recent results in topos theory, two systems of higher-order logic are
shown to be complete with respect to sheaf models over topological
spaces---so-called ``topological semantics''. The first is classical
higher-order logic, with relational quantification of finitely high type; the
second system is a predicative fragment thereof with quantification over
functions between types, but not over arbitrary relations. The second theorem
applies to intuitionistic as well as classical logic.
