類型對（x，y）與（x/= y）

Question

我想要設置類型(x, y)與x /= y。

我的想法是定義NEqPa : Type -> Type這樣NEqPa a應該包含所有的元素((x,y), p)與x : a，y : a和p : (x = y) -> Void。我嘗試了以下兩個版本：

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

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

這兩個似乎都是語法錯誤，但我不知道如何解決它們。

[編輯]我發現了一個解決方案：

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

是這種做法合理嗎？

Answer 1

**的語法糖在第一個座標上添加明確的類型註釋時有點難以使用。我只是直接使用DPair：

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