类型：输入 Coq

Question

一次偶然，我发现在 Coq 中可以做出如下定义：

Definition x := Type : Type.

这是什么Type : Type意思？这种定义有哪些用例？

Answer 1

这个答案有两个部分。

\n

这是什么Definition x := y : A意思？

\n

这意味着x被定义为y并且有一个y类型为 的断言A。通常，这个断言是多余的，因为 Coq 能够y自行确定 的类型。然而，有时一个术语有太多隐含部分，因此需要断言来确定所有这些隐含部分。

\n

这是什么Type : Type意思？

\n

具有隐式部分的一个示例是Type。您可能会惊讶 Coq 中没有单身人士Type。相反，存在类型Type@{0}, Type@{1}, Type@{2}\xe2\x80\xa6 和Type@{i} : Type@{j}if的无限层次结构i < j。这意味着每个宇宙（Type@{j}）都包含每个具有更小能级的宇宙作为一个元素。

\n

然而，默认情况下，Coq 不会明确显示这些“宇宙级别”。Coq 通常足够聪明，它可以计算出宇宙级别（或使它们通用），而不会打扰您。您可以告诉 Coq 使用白话命令来显示它们Set Printing Universes.，或者通过在 IDE 菜单中设置选项（如果您正在使用它）来显示它们。然后，按照x你的方式定义后，使用命令Print x.将显示

\n

x = \nType@{Top.2}\n     : Type@{Top.1}\n(* {Top.2 Top.1} |= Top.2 < Top.1\n                     *)\n

\n

所以x被定义为Type@{Top.2}并且具有类型Type@{Top.1}。Top.1和Top.2只是通用宇宙级别的名称。消息底部的部分只是简单地说明Top.2必须小于Top.1。这是因为我们需要Type@{Top.2}有类型Type@{Top.1}。请记住，宇宙包含其下方的宇宙，但不包含其上方的宇宙。

\n

附带问题：为什么有多个级别Type？

\n

简而言之，如果我们只有一个Type，Type : Type就有可能表明系统是不一致的。这被称为吉拉德悖论（或更简单的变体，称为赫肯悖论）。请参阅此答案以获取一些不错的细节。

\n

如果您想要 Coq 宇宙的另一种解释，请参阅这个很棒的答案。

\n