The notion of an inductive definition is fundamental in intuitionistic type theory. It is a primitive notion and not, as in set theory, a derived notion where an inductively defined set is defined impredicatively as the smallest set closed under some rules. However, in intuitionistic type theory inductive definitions are considered predicative: they are viewed as being built up from below.