This core intuitionistic type theory is not only the original one, but perhaps the minimal version which exhibits the essential features of the theory. Later extensions with primitive identity types, well-founded tree types, universe hierarchies, and general notions of inductive and inductive-recursive definitions have increased the proof-theoretic strength of the theory and also made it more convenient for programming and formalization of mathematics. For example, with the addition of well-founded trees we can interpret the Constructive Zermelo-Fraenkel Set Theory \(\CZF\) of Aczel (1978 [1977]). However, we will wait until the next section to describe those extensions.