Typ für Paare (x, y) mit (x/= y)

Question

Ich möchte einen Typ für Paare (x, y) mit x /= y einrichten.

Meine Idee ist NEqPa : Type -> Type so zu definieren, dass NEqPa a sollten alle Elemente enthalten ((x,y), p) mit x : a, y : a und p : (x = y) -> Void. Ich habe die folgenden zwei Versionen ausprobiert:

Beide scheinen syntaktisch falsch zu sein, aber ich habe keine Ahnung, wie man sie beheben kann.

[EDIT] ich eine Lösung gefunden:

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

Ist dieser Ansatz sinnvoll?

Answer 1

Die Syntax Sugar ** ist ein wenig unhandlich zu verwenden, wenn Sie explizite Typ Annotation auf der ersten Koordinate hinzufügen möchten. Ich würde einfach DPair direkt verwenden:

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