most recent 30 from http://mathoverflow.net 2013-06-20T05:45:47Z http://mathoverflow.net/feeds/question/116191 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/116191/prod-and-sig-in-coq Asymptotik 2012-12-12T18:25:28Z 2013-01-11T15:22:00Z

<p>Hello,</p> <p>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.</p> <p>Best</p>

http://mathoverflow.net/questions/116191/prod-and-sig-in-coq/117412#117412 Asymptotik 2012-12-28T15:06:43Z 2012-12-28T15:06:43Z

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