<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"?)<div>
<br></div><div>-Jason</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 class="h5">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 class="h5"><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 class="">_______________________________________________<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>