[HoTT-reading-group] Type of pointed types

[Jason Gross]

> 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/20140121/2a5d0772/attachment.htm