@@ -7,31 +7,36 @@ import Builtins
8using (a : Type, P : a -> Type)
8using (a : Type, P : a -> Type)
10− ||| Dependent pair where the first field is erased.
10+ ||| Dependent pair where the first field is erased.
11− data Exists : (P : a -> Type) -> Type where
11+ data Exists : (P : a -> Type) -> Type where
12− evidence : .(x : a) -> (pf : P x) -> Exists P
12+ evidence : .(x : a) -> (pf : P x) -> Exists P
14− ||| Dependent pair where the second field is erased.
14+ ||| Dependent pair where the second field is erased.
15− data Subset : (a : Type) -> (P : a -> Type) -> Type where
15+ data Subset : (a : Type) -> (P : a -> Type) -> Type where
16− element : (x : a) -> .(pf : P x) -> Subset a P
16+ element : (x : a) -> .(pf : P x) -> Subset a P
18− ||| The type class of dependent pairs.
18+ -- Monomorphic projections
19− class DepPair (a : Type) (P : a -> Type) (T : Type) where
21− ||| The first projection from a dependent pair.
20+ namespace Exists
21+ getWitness : Exists {a} P -> a
22− getWitness : (x : T) -> a
22+ getWitness (evidence x pf) = x
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
27− instance DepPair a P (Exists {a} P) where
27+ namespace Subset
28+ getWitness : Subset a P -> a
28− getWitness (evidence x pf) = x
29+ getWitness (element x pf) = x
29− getProof (evidence x pf) = pf
31− instance DepPair a P (Subset a P) where
32− getWitness (element x pf) = x
31+ getProof : (x : Subset a P) -> P (getWitness x)
33− getProof (element x pf) = pf
32+ getProof (element x pf) = pf
35− instance DepPair a P (Pair a P) where
34+ namespace Pair
35+ getWitness : Pair a P -> a
36− getWitness (pair x pf) = x
36+ getWitness (pair x pf) = x
38+ getProof : (x : Pair a P) -> P (getWitness x)
37− getProof (pair x pf) = pf
39+ getProof (pair x pf) = pf
41+ -- Polymorphic (class-based) projections have been removed
42+ -- because type-directed name disambiguation works better.