types - 为什么精益“命题”会受到特殊对待？

Question

自从我开始阅读交互式精益教程以来，一个问题一直困扰着我：Prop内部分离层次结构的目的是什么Type？

据我现在了解，我们有以下 Universe 层次结构：

Type (n+1)
  |   \
  |   Sort (n+1)
  |     |
Type n  | (?)
  |   \ |
 ...  Sort n
  |     |
Type 0 ... (?)
  |   \ |
 nat  Prop
  |     |
  0   p ∧ q
        |
     ⟨hp, hq⟩

1. 边缘是否?真的有标记，或者我只是弥补它们（可能）？
2. 快速查看 Agda 和 Idris 似乎他们没有区分Sort n和Type n。为什么精益区分它们？

令人感到奇怪的Prop是，一方面它就像一个归纳类型（例如，它是封闭的事实意味着p ∧ nat没有意义），但另一方面却像一种类型一样使用（例如，通过构造一个证明值来显示类型 ）。我怀疑这与区别有关，但我无法表达清楚。有一些基本的论文可以阅读吗？p : Propp

Answer 1

只有一个按 nat 索引的 Universe 层次结构Sort u。来自精益中定理证明的第 3 章：

事实上，类型Prop是 的语法糖Sort 0，是上一章中描述的类型层次结构的最底层。而且，Type u也只是Sort (u+1).

在扩展的构造演算中引入了在其之上具有不可谓语的底部宇宙Prop和谓语层次结构的想法。精益作为一个单一的通用层次结构引入，因此定义可以覆盖所有宇宙，而不是需要单独的定义 for和 for 。Type uSortSort uPropType u

相比之下，Idris 和 Agda 中的底层宇宙并没有做任何特别的事情，因此他们对整个层次结构使用一个名称。