Type theories tend towards predicativity mainly socio-technical reasons.
First, the informal concept of impredicativity can be formalized in (at least) two different ways. First, we say that a type theory like System F is impredicative because type quantification can range over all types (including the type the quantifier belongs to). So we can define generic identity and composition operators:
$$
\begin{array}{lclll}
\mathit{id} & : & \forall a.\; a \to a & = & \Lambda a.\;\lambda x.\;x\\
\mathit{compose} & : & \forall a, b, c.\; (a \to b) \to (b \to c) \to (a \to c)
& = & \Lambda a,b,c.\lambda f, g. \lambda x. g(f\;x)
\end{array}
$$
However, note that in standard (eg, ZFC) set theory, these operations are not definable as objects. There is no such thing as "the identity function" in set theory, because a function is a relation between a domain set and a codomain set, and if a single function could be the identity function, then you could use it to construct a set of all sets. (This is basically how John Reynolds showed that System-F style polymorphism had no set-theoretic models.)
However, set theory is impredicative in another way, via the powerset axiom. Power sets are impredicative because you can say things like "let $X$ be the intersection of all subsets of $S$ with property $P$" and then proceed to prove that $X$ itself has property $P$. As a result, $X$ has been defined "impredicatively", in terms of a set of which it is a member. This notion of impredicativity is incompatible with F-style quantification; see Andy Pitts's paper Non-trivial Power Types Can't Be Subtypes of Polymorphic Types.
So F-style impredicativity is incompatible with a naive view of types as sets. If you are using type theory as a proof assistant, it's nice to be able to port standard math easily to your tool, and so most people implementing such systems simply remove impredicativity. This way everything has both a set-theoretic and type-theoretic reading, and you can interpret types in whatever fashion is most convenient for you.
forall P : Type, {P} + {~P}
, as this + impredicative set implies proof irrelevance (andnat
is not proof irrelevant). See e.g. coq.inria.fr/library/Coq.Logic.ClassicalUniqueChoice.html and coq.inria.fr/library/Coq.Logic.Berardi.html $\endgroup$