Coq：Type(n) 中的 Prop 与 Set

我想考虑以下三个（相关的？）Coq 定义。

Inductive nat1: Prop :=
  | z1 : nat1
  | s1 : nat1 -> nat1.

Inductive nat2 : Set := 
  | z2 : nat2
  | s2 : nat2 -> nat2.

Inductive nat3 : Type :=
  | z3 : nat3
  | s3 : nat3 -> nat3.

所有这三种类型都给出了归纳原理来证明命题成立。

nat1_ind
     : forall P : Prop, P -> (nat1 -> P -> P) -> nat1 -> P

nat2_ind
     : forall P : nat2 -> Prop,
       P z2 -> (forall n : nat2, P n -> P (s2 n)) -> forall n : nat2, P n

nat3_ind
     : forall P : nat3 -> Prop,
       P z3 -> (forall n : nat3, P n -> P (s3 n)) -> forall n : nat3, P n

集合和类型版本还包含集合和类型（分别为 rec 和 rect）定义的归纳原理。这就是我对 Prop 和 Set 之间差异的了解程度； Prop 的感应力较弱。

我还读到 Prop 是谓语，而 Set 是谓语，但这似乎是一个属性，而不是一个定义的质量。

虽然 Set 和 Prop 之间的一些实际（道德？）差异是显而易见的，但 Set 和 Prop 之间的确切定义差异以及它们在类型宇宙中的位置尚不清楚（对 Prop 和 Set 运行检查给出 Type (* ( Set) + 1*))，我不太确定如何解释这个......

Type : Type不一致。

谓语Set排除中间意味着证明无关，所以是必然的Set具有证明相关性，例如true <> false，反驳排除中数，这是直觉主义不应该做的。

因此我们把不可预测性留在Prop类型层次结构的其余部分为我们提供了可预测性。

顺便一提，

forall P : nat1 -> Prop, P z1 -> (forall n : nat1, P n -> P (s1 n)) -> forall n : nat1, P n

是可证明的。不要问我 Coq 只自动证明其他较弱的归纳原理有什么好处......

另外，你读过吗CPDT 的这一章 http://adam.chlipala.net/cpdt/html/Universes.html?