MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top


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.


share|cite|improve this question
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

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).

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.