[HoTT-reading-group] Type of pointed types

[J. Ian Johnson]

They're propositionally equal by univalence, so you still have to transport across the equality to replace instances of 1 -> A with A. That way you don't have a well-typed term that tries to apply an arbitrary type A to * (the inhabitant of 1).
-Ian
----- Original Message -----
From: "Joe Hannon" <hannon at math.bu.edu>
To: "Jason Gross" <jasongross9 at gmail.com>
Cc: hott-reading-group at mit.edu
Sent: Thursday, January 23, 2014 3:08:14 AM GMT -05:00 US/Canada Eastern
Subject: Re: [HoTT-reading-group] Type of pointed types




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 


_______________________________________________
HoTT-reading-group mailing list
HoTT-reading-group at mit.edu
http://mailman.mit.edu/mailman/listinfo/hott-reading-group