В следующем коде оператор add'_commut принимается Coq, но add_commut отклоняется из-за несогласованности юниверса.
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).
*)
Как заставить это пройти?
