[HoTT-reading-group] Today; Next Monday

[Jason Gross]

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/1b5be164/attachment.htm