@@ -1,11 +1,11 @@
11data Sigma : (a : Set) -> (P : a -> Set) -> Set where
22 Exists : {P : a -> Set} -> (x : a) -> P x -> Sigma a P;
33
4−getSigIdx : {P : a -> Set} -> Sigma a P -> a;
5−getSigIdx (Exists a v) = a;
4+getWitness : {P : a -> Set} -> Sigma a P -> a;
5+getWitness (Exists a v) = a;
66
7−getSigVal : {P : a -> Set} -> (s : Sigma a P) -> P (getSigIdx s);
8−getSigVal (Exists a v) = v;
7+getProof : {P : a -> Set} -> (s : Sigma a P) -> P (getWitness s);
8+getProof (Exists a v) = v;
99
1010FalseElim : _|_ -> a;
1111