I'm having difficulty with the following from theorem 4.1.3:
Finally, Exercise 2.13 implies that every equivalence $2 \simeq 2$ is equal to either $id_2$ or $e$, so we can show (iii) by a four-way case analysis.
The first part (any $f : 2 \rightarrow 2$ that is an equivalence is either $id_2$ or $e$) is easy to show, but this fact cannot be used directly to case-analyze the conclusion we need
$iii : \Pi\space(p : a = a),\space (p \cdot q) = (q \cdot p)$
because it does not include terms of type $2 \simeq 2$. We do know, however, that $(a = a) \simeq (2 \simeq 2)$, so there is an $f : (a = a) \rightarrow (2 \simeq 2)$ which is an equivalence. So for any given $p$, we can expand the above using $p = f^{-1}(f(p))$ and $q = f^{-1}(f(q))$, and case-analyze on $f(p)$ and $f(q)$. Of the 4 cases thus obtained, 2 are reflexive, and the other 2 are symmetrical to each other. So it remains to show
$f^{-1}\langle id_2,\_\rangle \cdot f^{-1}\langle e,\_\rangle = f^{-1}\langle e,\_\rangle \cdot f^{-1}\langle id_2,\_\rangle$
where underscores are proofs that $id_2$ and $e$ are equivalences. And I'm not sure how to proceed from here. Is there a way to show this, or is there a different kind of solution?
The point is that $f$ takes path concatenation to composition of equivalences, so that $f^{-1}$ does the opposite. So you can pull out the $f^{-1}$s and reduce your goal to the obvious fact $\mathrm{id}_2 \circ e = e \circ \mathrm{id}_2$.