我正在研究软件基础，目前正在做关于教堂数字的练习。这是自然数的类型签名：
Definition nat := forall X : Type, (X -> X) -> X -> X.
我定义了一个succ类型的函数nat -> nat。我现在想定义一个加法函数，如下所示：
Definition plus (n m : nat) : nat := n nat succ m.
但是，我收到以下错误消息：
Error: Universe inconsistency.
此错误消息实际上是什么意思？
在 Coq 中，一切都有类型。Type也不例外：如果你用Check命令询问 Coq，它会告诉你它的类型是…… Type！
其实，这有点骗人。如果你通过发出指令来询问更多细节Set Printing Universes.，Coq 会告诉你这Type与第一个不同，而是一个“更大”的。形式上，每个Type都有一个与之关联的索引，称为它的宇宙级别。通常在打印表达式时，该索引是不可见的。因此，该问题的正确答案是任何 indexType_i都有 type 。这是确保 Coq 理论的一致性所必需的：如果只有一个，则可能会出现矛盾，类似于如果假设存在所有集合的集合，在集合论中如何得到矛盾。Type_jj > iType
为了使使用类型索引更容易，Coq 为您提供了一些灵活性：实际上没有任何类型具有与之关联的固定索引。相反，Coq 每次编写时都会生成一个新的索引变量Type，并跟踪内部约束以确保它们可以用满足理论要求的具体值来实例化。
您看到的错误消息意味着 Coq 的 Universe 级别的约束求解器说您要求的约束系统无法解决。问题是forall的定义中的nat被量化了Type_i，但是 Coq 的逻辑强制nat它本身是 类型的Type_j，带有j > i。另一方面，应用程序n nat需要j <= i，导致一组不可满足的索引约束。