<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 17, 2015 at 4:38 AM, N. Raghavendra <span dir="ltr"><<a href="mailto:raghu@hri.res.in" target="_blank">raghu@hri.res.in</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">At 2015-02-17T11:03:12+01:00, Andrea Vezzosi wrote:<br>
<br>
</span>I guess I should get used to the fact that it's only syntactic sugar.<br>
Whenever I see "forall x -> B x" I keep thinking "\prod_x B(x)". But I<br>
think of "(x : _) -> B x" also as "\prod_x B(x)", so I guess it's ok.<br>
<div class="HOEnZb"><div class="h5"><br></div></div></blockquote><div><br></div><div>The problem here is in terminology, unfortunately. The "dependent product" is the pi type (dependent function type), which has a logical interpretation of "for all". The "dependent sum" is the sigma type (dependent pair type), which as a logical interpretation of "there exists". This conflicts with referring to (dependent) pairs as a (Cartesian) product.<br></div></div><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div><div>Christopher Jenkins<br></div>Embedded Systems Software Engineer<br></div>Genesi USA Inc.<br></div></div>
</div></div>