[HoTT-reading-group] Today; Next Monday

[Chris Jeris]

Yes, I had just gotten there, and lifting that out simplifies the proof
down to something usable:



On Tue, Feb 25, 2014 at 9:19 AM, Jason Gross <jasongross9 at gmail.com> wrote:

> Can you use the fact that [ap f ∘ ap g = ap (f ∘ g)] and then factor out
> a proof that if f is pointwise the identity, then [ap f] is an equivalence?
>  (Would that help make the proof more "high-level"?)
>
> -Jason
>
>
> On Mon, Feb 24, 2014 at 11:14 PM, Chris Jeris <cjeris at gmail.com> wrote:
>
>> I played with it for a bit longer and I don't think the alternative proof
>> of 2.11.1 that I was heading toward is genuinely different.  If you start
>> like this:  (see
>> https://github.com/ystael/hott-sandbox/blob/master/exercises/Exercises4.agdafor context)
>>
>> equiv-ap′ : ∀ {i} {A B : Type i} (e : A ≃ B) →
>>             (x y : A) → is-equiv (ap (–> e) {x} {y})
>> equiv-ap′ {_} {A} {B} e x y =
>>   equiv-2/6.f-equiv f g h gf-equiv hg-equiv (is-eq-2/6 f g h gf-equiv
>> hg-equiv)
>>   where
>>     f : x == y → –> e x == –> e y
>>     f = ap (–> e)
>>
>>     g : –> e x == –> e y → x == y
>>     g q = ! (<–-inv-l e x) ∙ ap (<– e) q ∙ <–-inv-l e y
>>
>>     h :  x == y → –> e x == –> e y
>>     h = ap (–> e)
>>
>>     gf-equiv : is-equiv (g ∘ f)
>>     gf-equiv = {!!}
>>
>>     hg-equiv : is-equiv (h ∘ g)
>>     hg-equiv = {!!}
>>
>> then you end up essentially repeating the "three sides of the square"
>> proof from the text to show that g o f is homotopic to the identity.  If
>> you instead charge forward:
>>
>>   where
>>     f : x == y → –> e x == –> e y
>>     f = ap (–> e)
>>
>>     g : –> e x == –> e y → <– e (–> e x) == <– e (–> e y)
>>     g = ap (<– e)
>>
>>     h : <– e (–> e x) == <– e (–> e y) → –> e (<– e (–> e x)) == –> e (<–
>> e (–> e y))
>>     h = ap (–> e)
>>
>> then you have to do the same work in a different place: one would like to
>> say that g ∘ f = ap (idf A), and you can get this pointwise, but lifting
>> that to the function level with extensionality is obstructed by the fact
>> that the codomain type of g is not x == y.  It's intuitively obvious
>> that ap (<– e) ∘ ap (–> e)ought to be an equivalence -- in fact it ought
>> to be the identity -- but I haven't succeeded in getting it to go through
>> yet, and in any case I don't know that this is really the "higher level"
>> proof the book is alluding to.
>>
>> peace, Chris
>>
>>
>> On Mon, Feb 24, 2014 at 4:44 PM, Jason Gross <jasongross9 at gmail.com>wrote:
>>
>>> I forgot to mention, we also talked a bit about object classifiers and
>>> the fibrations.
>>>
>>> -Jason
>>>
>>>
>>> On Mon, Feb 24, 2014 at 4:22 PM, Jason Gross <jasongross9 at gmail.com>wrote:
>>>
>>>> Hi,
>>>> Today we went over exercises 3.13, 3.14, and most of 4.5 (we didn't
>>>> quite manage the higher-level proof of 2.11.1).  The Coq code that I wrote
>>>> for these is here<https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBookExercises.v#L343>
>>>> .
>>>>
>>>> For next week, please read chapter 5 (on induction), and do exercises
>>>> 5.2, 5.3, 5.4, and 5.5.
>>>>
>>>> -Jason
>>>>
>>>
>>>
>>> _______________________________________________
>>> 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/20140225/32b52fc2/attachment-0001.htm