  We present a method to construct "native" type systems for a broad class of
languages, in which types are built from term constructors by predicate logic
and dependent types. Any language with products and functions can be modelled
as a higher-order algebraic theory with rewrites, and the internal language of
its presheaf topos provides total specification of the structure and behavior
of terms. This construction is functorial, so translations of languages give
translations of type systems. The construction therefore provides a shared
framework of higher-order reasoning for most existing programming languages.
