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

[Joe Hannon]

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

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


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.


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

Hm, well that is very intriguing. Hopefully I can understand that point of
view better with time. Thank you for clarifying.

Joe



>
> 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/20140109/135fd2f8/attachment-0001.htm