（x/y）のペア（x​​/y）のタイプ

Question

(x, y)のタイプをx /= yに設定したいと考えています。

私の考えはNEqPa : Type -> Typeは、このようなNEqPa aはx : a、y : aとp : (x = y) -> Voidを持つすべての要素を((x,y), p)含めるべきであると定義することです。私は次の2つのバージョンを試しました：

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

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

どちらも文法的に間違っているようですが、私はそれらを修正する方法がありません。

[EDIT]私は解決策を見つけた：

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)