The first example of such an inductive-recursive definition is an alternative formulation à la Tarski of the universe of small types. Above we presented the universe formulated à la Russell, where there is no notational distinction between the element \(A {:} \U\) and the corresponding type \(A\). For a universe à la Tarski there is such a distinction, for example, between the element \(\hat{\N} {:} \U\) and the corresponding type \(\N\). The element \(\hat{\N}\) is called the code for \(\N\).