为什么精益`命题得到特殊对待？

Question

自从我开始学习交互式精益教程以来，一个问题一直困扰着我：Type 中单独的 Prop 层次结构的目的是什么？

据我所知，我们有以下 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 没有意义）但另一方面又像一种类型（例如 show type p : Prop 通过为p 构造一个证明value 来居住）。我怀疑这与区别有关，但我无法表达清楚。有一些基本的论文可以阅读吗？

Answer 1

只有一个由 nat 索引的 Universe Sort u 的层次结构。来自Chapter 3 of Theorem Proving in Lean：

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

在Extended Calculus of Constructions 中引入了在其之上具有不可谓语底层宇宙Prop 和谓词层次结构Type u 的想法。 Lean 将Sort 作为一个单一的通用层次结构引入，这样定义就可以使用Sort u 覆盖所有宇宙，而不需要为Prop 和Type u 单独定义。

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