 Assigning types to terms The language of type theory begins with an (infinite) set of type variables (which is assumed to be disjoint from the set of variables of the \(\lambda\)-calculus and from the symbol ‘\(\lambda\)’ itself).  The set of types is made up of type variables and the operation \(\sigma \rightarrow \tau\). Variables in type theory now come with a type annotation (unlike the unadorned term variables of untyped \(\lambda\)-calculus). Typed variables are rendered ‘\(x : \sigma\)’; the intuitive reading is ‘the variable \(x\) has the type \(\sigma\)’. The intuitive reading of the judgment ‘\(t : \sigma \rightarrow \tau\)’ is that the term \(t\) is a function that transforms arguments of type \(\sigma\) into arguments of type \(\tau\). Given an assignment of types to term variables, one has the typing rules: