Search code examples
syntaxdependent-typeidris

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

I'd like to set up a type for pairs (x, y) with x /= y.

My idea is to define NEqPa : Type -> Type such that NEqPa a should contain all the elements ((x,y), p) with x : a, y : a and 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 to be 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?

Solution

  • The syntax sugar of ** is a bit unwieldy to use when you want to add explicit type annotation on the first coordinate. I'd just use DPair directly:

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