@@ -7,31 +7,36 @@ import Builtins
77
88using (a : Type, P : a -> Type)
99
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
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
1313
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
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
1717
18− ||| The type class of dependent pairs.
19− class DepPair (a : Type) (P : a -> Type) (T : Type) where
18+ -- Monomorphic projections
2019
21− ||| The first projection from a dependent pair.
22− getWitness : (x : T) -> a
20+ namespace Exists
21+ getWitness : Exists {a} P -> a
22+ getWitness (evidence x pf) = x
2323
24− ||| The second projection from a dependent pair.
25− getProof : (x : T) -> P (getWitness x)
24+ getProof : (x : Exists {a} P) -> P (getWitness x)
25+ getProof (evidence x pf) = pf
2626
27− instance DepPair a P (Exists {a} P) where
28− getWitness (evidence x pf) = x
29− getProof (evidence x pf) = pf
27+ namespace Subset
28+ getWitness : Subset a P -> a
29+ getWitness (element x pf) = x
3030
31− instance DepPair a P (Subset a P) where
32− getWitness (element x pf) = x
33− getProof (element x pf) = pf
31+ getProof : (x : Subset a P) -> P (getWitness x)
32+ getProof (element x pf) = pf
3433
35− instance DepPair a P (Pair a P) where
36− getWitness (pair x pf) = x
37− getProof (pair x pf) = pf
34+ namespace Pair
35+ getWitness : Pair a P -> a
36+ getWitness (pair x pf) = x
37+
38+ getProof : (x : Pair a P) -> P (getWitness x)
39+ getProof (pair x pf) = pf
40+
41+ -- Polymorphic (class-based) projections have been removed
42+ -- because type-directed name disambiguation works better.