Re: [Agda] Why does Data.Product have � for the type constructor?

[Marcin Benke]

2008/5/9 Samuel Bronson <naesten at gmail.com>:
> Why does Data.Product have $B-t(B for the type constructor? Wouldn't $B&0(B be
> more appropriate? I guess that might have other connotations,
> though... still, $B-t(B???

Sigma x:A.B(x) is the set of proofs of the *existential* statement
"exists x in A such that B(x)".
As it happens, it is also a set of pairs <x,y> s.t. x in A, y in B(x),
hence a generalisation of cartesian product

Pi x:A.B(x) corresponds to the universal statement "for all x in A
B(x) holds". It is a generalised product, i.e a set of functions.

Hope this helps.

-- 
Marcin Benke