[HoTT-reading-group] Today; Next Monday

[Jason Gross]

Your description in 1. fails to match the example; an inverse of f : A -> B
needs to be a function B -> A, not a function forall b : B, P b.  (In this
case, P b unifies with A whenever b is jundgmentally a constructor of B; so
it only acts as an inverse in the judgmental image of f, but not in the
rest of B.)

-Jason
On Feb 18, 2014 12:17 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-_-ℕ-‖ℕ‖-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/b8dda770/attachment.htm