<div dir="ltr"><div><span style="font-family:arial,sans-serif;font-size:13px">Sorry, fat-fingered a send there.</span></div><div><span style="font-family:arial,sans-serif;font-size:13px"><br></span></div><span style="font-family:arial,sans-serif;font-size:13px">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.</span><div>
<div><span style="font-family:arial,sans-serif;font-size:13px"><br></span></div><div><div><font face="courier new, monospace">-- This needs functional extensionality somewhere, I think ... to prove that</font></div><div><font face="courier new, monospace">-- idf ∘ idf == idf if nothing else</font></div>
<div><font face="courier new, monospace">ap-idf-is-equiv : ∀ {i} {A : Type i} (x y : A) → is-equiv (ap (idf A) {x = x} {y = y})</font></div><div><font face="courier new, monospace">ap-idf-is-equiv x y = transport is-equiv (! (λ= ap-idf)) (idf-is-equiv (x == y))</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- A function which is extensionally equal to the identity is also an equivalence when</font></div><div><font face="courier new, monospace">-- you ap it ... this is just ap-idf-is-equiv transported through the extensional equality</font></div>
<div><font face="courier new, monospace">ap-like-idf-is-equiv : ∀ {i} {A : Type i} {f : A → A} → ((a : A) → f a == a) → (x y : A) →</font></div><div><font face="courier new, monospace"> is-equiv (ap f {x = x} {y = y})</font></div>
<div><font face="courier new, monospace">ap-like-idf-is-equiv f-ext-id x y =</font></div><div><font face="courier new, monospace"> transport (λ f → is-equiv (ap f {x = x} {y = y})) (! (λ= f-ext-id)) (ap-idf-is-equiv x y)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- The idea of this alternative proof of 2.11.1 is to let the three functions be forward,</font></div><div><font face="courier new, monospace">-- back, forward through e, and observe that forward-back and back-forward are essentially</font></div>
<div><font face="courier new, monospace">-- ap idf, so the 2/6 lemma applies. We just have to do a bit of work to get there.</font></div><div><font face="courier new, monospace">equiv-ap′ : ∀ {i} {A B : Type i} (e : A ≃ B) →</font></div>
<div><font face="courier new, monospace"> (x y : A) → is-equiv (ap (–> e) {x} {y})</font></div><div><font face="courier new, monospace">equiv-ap′ {_} {A} {B} e x y =</font></div><div><font face="courier new, monospace"> equiv-2/6.f-equiv f g h gf-equiv hg-equiv (is-eq-2/6 f g h gf-equiv hg-equiv)</font></div>
<div><font face="courier new, monospace"> where</font></div><div><font face="courier new, monospace"> f : x == y → –> e x == –> e y</font></div><div><font face="courier new, monospace"> f = ap (–> e)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> g : –> e x == –> e y → <– e (–> e x) == <– e (–> e y)</font></div><div><font face="courier new, monospace"> g = ap (<– e)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> h : <– e (–> e x) == <– e (–> e y) → –> e (<– e (–> e x)) == –> e (<– e (–> e y))</font></div>
<div><font face="courier new, monospace"> h = ap (–> e)</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> gf-equiv : is-equiv (g ∘ f)</font></div><div>
<font face="courier new, monospace"> gf-equiv = transport is-equiv (λ= (ap-∘ (<– e) (–> e)))</font></div><div><font face="courier new, monospace"> (ap-like-idf-is-equiv (<–-inv-l e) x y)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> hg-equiv : is-equiv (h ∘ g)</font></div><div><font face="courier new, monospace"> hg-equiv = transport is-equiv (λ= (ap-∘ (–> e) (<– e)))</font></div>
<div><font face="courier new, monospace"> (ap-like-idf-is-equiv (<–-inv-r e) (–> e x) (–> e y))</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">peace, Chris</font></div>
<div style="font-family:arial,sans-serif;font-size:13px"><br></div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 25, 2014 at 10:29 AM, Chris Jeris <span dir="ltr"><<a href="mailto:cjeris@gmail.com" target="_blank">cjeris@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Yes, I had just gotten there, and lifting that out simplifies the proof down to something usable:<div><br>
</div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 25, 2014 at 9:19 AM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Can you use the fact that [<span style="font-family:'courier new',monospace;font-size:13px">ap f ∘ ap g = </span><span style="font-family:'courier new',monospace;font-size:13px">ap (f ∘ g)</span>] 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"?)<span><font color="#888888"><div>
<br></div><div>-Jason</div></font></span></div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Feb 24, 2014 at 11:14 PM, Chris Jeris <span dir="ltr"><<a href="mailto:cjeris@gmail.com" target="_blank">cjeris@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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 <a href="https://github.com/ystael/hott-sandbox/blob/master/exercises/Exercises4.agda" target="_blank">https://github.com/ystael/hott-sandbox/blob/master/exercises/Exercises4.agda</a> for context)<div>
<br></div><div><div><font face="courier new, monospace">equiv-ap′ : ∀ {i} {A B : Type i} (e : A ≃ B) →</font></div><div><font face="courier new, monospace"> (x y : A) → is-equiv (ap (–> e) {x} {y})</font></div>
<div><font face="courier new, monospace">equiv-ap′ {_} {A} {B} e x y =</font></div><div><font face="courier new, monospace"> equiv-2/6.f-equiv f g h gf-equiv hg-equiv (is-eq-2/6 f g h gf-equiv hg-equiv)</font></div><div>
<font face="courier new, monospace"> where</font></div><div><font face="courier new, monospace"> f : x == y → –> e x == –> e y</font></div><div><font face="courier new, monospace"> f = ap (–> e)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> g : –> e x == –> e y → x == y</font></div><div><font face="courier new, monospace"> g q = ! (<–-inv-l e x) ∙ ap (<– e) q ∙ <–-inv-l e y</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> h : x == y → –> e x == –> e y</font></div><div><font face="courier new, monospace"> h = ap (–> e)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> gf-equiv : is-equiv (g ∘ f)</font></div><div><font face="courier new, monospace"> gf-equiv = {!!}</font></div><div>
<font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> hg-equiv : is-equiv (h ∘ g)</font></div><div><font face="courier new, monospace"> hg-equiv = {!!}</font></div></div><div>
<br></div><div>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:</div><div><br></div><div>
<div><font face="courier new, monospace"> where</font></div><div><font face="courier new, monospace"> f : x == y → –> e x == –> e y</font></div><div><font face="courier new, monospace"> f = ap (–> e)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> g : –> e x == –> e y → <– e (–> e x) == <– e (–> e y)</font></div><div><font face="courier new, monospace"> g = ap (<– e)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> h : <– e (–> e x) == <– e (–> e y) → –> e (<– e (–> e x)) == –> e (<– e (–> e y))</font></div>
<div><font face="courier new, monospace"> h = ap (–> e)</font></div><div><br></div></div><div>then you have to do the same work in a different place: one would like to say that <span style="font-family:'courier new',monospace">g ∘ f = ap (idf A)</span><font face="arial, helvetica, sans-serif">, 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 </font><span style="font-family:'courier new',monospace">x == y</span><font face="arial, helvetica, sans-serif">. It's intuitively obvious that </font><font face="courier new, monospace">ap (<– e) ∘ ap (–> e)</font><font face="arial, helvetica, sans-serif">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.</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">peace, Chris</font></div>
<div class="gmail_extra"><br><br><div class="gmail_quote"><div><div>On Mon, Feb 24, 2014 at 4:44 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><div dir="ltr">I forgot to mention, we also talked a bit about object classifiers and the fibrations.<span><font color="#888888"><div>
<br></div><div>-Jason</div></font></span></div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Feb 24, 2014 at 4:22 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi,<div>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 <a href="https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBookExercises.v#L343" target="_blank">here</a>.</div>
<div><br></div><div>For next week, please read chapter 5 (on induction), and do exercises 5.2, 5.3, 5.4, and 5.5.</div><span><font color="#888888"><div><br></div><div>-Jason</div></font></span></div>
</blockquote></div><br></div>
</div></div><br></div></div><div>_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu" target="_blank">HoTT-reading-group@mit.edu</a><br>
<a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group" target="_blank">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br>
<br></div></blockquote></div><br></div></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>