为什么Leans'提议得到特殊待遇？

Question

自从我开始学习交互式精益教程以来，一个问题让我感到不快：在Type内，单独的Prop层次结构的目的是什么？

正如我现在明白了吧，我们已经制定了以下宇宙层次：

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

1. 是边缘打上?居然有或没有我只是做起来（可能）？
2. 从迅速直视阿格达和伊德里斯似乎他们不这样做Sort n和Type n之间的区别。为什么精益区分它们？

什么感觉怪怪的约Prop是，它就像一方面是感应型（例如，实际上它是封闭的手段p ∧ nat没有意义），但就像是一种从另一方面使用（如显示类型p : Prop到通过构建一个证明值为p）被inhabitated。我怀疑这与区别有关，但我无法表达它。有没有一些基本的论文可以阅读这些内容？

Answer 1

有NAT索引宇宙Sort u的只是一个单一的层次结构。从Chapter 3 of Theorem Proving in Lean：

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

具有impredicative底部宇宙Prop和在它的上面表语层次Type u的想法在Extended Calculus of Constructions引入。精益将Sort引入为一个单一的广义层次结构，因此定义可以使用Sort u覆盖所有Universe，而不需要单独定义Prop和Type u。

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