[HoTT-reading-group] Type of pointed types

[Joe Hannon]

Thanks, Jason and Ian. It's clear now. And the types A and 1 -> A are
equivalent, but not equal?

Joe


On Tue, Jan 21, 2014 at 12:47 PM, Jason Gross <jasongross9 at gmail.com> wrote:

> > It seems like a term in this type is just a term in some A.
>
> Note that the indexing type for sigma types, unlike the indexing type for
> many disjoint unions, matters.  A term of type Sum_{A : Type} A is _a type
> A_, together with an inhabitant (point) of that type.  Similarly, a term of
> type Sum_{A : Type} 1 is  just a type.
>
> -Jason
> On Jan 21, 2014 8:24 AM, "Joe Hannon" <hannon at math.bu.edu> wrote:
>
>> On page 89 definition 2.1.7 gives the type of pointed types as Sum_A:U A.
>> Is this right? It seems like a term in this type is just a term in some A.
>> I would've guessed Sum_A:U 1 -> A or something. Or maybe these are equal?
>> _______________________________________________
>> 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/20140123/e08f5d69/attachment.htm