The origins of intuitionistic type theory are Brouwer’s intuitionism and Russell’s type theory. Like  Church’s classical simple theory of types  it is based on the lambda calculus with types, but differs from it in that it is based on the propositions-as-types principle, discovered by Curry (1958) for propositional logic and extended to predicate logic by Howard (1980) and de Bruijn (1970). This extension was made possible by the introduction of indexed families of types (dependent types) for representing the predicates of predicate logic. In this way all logical connectives and quantifiers can be interpreted by type formers. In intuitionistic type theory further types are added, such as a type of natural numbers, a type of small types (a universe) and a type of well-founded trees. The resulting theory contains intuitionistic number theory (Heyting arithmetic) and much more.