Coq的类型系统CiC和lambda立方体之间是什么关系？

Question

我读了https://en.wikipedia.org/wiki/Lambda_cube#Formal_definition，并对CiC和lambda cube之间的关系感到困惑。据我了解，CiC扩展了作为Lambda多维数据集的一角的CoC，因此在Coq中也应满足lambda多维数据集的规则。

例如，似乎coq接受（＊，＊）。因为nat -> nat的类型是Set，这是nat的类型（右侧的一个）。

但是Coq似乎不接受（□，＊）。如果是这样，则Set -> nat的类型必须是Set，而不是Type。但是Coq对Check (Set -> nat)的答案是Type。

我是否误解了Wiki页面上的描述？

Answer 1

Coq没有一个不可键入的□，但是是一个可键入变量的层次结构。 （尤其是□：□是其中一种输入规则的粗略近似。）因此，由于这些“宇宙”，Coq不太适合lambda多维数据集的设置。

关于Set -> nat的类型为Set，取决于Set是否为强制性。默认情况下，它是谓词，因此Set -> nat必须具有严格大于Set本身的类型，即Type。但是您可以将Set更改为强制性的：

$ coqtop -impredicative-set
Welcome to Coq 8.11.1 (April 2020)

Coq < Check (Set -> nat).
Set -> nat
     : Set