We now present a core version of intuitionistic type theory, closely related to the first version of the theory presented by Martin-Löf in 1972 (Martin-Löf 1998 [1972]). In addition to the type formers needed for the Curry-Howard interpretation of typed intuitionistic predicate logic listed above, we have two types: the type \(\N\) of natural numbers and the type \(\U\) of small types.