prod and sig in COQ

Hello,

Apparently in COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is described the fact that the cartesian product is a particular case of dependent sum ? I wonder there is a link between prod and sig but I don't find it explicitely.

Best

-
Note that if you don't get any help here (wait a few days), you may want to ask on the Coq mailing list, which you can sign up to without trouble (and post a message here saying you've done so). –  David Roberts Dec 12 '12 at 23:26

1 Answer

Actually, the type prod is more akin to sigT than sig. You can use sigT to define a prod' and show there is a bijection between the two types prod and prod' (but they cannot be definitionally equal).

-
More precisely, prodT and sigT (which act on Types) correspond. I don't know anything sig-like that corresponds directly to prod (which acts on Sets). One could also define something prod-like that corresponds directly to sig (which acts on a Set and a (dependent) Prop). –  Toby Bartels Jan 11 '13 at 15:38
But these are pretty much technicalities. The differences between Set and Type are rarely relevant (Prop is more so). –  Toby Bartels Jan 11 '13 at 15:39