Merge branch '8.8.3' of https://github.com/peterlefanulumsdaine/book …

…into fpvandoorn-8.8.3

errata.tex

@@ -716,10 +716,7 @@
   %
   \cref{thm:whiteheadn}
   & % merge of 1026-g8c2bc9d
-  & There was a hole in the last line of the proof of \cref{thm:whiteheadn}. After applying the
-  induction hypothesis, it needs to be checked that for any $p : a = a$ the map $\pi_k(\apfunc
-  f):\pi_k(x = x,p) \to \pi_k(f(x) = f(x),\apfunc f(p))$ is a bijection, while the proof only
-  checked this for $p\equiv\refl{a}$.\\
+  & After applying the induction hypothesis, it additionally needs to be checked that for every path $p : a = a$ the map $\pi_k(\apfunc f):\pi_k(x = x,p) \to \pi_k(f(x) = f(x),\apfunc f(p))$ is a bijection. \\
   %
   % Chapter 9
   %

homotopy.tex

@@ -2441,16 +2441,13 @@ \section{Whitehead's theorem and Whitehead's principle}
   Thus, suppose it to be true for all functions between $n$-types, and let $A$ and $B$ be $(n+1)$-types and $f:A\to B$ as above.
   The first condition in \cref{thm:whitehead1} holds by assumption, so it will suffice to show that for any $x:A$, the function $\Omega f: \Omega(A,x) \to \Omega(B,f(x))$ is an equivalence.
 
-  Since $\Omega(A,x)$ and $\Omega(B,f(x))$ are $n$-types we can apply the induction hypothesis.  We
-  need to check that $\trunc 0{\Omega f}$ is a bijection and that for all $p : x = x$ the map
-  $\pi_k(\Omega f):\pi_k(x = x,p) \to \pi_k(f(x) = f(x),\Omega f(p))$ is a bijection for $k\geq1$.
-  The first statement is given, since $\trunc 0{\Omega f}=\pi_1(f)$. To prove the second statement,
-  we generalize it first. We prove that for all $y : A$ and $q : x = y$ we have $\pi_k(\apfunc
-  f):\pi_k(x = y,q) \to \pi_k(f(x) = f(y),\apfunc f(q))$. This is indeed a generalization, because
-  $\pi_k(\Omega f)=\pi_k(\apfunc f)$ if we identify the base points $\Omega f(p)=\apfunc f(p)$. To
-  prove the generalization, we use path induction, so it's sufficient to prove it for $q \equiv
-  \refl{a}$. In this case, we have $\pi_k(\apfunc f) = \pi_k(\Omega f) = \pi_{k+1}(f)$, and it's
-  given that $\pi_{k+1}(f)$ is an bijection.
+  Since $\Omega(A,x)$ and $\Omega(B,f(x))$ are $n$-types we can apply the induction hypothesis.
+  We need to check that $\trunc 0{\Omega f}$ is a bijection, and that for all $k\geq1$ and $p : x = x$ the map $\pi_k(\Omega f):\pi_k(x = x,p) \to \pi_k(f(x) = f(x),\Omega f(p))$ is a bijection.
+  The first statement holds by assumption, since $\trunc 0{\Omega f} \jdeq \pi_1(f)$.
+  To prove the second statement, we generalize it first: we show that for all $y : A$ and $q : x = y$ we have $\pi_k(\apfunc f):\pi_k(x = y,q) \to \pi_k(f(x) = f(y),\apfunc f(q))$.
+  This implies the desired statement, since when $y\defeq x$, we have $\pi_k(\Omega f)=\pi_k(\apfunc f)$ modulo identifying their base points $\Omega f(p)=\apfunc f(p)$.
+  To prove the generalization, it suffices by path induction to prove it when $q$ is $\refl{a}$.
+  In this case, we have $\pi_k(\apfunc f) = \pi_k(\Omega f) = \pi_{k+1}(f)$, and $\pi_{k+1}(f)$ is an bijection by the original assumptions.
 \end{proof}
 
 Note that if $A$ and $B$ are not $n$-types for any finite $n$, then there is no way for the induction to get started.