Coq中Prop是否为Set的真子类型？背后机制是什么？

你发现的这个现象，本质是Coq内置的宇宙层级包含规则，而非常规的子类型机制。

先明确你的实验结果 #

正向转换能正常通过：

Check ((True : Prop) : Set).

(* 输出结果：
(True : Prop) : Set
     : Set
*)

反向转换直接报错：

Check ((True : Set) : Prop).

(* 错误信息：
Error:
The term "True : Set" has type "Set" while it is expected to have type 
"Prop" (universe inconsistency: Cannot enforce Set <= Prop).
*)

核心原因：Prop是Set的子宇宙 #

Coq的类型论设计里，Prop是Set的子宇宙（可以近似理解成Prop <: Set，但这是宇宙层面的包含，不是普通类型的子类型）。具体规则是：

• 所有类型为Prop的项，都能被“提升”成Set类型——因为Prop里的所有内容都属于Set的范畴
• 但反过来绝对不行：Set里的项没法“降级”到Prop。原因很简单：Set包含了大量非命题的类型（比如自然数nat、列表list这些带计算内容的类型），而Prop只用来容纳命题，还自带证明无关性这类特殊特性，Set的项根本满足不了Prop的约束。

和常规子类型的区别 #

这和OOP里的子类型不是一回事：

• 常规子类型讲的是类型间的替换兼容性，而这是Coq基础类型论里的宇宙层级设计
• Prop有Set没有的特性（比如证明无关性：同一个命题的所有证明在Prop里被视为完全等价），Set也有Prop没有的能力（比如可以定义能参与计算的具体类型，Prop里的项一般只作为证明，不参与计算）

总结 #

你看到的就是Coq构造演算的基础规则：Prop是Set的子宇宙，所以Prop的项可以被归类为Set类型，但反向操作违反了宇宙层级的约束，自然会报错。这个规则是内置的，很多入门资料可能不会特意拿出来讲，所以容易被忽略。

内容的提问来源于stack exchange，提问作者radrow