<div dir="ltr">I agree it's probably a good thing to know about this example, even if it makes me feel like I don't understand HoTT. At least this way I know that my intuition is wrong.<div><br></div><div style>However, it seems to me to be of utmost importance (relative to this reading group) to understand either:</div>
<div style><ol style><li style>In what sense there could possibly be a continuous inverse to the inclusion of the naturals in the non-negative reals; or</li><li style>In what sense my description in 1. above fails to match the mathematics underlying the <a href="http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-ℕ-‖ℕ‖-is-nearly-invertible/">mystery map offered by Nicolai Kraus</a>.</li>
</ol><div style>David</div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 18, 2014 at 10:44 AM, Gregory Malecha <span dir="ltr"><<a href="mailto:gmalecha@cs.harvard.edu" target="_blank">gmalecha@cs.harvard.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Despite getting a little bit derailed at the end of yesterday, I found the discussion to be very useful.<i> </i>In particular, being a type theorist I don't get the mathematical point of view just from reading the book. I'm happy to offer the 'type theorist perspective' whenever it is useful but I feel that those intuitions are shallower (because they are less interested in the model and more interested in doing things above the model) than the mathematical ones.<div>
<br></div><div>I'm enjoying it, and thanks for the example, Jason. There is still something that feels strange about it, but I will continue to wrapping my head around it.</div></div><div class="gmail_extra"><br><br>
<div class="gmail_quote"><div><div class="h5">
On Mon, Feb 17, 2014 at 11:42 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div><div class="h5">
<div dir="ltr"><div>Next week, I plan for us to do what was actually on the schedule for this week, namely covering questions on chapters 3 and 4 and reviewing exercises 3.13, 3.14, and 4.5; please come in with the exercises completed or with questions about how to do them.</div>
<div><br></div><div>I also welcome advice and feedback on the reading group (now or in the future, in person, or by private email), whether that's "I want to get <i>foo</i> out of the group, and I'm not getting it" or "keep doing what you're doing" or "more/fewer exercises" or something else.</div>
<div><br></div><div>Finally, today in the HoTT reading group, we talked about how chapter 4 seems dry to those with no prior knowledge of how the various definitions of equivalence are used in math, but interesting to those who can connect them up to various other bits of math; we talked about various notions of contractibility (inhabited hprop; equivalent to unit; filling of spheres/holes); a bit about truncation; and I brought up the fact that <a href="http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible/" target="_blank">The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible</a>, which was perhaps a mistake, given that I botched the presentation. I will leave it up to those interested to read the <a href="http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible/" target="_blank">blog post</a>, <a href="http://red.cs.nott.ac.uk/~ngk/html-trunc-inverse/trunc-inverse.html" target="_blank">Nicolai's Agda code</a>, or <a href="https://gist.github.com/JasonGross/9064514" target="_blank">my own Coq version of it</a>. I think the essence of it is that you can extract information even from contractible types, which I show in <a href="https://gist.github.com/JasonGross/9064636" target="_blank">a much shorter Coq example</a> involving Bool, and two values [x] and [y] where we have [x = y] but we have a (dependent) function [f] with [f x ≠ f y]. (I believe this is related to the difference between having a path between two points in a fiber, and a path between those points which lies over the constant path, and how you can have the former without the latter.)</div>
<span><font color="#888888">
<div><br></div><div>-Jason</div></font></span></div>
<br></div></div>_______________________________________________<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>
<br></blockquote></div><span class="HOEnZb"><font color="#888888"><br><br clear="all"><div><br></div>-- <br><div dir="ltr">gregory malecha<br><div><a href="http://www.people.fas.harvard.edu/~gmalecha/" target="_blank">http://www.people.fas.harvard.edu/~gmalecha/</a></div>
</div>
</font></span></div>
<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>
<br></blockquote></div><br></div>