Sections 2.1 to 2.4 introduce a sequence of approximations to Nuprl , starting with a familiar formalism, the typed lambda calculus. These approximations are not exactly subsets of Nuprl , but the differences between these theories and subtheories of are minor. These subsections take small steps toward the full theory and relate each step to familiar ideas. Section 2.5 summarizes the main ideas and can be used as a starting point for readers who want a brief introduction. The last two sections relate the idea of a type in Nuprl to the concept of a set and to the concept of a data type in programming languages.