coq - Coq 中的类型是互斥的吗？

Question

问题:

Coq 中的类型是互斥的吗？

例如，在该问题的已接受答案中: What exactly is a Set in COQ
提到“Set <= Type_0”。 (这是否意味着任何 Set 类型也是 Type 类型？)

另一方面，在这个问题的公认答案中: Making and comparing Sets in Coq
提到“语言的每个有效元素都只有一种类型”。

我的动机:

Coq 中的关系(在关系中: Coq.Relations.Relation_Definitions )定义为:

Variable A : Type.
Definition relation := A -> A -> Prop.

我的意图是表达对某些“较小”B 的关系的限制。如果类型是相互排斥的，那么它可能没有意义。

Answer 1

从这个意义上来说，是的，类型是排他性的。

您不能对某些较小的 B 表达限制，至少不是像 Set/Prop/Type(0) 这样的类型之间- 一种类型中包含的所有内容也包含在更大的类型中。

Coq 中的子类型与传统语言略有不同。 Set <= Type(0)表示任何类型 Set可以提升为类型 Type(0) ，并不总是有 Type(0) 。 Coq Manual 的 CIC/Sorts 部分解释了排序之间的子类型。 .

但是，如果您使用类型类，则可以定义子类的关系限制!例如，您可以定义一个具有“+”运算符的类型类，并定义一个“+”运算符关联的子类。