我想为(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)
这种方法合理吗？
最佳答案
当您想在第一个坐标上添加显式类型注释时，使用**的语法糖有点笨拙。我只是直接使用DPair：
NEqPa : Type -> Type
NEqPa a = DPair (a, a) $ \(x, y) => Not (x = y)