In this paper, the theory of constructions is reinterpreted as a type theory of "sets" and "predicates". Following some set-theoretical intuitions, it is modified at two points: (1) a simple new operation is added — to represent a constructive version of the comprehension principle; (2) a restriction on contexts is imposed — "sets" must not depend on "proofs" of "predicates". The resulting theory is called theory of predicates. Sufficiently constructive arguments from naive set theory can be directly written down in it. On the other hand, modification (2) is relevant from a computational point of view, since it corresponds to a necessary condition of the modular approach to programming.