Intuitionistic type theory can be considered as an extension of first-order logic, much as higher order logic is an extension of first order logic. In higher order logic we find some individual domains which can be interpreted as any sets we like. If there are relational constants in the signature these can be interpreted as any relations between the sets interpreting the individual domains. On top of that we can quantify over relations, and over relations of relations, etc. We can think of higher order logic as first-order logic equipped with a way of introducing new domains of quantification: if \(S_1, \ldots, S_n\) are domains of quantification then \((S_1,\ldots,S_n)\) is a new domain of quantification consisting of all the n-ary relations between the domains \(S_1,\ldots,S_n\). Higher order logic has a straightforward set-theoretic interpretation where \((S_1,\ldots,S_n)\) is interpreted as the power set \(P(A_1 \times \cdots \times A_n)\) where \(A_i\) is the interpretation of \(S_i\), for \(i=1,\ldots,n\). This is the kind of higher order logic or simple theory of types that Ramsey, Church and others introduced.