[HoTT-reading-group] Disjoint Unions and Sigma Types

[Jason Gross]

Hi,
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).

-Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140108/04863662/attachment.htm