<p>> It seems like a term in this type is just a term in some A.</p>
<p>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.</p>
<p>-Jason</p>
<div class="gmail_quote">On Jan 21, 2014 8:24 AM, "Joe Hannon" <<a href="mailto:hannon@math.bu.edu">hannon@math.bu.edu</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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?<br>
_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu">HoTT-reading-group@mit.edu</a><br>
<a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group" target="_blank">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br>
</blockquote></div>