The type hierarchy corresponds neatly to the hierarchy of domains that we saw in our discussion of Cantor's theorem.  A unary predicate has the type &lt;i&gt;; its domain is D—the set of individuals. A unary predicate of predicates has the type &lt;&lt;i&gt;&gt;, and this corresponds to the domain of subsets of D. And so on.