Closed mikeshulman closed 10 years ago
It might be possible to do an end-run around this using univalence, which would be a bit of a cheat since the correct statement of univalence also requires chapter 4, but at least it would let us give some proof of 2.11.1 in chapter 2. Thoughts?
Ah, there is yet another proof that Ben points out. The first part of the proof works to show that the composite
(a=a') --> (fa = fa') --> (f^-1 f a = f^-1 f a')
is homotopic to concatenating with beta and beta^-1, which is an equivalence. An analogous argument shows that
(fa = fa') --> (f^-1 f a = f^-1 f a') --> (f f^-1 f a = f f^-1 f a')
is homotopic to concatenating with alpha and alpha^-1. So by the 2-out-of-6 property (Exercise 4.5, which needs only quasi-inverses), all of these individual maps are equivalences.
We could also avoid explicit mention of the 2-out-of-6 property by observing that (fa = fa') --> (f^-1 f a = f^-1 f a') has a left and a right inverse, hence is an equivalence, and thus so is (a=a') --> (fa = fa') by 2-out-of-3.
What hott-amateurs list? Are the authors of the book allowed to join?
Sure why not, we need all the help we can get!
Mike
(fa = fa') --> (f^-1 f a = f^-1 f a') has a left and a right inverse
Left inverse is easy. Having trouble proving any of my candidate right inverses are actually right inverses. Can you throw me a clue?
I can never remember which is the "left" inverse and which is the "right" inverse. Its section is given by concatenating with beta and beta^-1 to get to (a = a') and then applying f. Its retraction is given by applying f and then concatenating with alpha and alpha^-1.
FWIW I fully formalised a proof of 2.11.1 using the 2-out-of-6 approach suggested by Mike. Almost trivial to state in English, but the most time consuming theorem to formalise in the book so far.
Fixed in #471. I went back and forth over how to present this, but eventually I settled on a "fully beta-reduced" version with no forward references.
The proof of the second half of theorem 2.11.1 seems to need f to be a half adjoint equivalence, not just equipped with a quasi-inverse. At least, I don't see how to do without it right now, and it's also used by the formalization
isequiv_ap
in types/Paths of HoTT/Coq.If so, this is probably the most serious bug we've found so far, since it requires reordering at least of some proofs. We could say "the proof of 2.11.1 will be given in section 4.2" and then do so.
(Thanks to Dan Piponi and Ben for bringing this up on the hott-amateurs list.)