Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
3  
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
add comment

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

share|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
add comment

Your Answer

 
discard

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.