[HoTT-reading-group] Today; Next Monday

[Chris Jeris]

Sorry, fat-fingered a send there.

Yes, I had just gotten there, and lifting that out simplifies the proof
down to something usable.  There are several uses of extensionality in this
proof, which I think makes it less nice than the one from the book, but I
don't see how to avoid them as you have to turn paths on function values
into paths on functions.

-- This needs functional extensionality somewhere, I think ... to prove that
-- idf ∘ idf == idf if nothing else
ap-idf-is-equiv : ∀ {i} {A : Type i} (x y : A) → is-equiv (ap (idf A) {x =
x} {y = y})
ap-idf-is-equiv x y = transport is-equiv (! (λ= ap-idf)) (idf-is-equiv (x
== y))

-- A function which is extensionally equal to the identity is also an
equivalence when
-- you ap it ... this is just ap-idf-is-equiv transported through the
extensional equality
ap-like-idf-is-equiv : ∀ {i} {A : Type i} {f : A → A} → ((a : A) → f a ==
a) → (x y : A) →
                       is-equiv (ap f {x = x} {y = y})
ap-like-idf-is-equiv f-ext-id x y =
  transport (λ f → is-equiv (ap f {x = x} {y = y})) (! (λ= f-ext-id))
(ap-idf-is-equiv x y)

-- The idea of this alternative proof of 2.11.1 is to let the three
functions be forward,
-- back, forward through e, and observe that forward-back and back-forward
are essentially
-- ap idf, so the 2/6 lemma applies.  We just have to do a bit of work to
get there.
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 → <– 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)

    gf-equiv : is-equiv (g ∘ f)
    gf-equiv = transport is-equiv (λ= (ap-∘ (<– e) (–> e)))
                         (ap-like-idf-is-equiv (<–-inv-l e) x y)

    hg-equiv : is-equiv (h ∘ g)
    hg-equiv = transport is-equiv (λ= (ap-∘ (–> e) (<– e)))
                         (ap-like-idf-is-equiv (<–-inv-r e) (–> e x) (–> e
y))

peace, Chris



On Tue, Feb 25, 2014 at 10:29 AM, Chris Jeris <cjeris at gmail.com> wrote:

> 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/03d04b79/attachment.htm