为什么高阶类型是转义的，而程序的类型不是？

Question

这可能看起来是一个愚蠢的问题，但我想知道为什么规范类型（如 nat) "继承 "了 Set 类型 Type 类型），而类型的程序却没有？这个包容性是用来做什么的？

示例程序。

> Check (1 : nat).
1 : nat
> Check (nat : Set).
nat : Set
> Check (Set : Type).
Set : Type
> Check (nat : Type).
nat : Type
> Check (1 : Set).
Error: The term "1" has type "nat" while it is expected to have type "Set".

Answer 1

1 没有类型 Set 因为它不是一个类型.没有继承或者类似的东西，你没有 A : Set 意味着 A : Type因为 Set : Type 但由于 Set 是一个 亚型 的 Type.

这就是所谓的 累积性 在Coq的情况下，它只适用于宇宙.宇宙如 Type, Prop 或 Set 是类型的类型。