Type for pairs (x, y) with (x / = y)

Question

I would like to set the type for couples (x, y)with x /= y.

My idea is to define NEqPa : Type -> Typewhat NEqPa ashould contain all elements ((x,y), p)with x : a, y : aand p : (x = y) -> Void. I tried the following two versions:

NEqPa a = ((x, y) : (a, a) ** (x = y) -> Void)

NEqPa a = ((x : a, y : a) ** (x = y) -> Void)

Both seem syntactically incorrect, but I have no idea how to fix them.

[EDIT] I found a solution:

NEqPa a = (p : (a, a) ** (fst p = snd p) -> Void)

Is this approach reasonable?

Answer 1

Syntactic sugar **is a bit cumbersome to use when you want to add an explicit type annotation to the first coordinate. I would just use DPairdirectly:

NEqPa : Type -> Type
NEqPa a = DPair (a, a) $ \(x, y) => Not (x = y)