Comment by GregarianChild

The "intersection of all sets such that" is not vague at all. It's perfectly formally defined in ZF* set theories. But it's impredicative. One of the guiding ideas behind type theories is to minimise impredicative constructions as much as possible. After all, impredicative definitions are circular ... Of course there is no free lunch and the power of impredicative constructions needs to be supplied in other ways in type theories ...