types - 为什么 Leans `Prop` 位置得到特殊处理？

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 没有意义)但是另一方面，像一种类型一样使用(例如，显示 type p : Prop 通过为 p)。我怀疑这与区别有关，但我无法表达清楚。有没有一些基础论文可以阅读这篇文章？

Answer 1

nat-i​​ndexed universe 只有一个层次结构 Sort u。来自 Chapter 3 of Theorem Proving in Lean :

In fact, the type Prop is syntactic sugar for Sort 0, the very bottom of the type hierarchy described in the last chapter. Moreover, Type u is also just syntactic sugar for Sort (u+1).

在 Extended Calculus of Constructions 中介绍了拥有一个命令式底部宇宙 Prop 和一个命令式层次结构 Type u 的想法。 .精益将 Sort 作为一个单一的广义层次结构引入，这样定义就可以覆盖所有使用 Sort u 的宇宙，而不需要为 Prop 和 键入 u。

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