Today, we write a quick specialized note on what impredicativity exactly means, for those reasonably familiar with the Coq syntax.

Historically speaking, Coq started out with making `Set` predicative and they still carry around the flag `--set-impredicative` to maintain impredicativity in Sets. Let's check it quickly:

```
(* Set is predicative. *)
Fail Definition SetPred := (forall X : Set, X) : Set.
```

We use a little macro to check the impredicativity of various types, since an equivalent definition wouldn't type-check:

```
(* Checks that all inhabitants of U are of type V. *)
Notation "'check' U V" := ((forall X : U, X) : V) (at level 0, U, V at level 0).
```

All inhabitants of `Prop` are of type Prop, for good reason.

```
(* Prop is impredicative. *)
Definition PropImpr := check Prop Prop.
```

Attempt to check the predicativity of `Type` naïvely:

```
(* Is Type impredicative? This is misleading. *)
Definition TypeNaive := (forall X : Type, X) : Type.
```

The previous example was misleading, and we clarify it in the next example:

```
(* In the previous definition, Type is really Type@{i},
* and the following definition fails with: Universe {Predicativity.153} is unbound. *)
Fail Definition TypePred@{i} := check Type@{i} Type@{i}.
```

The Type universe is cumulative, not impredicative. We show the cumulativity using algebraic universe notation:

```
(* Fails due to a bug in Coq: Unable to handle arbitrary u+k <= v constraints? *)
Definition TypePred'@{i} := ((forall X : Type@{i}, X) : Type@{i+1}).
Definition TypePred'@{i} := check Type@{i} Type@{i+1}.
```