[HoTT-reading-group] Regarding the "nearly invertible" truncation map (Re: Today; Next Monday)

[Jason Gross]

As a result of discussion with David, I've posted a blog post which I hope
will clarify this issue:
http://homotopytypetheory.org/2014/02/24/composition-is-not-what-you-think-it-is-why-nearly-invertible-isnt/.
 Let me know if anything is unclear or if you have further questions or
comments.

-Jason


On Tue, Feb 18, 2014 at 12:35 PM, Ryan Wisnesky <wisnesky at math.mit.edu>wrote:

> The last comment in the thread linked to by David is pretty interesting.
>
> Mike Shulman: I have to say that this trick makes me a bit more suspicious
> of all judgmental equalities. Maybe even beta-reduction should be
> propositional.
>
> Proof assistants based on extensional type theory, like NuPRL, end up
> having to keep around entire typing derivations to witness places where
> beta reduction happens - because in extensional type theory, it is unsound
> to arbitrarily beta reduce under binders.  Interesting that propositional
> beta-reduction would show up again in a type theory (HoTT) that is “more
> extensional” than intensional type theory.
>
> On Feb 18, 2014, at 12:16 PM, David Spivak <dspivak at gmail.com> wrote:
>
> 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-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-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
>>
>>
> _______________________________________________
> 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/20140224/46f4f1c2/attachment.htm