<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>
<br></div><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>
<br></div><div>Joe<br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jan 8, 2014 at 9:33 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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 class="HOEnZb"><font color="#888888">
<div><br></div><div>-Jason</div></font></span></div>
<br>_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu">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>