[HoTT-reading-group] Today; Next Monday

[Chris Jeris]

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/20140224/475acd4a/attachment-0001.htm