 In such a context, the distinction between meta-syntactic and syntactic readings of ‘type’ is not very important. Even if ‘type’ is taken to be a purely metatheoretic notion, the axioms and rules of inference of type theory enable us to prove meta-theorems about types. The situation can be compared to the relation between sequent calculus and natural deduction, with the turnstile \(\vdash\) of the former interpretable as a relation of derivability in some underlying natural deduction system, and the sequent calculus providing higher-order theorems about object language derivability. Thus whether or not one thinks of types as meta-theoretic notions, the calculi of type theory are such that one can prove theorems to the effect that term \(N\) is of type \(\tau\). 