  However it is not just the universal set that appears at each type. We also get the naturals, the reals and the rationals etc. etc. at each type, and this is clearly not what we want. (Holmes refers to this as the Hall of Mirrors effect.) Quine’s move in [1937a] is the natural one of taking the pseudoformulæ like (A) and thinking of them as genuine formulæ in a new, one-sorted, language. The new theory does not have a universal set at each type, for it has no types: it has a single universal set. And a single implementation of the reals, and so on. Formulæ of the one-sorted language obtained in this way from formulæ of type theory are said to be stratified. The axioms of NF are now extensionality plus those instances of naïve comprehension that happen to be stratified.