<div dir="ltr"><div>On Wed, Jan 8, 2014 at 10:48 PM, Joe Hannon <span dir="ltr"><<a href="mailto:hannon@math.bu.edu" target="_blank" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=hannon@math.bu.edu&cc=&bcc=&su=&body=','_blank');return false;">hannon@math.bu.edu</a>></span> wrote:<br>
</div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I can't comment about the type theoretic viewpoint, but in category theory, we call these things "dependent sums". The fact that they are (generalizations of) sums is I think the reason for the sigma notation. And the Pi notation for dependent products, which are generalizations of products.<br>
</div></div></blockquote><div><br></div><div>That's true in type theory too. (However, at least in type theory, Cartesian product is representable both as a dependent sum (by making it non-dependent) and as a dependent product (by picking the indexing set to be bool).)</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>But Jason, I don't understand your remark about weak infty-groupoids versus sets, can you explain further? If f: X -> Y is a map of sets, then we have a dependent sum which is just the disjoint union of the fibers f^{-1}(y), and we have a dependent product which is the set of sections of f, i.e. maps s:Y -> X such that fs = 1. In the event that X is a product FxY and f is projection, then these reduce to the sum (resp. product) of Y copies of F, which is just the product FxY (resp. power F^Y). So these constructions make good sense in Sets. Is there some type-theoretic reason to move to infinity-groupoids?<br>
</div></div></blockquote><div><br></div><div>(One of) the message(s) of HoTT is that, unless you have UIP (uniqueness of identity proofs), types are more naturally interpreted as weak infinity groupoids rather than as sets with weird equality. That was all I was commenting on.</div>
<div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Joe<br></div></div></blockquote><div><br></div><div>-Jason</div><div><br></div><div>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote"><div><div class="h5">
On Wed, Jan 8, 2014 at 9:33 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=jasongross9@gmail.com&cc=&bcc=&su=&body=','_blank');return false;">jasongross9@gmail.com</a>></span> wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr">Hi,<div>At the meeting this past monday, I had said that sigma types were like cartesian products, and David corrected me that they are like disjoint unions, and I had to think for a bit before agreeing. (They are actually colimits, because the indexing types are weak infinity groupoids, not sets.) The reason is that, generally, when you talk about a disjoint union or a colimit, the indexing set is uninteresting. On the other hand, in a sigma type, the indexing type is often the most interesting part. It sounds very strange, perhaps bordering on the nonsensical, to say that you are taking the disjoint union of singleton sets, indexed by functions f : A -> B. On the other hand, it's perfectly natural to do this with a sigma type (and I usually think of inhabitants of a sigma type as pairs, just where the second can depend on the first, while I usually mentally throw away the indexing label of a disjoint union).</div>
<span><font color="#888888">
<div><br></div><div>-Jason</div></font></span></div>
<br></div></div>_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu" target="_blank" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=HoTT-reading-group@mit.edu&cc=&bcc=&su=&body=','_blank');return false;">HoTT-reading-group@mit.edu</a><br>
<a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group" target="_blank">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br>
<br></blockquote></div><br></div>
<br>_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=HoTT-reading-group@mit.edu&cc=&bcc=&su=&body=','_blank');return false;">HoTT-reading-group@mit.edu</a><br>
<a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group" target="_blank">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br>
<br></blockquote></div><br></div></div>