类型对（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)