无交并 (类型论)

无交并类型 (又叫余积类型) 是集合的无交并类型论中的类比, 它在简单类型论依值类型论里都可以定义. 在类型论中, 无交并的对偶是积类型.

1类型规则

类型 的无交并记作 .

以下规则基本上是模仿余积万有性质.

构造规则

可以直接将 视为由如上两构造子生成的归纳类型, 也可以单独给出消去规则.

消去规则

简单类型的消去规则:

简单类型的计算规则:

2范畴语义

在简单类型论的范畴语义中, 无交并类型对应 (弱化的) 余积对象. 而在依值类型论的范畴语义中, 无交并类型对应 (弱化的) 俯范畴里的余积, 注意这不是推出.

术语翻译

无交并类型英文 disjoint union type法文 type d’union disjointe拉丁文 typus summae disiunctae

余积类型英文 coproduct type法文 type coproduit拉丁文 typus coproductus