title: Relation between types prod and sig in COQ
body: <p>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, for instance some definitional equality but I don't find it explicitely in the reference manual.</p>