@@ -33,19 +33,15 @@ namespace Builtins
33 ||| @b the right element of the pair
33 ||| @b the right element of the pair
34 MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
34 MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
36− -- Usage hints for erasure analysis
40− ||| Dependent pairs
36+ ||| Dependent pairs aid in the construction of dependent types by
37+ ||| providing evidence that some value resides in the type.
39+ ||| Formally, speaking, dependent pairs represent existential
42− ||| Dependent pairs represent existential quantification - they consist of a
40+ ||| quantification - they consist of a witness for the existential
43− ||| witness for the existential claim and a proof that the property holds for
41+ ||| claim and a proof that the property holds for it.
44− ||| it. Another way to see dependent pairs is as just data - for instance, the
45− ||| length of a vector paired with that vector.
47− ||| @ a the type of the witness
43+ ||| @ a the value to place in the type.
48− ||| @ P the type of the proof
44+ ||| @ P the dependent type that requires the value.
49 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
45 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
50 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
46 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P