<div dir="ltr"><div>Thanks, Jason and Ian. It's clear now. And the types A and 1 -> A are equivalent, but not equal?<br><br></div>Joe<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jan 21, 2014 at 12:47 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><p>> It seems like a term in this type is just a term in some A.</p>
</div><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>
<span class="HOEnZb"><font color="#888888">
<p>-Jason</p>
</font></span><div class="gmail_quote"><div class="im">On Jan 21, 2014 8:24 AM, "Joe Hannon" <<a href="mailto:hannon@math.bu.edu" target="_blank">hannon@math.bu.edu</a>> wrote:<br type="attribution"></div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
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>
</div><div class="im">
_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu" target="_blank">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>
</div></blockquote></div>
</blockquote></div><br></div>