 We present a typed theory of sets with predicativity restrictions (we have seen this in work of Marcel Crabbé, but it may be older). In this system, the types do not have orders, but Russell’s ramified type theory with orders (complete with relation types) can be interpreted in it (a technical result of which we do not give an account here).