Predicativity in Coq


Paris
Très niche

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

† [Paolo G. Giarrusso](http://blaisorblade.github.io): the initial push

‡ [Gaëtan Gilbert](https://github.com/SkySkimmer): intricacies of universes in Coq

§ [Hugo Herbelin](http://pauillac.inria.fr/~herbelin/): syntactic mastery over Coq