The inductive definability of types is inherent in the meaning explanations of intuitionistic type theory which we shall discuss in the next section. In fact, intuitionistic type theory can be described briefly as a theory of inductive, recursive, and inductive-recursive definitions based on a framework of lambda calculus with dependent types.