@@ -1,12 +1,37 @@
11module Prelude.Pairs
22
3+import Builtins
4+
35%access public
46%default total
57
6−||| Dependent pair where the first field is erased.
7−data Exists : {a : Type} -> (P : a -> Type) -> Type where
8− witness : .{P : a -> Type} -> .{x : a} -> (pf : P x) -> Exists P
8+using (a : Type, P : a -> Type)
9+
10+ ||| Dependent pair where the first field is erased.
11+ data Exists : (P : a -> Type) -> Type where
12+ evidence : .{x : a} -> (pf : P x) -> Exists P
13+
14+ ||| Dependent pair where the second field is erased.
15+ data Subset : (a : Type) -> (P : a -> Type) -> Type where
16+ element : (x : a) -> .(pf : P x) -> Subset a P
17+
18+ ||| The type class of dependent pairs.
19+ class DepPair (a : Type) (P : a -> Type) (T : Type) where
20+
21+ ||| The first projection from a dependent pair.
22+ getWitness : (x : T) -> a
23+
24+ ||| The second projection from a dependent pair.
25+ getProof : (x : T) -> P (getWitness x)
26+
27+ instance DepPair a P (Exists {a} P) where
28+ getWitness (evidence {x=x} pf) = x
29+ getProof (evidence {x=x} pf) = pf
30+
31+ instance DepPair a P (Subset a P) where
32+ getWitness (element x pf) = x
33+ getProof (element x pf) = pf
934
10−||| Dependent pair where the second field is erased.
11−data Subset : (a : Type) -> (P : a -> Type) -> Type where
12− element : .{P : a -> Type} -> (x : a) -> .(pf : P x) -> Subset a P
35+ instance DepPair a P (Pair a P) where
36+ getWitness (pair x pf) = x
37+ getProof (pair x pf) = pf