"Impredicative" in type theory I am confused. I think I've read two usages of the word "impredicative" in type theory:


When people talk about the "impredicative" version of Martin-Löf's type theory, which they say it is inconsistent. Apparently they call it impredicative because of Type : Type.
When people talk about the "impredicative" Prop in CoC. Apparently they call it impredicative because you can quantify over Prop and get Prop stuff.


Is it the case? One notion of impredicativity implies the other? Is there no problem (i.e. inconsistency) by assuming "Prop impredicative"?
The definition of an object $X$ is impredicative, if the definition uses a collection $C$ in the construction of $X$, such that $X$ is a member of $C$.  So impredicativity is a form of circularity.

We are wary of circular definitions because they are often paradoxical. Fortunately it turns out that not all forms of
circularity are (or appear to be) problematic.  The most famous example of an impredicative definition that is circular, but (as far as we know) not contradictory is the definition of natural numbers in set theory:

$$
\mathbb{N}\ \stackrel{\text{def}}{=}\ \bigcap \{X\ |\ X\ \text{is an inductive set}\}
$$

where a set is inductive if it contains $\emptyset$ and
  is closed under the set-theoretic successor operation.  Clearly, $\mathbb{N}$ is itself inductive, hence what you define on the left already occurs in some sense on the right.

By the "impredicative version of Martin-Löf's type theory" I guess you mean the type theory in his 1971 manuscript "An intuitionistic theory of types". This system has an  impredicative axiom  that stipulates a type of all types.  For this reason the system is often simply called "type:type". This axiom is too strong as J.-Y. Girard showed, as it makes the type-theory inconsistent. 

In contrast, the impredicativity in the CoC is not (known to be) inconsistent.

In some sense there are two forms of impredicativity: those that are known to be paradoxical, and those that are not.