在范畴论 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) -- …