[HoTT-reading-group] Today; Next Monday

[David Spivak]

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.

However, it seems to me to be of utmost importance (relative to this
reading group) to understand either:

   1. In what sense there could possibly be a continuous inverse to the
   inclusion of the naturals in the non-negative reals; or
   2. In what sense my description in 1. above fails to match the
   mathematics underlying the mystery map offered by Nicolai
Kraus<http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-ℕ-‖ℕ‖-is-nearly-invertible/>
   .

David


On Tue, Feb 18, 2014 at 10:44 AM, Gregory Malecha
<gmalecha at cs.harvard.edu>wrote:

> Despite getting a little bit derailed at the end of yesterday, I found the
> discussion to be very useful. 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.
>
> 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.
>
>
>  On Mon, Feb 17, 2014 at 11:42 PM, Jason Gross <jasongross9 at gmail.com>wrote:
>
>>  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.
>>
>> 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
>> *foo* out of the group, and I'm not getting it" or "keep doing what
>> you're doing" or "more/fewer exercises" or something else.
>>
>> 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 The
>> Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible<http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible/>,
>> which was perhaps a mistake, given that I botched the presentation.  I will
>> leave it up to those interested to read the blog post<http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible/>,
>> Nicolai's Agda code<http://red.cs.nott.ac.uk/~ngk/html-trunc-inverse/trunc-inverse.html>,
>> or my own Coq version of it <https://gist.github.com/JasonGross/9064514>.
>>  I think the essence of it is that you can extract information even from
>> contractible types, which I show in a much shorter Coq example<https://gist.github.com/JasonGross/9064636> 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.)
>>
>> -Jason
>>
>> _______________________________________________
>> HoTT-reading-group mailing list
>> HoTT-reading-group at mit.edu
>> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>>
>>
>
>
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/
>
> _______________________________________________
> HoTT-reading-group mailing list
> HoTT-reading-group at mit.edu
> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140218/eb49152b/attachment.htm