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

[Joe Hannon]

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.

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?

Joe


On Wed, Jan 8, 2014 at 9:33 PM, Jason Gross <jasongross9 at gmail.com> wrote:

> 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
>
> _______________________________________________
> HoTT-reading-group mailing list
> HoTT-reading-group at mit.edu
> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140108/c16ef50c/attachment.htm