Fix typos in the proof of Theorem 8.4.6

errata.tex

@@ -716,6 +716,12 @@
   & 1181-g3e51973
   & In the proof, $(x:A)$ should be $(x:X)$.\\
   %
+  \cref{thm:les}
+  & % merge of 9065dea
+  & In the proof, $\trunc0g\circ\trunc0f$ should be $\trunc0f\circ\trunc0g$, and similarly for $g\circ f$.
+  Also, $g(t)=w'$ should be $\tproj0{g(t)}=w'$.
+  Finally, $\tproj0{(w,p)}:\tproj0{\hfib{f}{z_0}}$ should be $\tproj0{(w,p)}:\trunc{0}{\hfib{f}{z_0}}$.\\
+  %
   \cref{thm:conn-pik}
   & 1023-gf188aeb
   & The proof requires a separate argument for $k=0$.\\

homotopy.tex

@@ -1110,12 +1110,12 @@ \section{Fiber sequences and the long exact sequence}
   %
   is exact, i.e.\ that $\im(\trunc0g)\subseteq\ker(\trunc0f)$ and $\ker(\trunc0f)\subseteq\im(\trunc0g)$.
 
-  The first inclusion is equivalent to $\trunc0g\circ\trunc0f=0$, which holds by functoriality of $\truncf0$ and the fact that $g\circ f=0$.
-  For the second, we assume $w':\trunc0W$ and $p':\trunc0f(w')=\tproj0{z_0}$ and show there merely exists ${t:\hfib{f}{z_0}}$ such that $g(t)=w'$.
+  The first inclusion is equivalent to $\trunc0f\circ\trunc0g=0$, which holds by functoriality of $\truncf0$ and the fact that $f\circ g=0$.
+  For the second, we assume $w':\trunc0W$ and $p':\trunc0f(w')=\tproj0{z_0}$ and show there merely exists ${t:\hfib{f}{z_0}}$ such that $\tproj0{g(t)}=w'$.
   Since our goal is a mere proposition, we can assume that $w'$ is of the
   form $\tproj0w$ for some $w:W$.
   Now by \cref{thm:path-truncation}, $p' : \tproj0{f(w)}=\tproj0{z_0}$ yields $p'': \trunc{-1}{f(w)=z_0}$, so by a further truncation induction we may assume some $p:f(w)=z_0$.
-  But now we have $\tproj0{(w,p)}:\tproj0{\hfib{f}{z_0}}$ whose image under $\trunc0g$ is $\tproj0w\jdeq w'$, as desired.
+  But now we have $\tproj0{(w,p)}:\trunc{0}{\hfib{f}{z_0}}$ whose image under $\trunc0g$ is $\tproj0w\jdeq w'$, as desired.
 
   Thus, applying $\truncf0$ to the fiber sequence of $f$, we obtain a long exact sequence involving the pointed sets $\pi_k(F)$, $\pi_k(X)$, and $\pi_k(Y)$ in the desired order.
   And of course, $\pi_k$ is a group for $k\ge1$, being the 0-truncation of a loop space, and an abelian group for $k\ge 2$ by the Eckmann--Hilton argument