coq - 输入 : Type in Coq

Question

偶然地，我发现可以在 Coq 中做出以下定义:

Definition x := Type : Type.

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

Answer 1

这个答案有两个部分。
什么Definition x := y : A意思？
这意味着 x定义为 y并且有一个断言y类型为 A .通常，这个断言是多余的，因为 Coq 能够确定 y 的类型。就靠它自己。然而，有时一个术语有太多的隐含部分，所以需要断言来确定所有这些隐含部分。
什么Type : Type意思？
具有隐式部分的示例是 Type .您可能会惊讶于没有一个 Type在科克。取而代之的是无限的类型层次结构 Type@{0} , Type@{1} , Type@{2} ... 与 Type@{i} : Type@{j}如果 i < j .这意味着每个宇宙( Type@{j} )都包含每个具有较小级别的宇宙作为元素。
但是，默认情况下，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} .请记住，宇宙包含它们下方的宇宙，但不包含它们上方的宇宙。
附带问题:为什么 Type会有多个级别?
简而言之，如果我们只有一个 Type与 Type : Type ，就可以证明系统是不一致的。这称为吉拉德悖论(或称为赫肯斯悖论的更简单变体)。见 this answer一些不错的细节。
如果您想对 Coq 的 Universe 进行另一种解释，请参阅 this great answer .