<div dir="ltr">On Wed, Jan 8, 2014 at 11:03 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br><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 class="im"><div>On Wed, Jan 8, 2014 at 10:48 PM, Joe Hannon <span dir="ltr"><<a href="mailto:hannon@math.bu.edu" target="_blank">hannon@math.bu.edu</a>></span> wrote:<br>
</div></div><div class="gmail_extra"><div class="gmail_quote"><div class="im"><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><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></div></blockquote><div><br><br></div><div>Ok, that's cool. According to nLab, this is the case in any category with a terminal object s.t. you can pullback any morphism along the terminal arrow. That's definitely true in Set. I guess must be true in the category of types as well.<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 class="gmail_extra"><div class="gmail_quote"><div class="im">
<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><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></div></div></blockquote><div><br></div><div>Hm, well that is very intriguing. Hopefully I can understand that point of view better with time. Thank you for clarifying.<br><br>Joe<br></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 class="gmail_extra"><div class="gmail_quote">
<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<span class="HOEnZb"><font color="#888888"><br></font></span></div></div></blockquote>
<span class="HOEnZb"><font color="#888888"><div><br></div><div>-Jason</div></font></span><div class="im"><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>
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>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><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">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" target="_blank">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></div><br></div></div>
</blockquote></div><br></div></div>