[HoTT-reading-group] Type of pointed types

[J. Ian Johnson]

Those are equivalent. 1 -> A is the morphism way of writing a constant. A pointed type is simply a type that has something in it, i.e., proof that it's inhabited.
-Ian
----- Original Message -----
From: "Joe Hannon" <hannon at math.bu.edu>
To: hott-reading-group at mit.edu
Sent: Tuesday, January 21, 2014 11:09:43 AM GMT -05:00 US/Canada Eastern
Subject: [HoTT-reading-group] Type of pointed types

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