What type corresponds to a xor b in type theory?

Question

At the end of Category Theory 8.2, Bartosz Milewski shows some examples of the correspondence between logic, category theory, and type systems.

I was wandering what corresponds to the logical xor operator. I know that

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

so I've solved only part of the problem: a xor b corresponds to (Either a b, Either ? ?). But what are the two missing types?

It seems that how to write xor actually boils down to how to write not.

So what is ¬a? My understanding is that a is logical true if there exist an element (at least one) of type a. So for not a to be true, a should be false, i.e. it should be Void. Therefore, it seems to me that there are two possibilities:

(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"

But in this last paragraph I have the feeling I'm just getting the wrong end of the dog.

(Follow up question here.)

Answer 1

The standard trick for negation is to use -> Void, so:

type Not a = a -> Void

We can construct a total inhabitant of this type exactly when a is itself a provably uninhabited type; if there are any inhabitants of a, we cannot construct a total inhabitant of this type. Sounds like a negation to me!

Inlined, this means your definition of xor looks like one of these:

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)