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

[Jason Gross]

On Wed, Jan 8, 2014 at 10:48 PM, Joe Hannon <hannon at math.bu.edu> wrote:

> 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.
>

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


> 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?
>

(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.

Joe
>

-Jason



>
>
> 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
>>
>>
>
> _______________________________________________
> 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/01689e71/attachment.htm