<div dir="ltr"><div class="gmail_extra">On Wed, Feb 25, 2015 at 3:26 AM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>&gt;</span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I guess programmers are more interested in whether something is a pair or a function than in Descartes or families of sets.<br></blockquote><div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">​If they are, then shouldn&#39;t they recognize that the sum type A + B is inhabited by pairs? The values are pairs of a tag and ​a value of the corresponding type. And sigma types internalize what you get to put in the tag portion of the pair.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">Anyhow, I&#39;m pretty sure I&#39;m a programmer, but I&#39;ve always used and liked the sum-product terminology. I actually thought it was the more common amongst people doing work on dependent type theory (although if you want to eliminate any chance of misinterpretation, &quot;sigma type&quot; and &quot;pi type&quot; seem safest, and serviceable).  Maybe I&#39;m a weird programmer, though.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">-- Dan<br></div></div></div><br></div></div>