类型理论中与xor b相对应的类型是什么？

问题描述

Category Theory 8.2的末尾，Bartosz Milewski展示了一些逻辑，类别理论和类型系统之间对应关系的示例。

我在徘徊与逻辑异或运算符相对应的内容。我知道

a xor b == (a ∨ b) ∧ ¬(a ∧ b) == (a ∨ b) ∧ (¬a ∨ ¬b)

所以我只解决了部分问题：a xor b对应于(Either a b,Either ? ?)。但是，缺少的两种类型是什么？

看来xor的写法实际上归结为not的写法。

那么¬a是什么？我的理解是，如果存在类型为a的元素（至少一个），则a是逻辑上正确的。因此，对于not a为真，a应该为假，即Void。因此，在我看来，有两种可能性：

(Either a Void,Either Void b) -- here I renamed "not b" to "b"
(Either Void b,Either a Void) -- here I renamed "not a" to "a"

但是在最后一段中，我有种感觉，就是我把狗弄错了。

（跟进问题here。）

解决方法

求反的标准技巧是使用-> Void，因此：

type Not a = a -> Void

当a本身是可证明的无人居住类型时，我们可以完全构造这种居民类型。如果a有任何居民，我们将无法构造这种类型的居民。听起来像是对我的否定！

内联，这意味着您对xor的定义类似于以下之一：

type Xor a b = (Either a b,(a,b) -> Void) -- (a ∨ b) ∧ ¬(a ∧ b)
type Xor a b = (Either a b,Either (a -> Void) (b -> Void)) -- (a ∨ b) ∧ (¬a ∨ ¬b)