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?