Russell developed  type theory in response to his discovery of a paradox in naive set theory. In his ramified type theory mathematical objects are classified according to their types: the type of propositions, the type of objects, the type of properties of objects, etc. When Church developed his  simple theory of types on the  basis of a typed version of his lambda calculus he added the rule that there is a type of functions between any two types of the theory. Intuitionistic type theory further extends the simply typed lambda calculus with dependent types, that is, indexed families of types. An example is the family of types of \(n\)-tuples indexed by \(n\).