0
$\begingroup$

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

Improve this question
$\endgroup$
1
  • 3
    $\begingroup$ 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). $\endgroup$
    – David Roberts ♦
    Commented Dec 12, 2012 at 23:26

1 Answer 1

Reset to default
1
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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). $\endgroup$
    – Toby Bartels
    Commented Jan 11, 2013 at 15:38
  • $\begingroup$ But these are pretty much technicalities. The differences between Set and Type are rarely relevant (Prop is more so). $\endgroup$
    – Toby Bartels
    Commented Jan 11, 2013 at 15:39

You must log in to answer this question.