  Native type systems are those in which type constructors are derived from
term constructors, as well as the constructors of predicate logic and
intuitionistic type theory. We present a method to construct native type
systems for a broad class of languages, lambda-theories with equality, by
embedding such a theory into the internal language of its topos of presheaves.
Native types provide total specification of the structure of terms; and by
internalizing transition systems, native type systems serve to reason about
structure and behavior simultaneously. The construction is functorial, thereby
providing a shared framework of higher-order reasoning for many languages,
including programming languages.
