Prop と Type

宇宙を $\mathsf{Prop}:\mathsf{Type}_0:\mathsf{Type}_1:\cdots$ と並べる（Lean では $\mathsf{Sort}\ 0=\mathsf{Prop}$、$\mathsf{Sort}\ (u+1)=\mathsf{Type}\ u$）。Π 型の形成規則は、$B(x):\mathsf{Prop}$ ならば、$A$ がどの宇宙にあっても $\Pi_{(x:A)}B(x):\mathsf{Prop}$ とする（非可述性）。さらに Lean では、$P:\mathsf{Prop}$ の任意の二つの証明 $h_1,h_2:P$ は定義的に等しい（証明の無関係性）。