In the following code, the statement add'_commut is accepted by Coq but add_commut is rejected because of a universe inconsistency.
Set Universe Polymorphism.
Definition nat : Type := forall (X : Type), X -> (X -> X) -> X.
Definition succ (n : nat) : nat := fun X z s => s (n X z s).
Definition add' (m n : nat) : nat := fun X z s => m X (n X z s) s.
Definition nat_rec (z : nat) (s : nat -> nat) (n : nat) : nat := n nat z s.
Definition add (m n : nat) : nat := nat_rec n succ m.
Definition equal (A : Type) (a : A) : A -> Type := fun a' => forall (P : A -> Type), P a -> P a'.
Lemma add'_commut (m n : nat) : equal nat (add' m n) (add' n m).
Admitted.
Lemma add_commut (m n : nat) : equal nat (add m n) (add n m).
(*
In environment
m : nat
n : nat
The term "add n (fun X : Type => m X)" has type
"nat@{Top.1078 Top.1079}"
while it is expected to have type
"nat@{Top.1080 Top.1078}" (universe inconsistency).
*)
How to make it go through?
Church numerals only work if you turn on impredicative Set, by putting -arg -impredicative-set into your _CoqProject file or using -impredicative-set command line option. Then define nat as:
Definition nat : Set := forall (X : Set), X -> (X -> X) -> X.
Impredicative Set allows nat to have exactly the same type Set which it quantifies over. Without impredicativity, nat must have a higher universe level than what it quantifies over, although the levels are hidden from you until you get an error like in the question.
Note that impredicative Set is incompatible with classical logic.