# Case analysis in theorem 4.1.3 of the HoTT book

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?

• I manually typed in path composition operators because I don't know the LaTeX command for them, which may have been causing the problem. I replaced them with centered dots. Jan 29, 2016 at 4:19
• I think \circ for function composition is what you need. Jan 29, 2016 at 4:25
• I looked again and they're called path concatenation operators, not composition. I meant the small square dots used for concatenating paths. Jan 29, 2016 at 4:37
• By Lemma 2.3.9, Lemma 2.10.1 and Axiom 2.10.3 (univalence axiom) in the HoTT Book, it suffices to show $f\circ g=g\circ f$ for all invertible maps $f,g:\mathbf2\to\mathbf2$. Jan 29, 2016 at 5:44

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$.
• $f$ is idtoequiv composed with $\mathsf{ap}$ of the projection $X \to \mathcal{U}$, and $\mathsf{ap}$ always preserves concatenation. Jan 29, 2016 at 21:05