类型：输入 Coq

Question

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

Definition x := Type : Type.

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

Answer 1

这个答案有两个部分。

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

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

Type : Type 是什么意思？

具有隐式部分的示例是Type。 Coq 中没有一个 Type 可能会让您感到惊讶。相反，Type@{0}、Type@{1}、Type@{2}... 和Type@{i} : Type@{j} 类型的无限层次结构i < j。这意味着每个 Universe (Type@{j}) 都包含每个具有较小级别的 Universe 作为元素。

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

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

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

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

简而言之，如果我们只有一个Type 和Type : Type，就有可能表明系统不一致。这称为 Girard 悖论（或称为 Hurkens 悖论的更简单变体）。请参阅this answer 了解一些不错的详细信息。

如果您想对 Coq 的宇宙进行其他解释，请参阅 this great answer。