Type theories are formal logic languages. People use formal logic for all sorts of things but mathematics has the longest history. This is where people first defined formal languages and assigned meaning (mathematical meaning.)

Starting from simply typed lambda calculus ("simple type theory", also "higher order logic"), one can make various extensions that make the logic language more expressive. The lambda cube is a way to systematically organize the space of type theories.

Interestingly, the theory has become very relevant for type systems of normal programming languages. Milner invented ML as "meta language" for helping with logic and theorem proving, but it was used widely and today everyone expects generics to work more or less as in System F polymorphic lambda calculus.