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 impredicative 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}.