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?

  • $\begingroup$ 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. $\endgroup$
    – Seul Baek
    Jan 29, 2016 at 4:19
  • $\begingroup$ I think \circ for function composition is what you need. $\endgroup$
    – hardmath
    Jan 29, 2016 at 4:25
  • $\begingroup$ I looked again and they're called path concatenation operators, not composition. I meant the small square dots used for concatenating paths. $\endgroup$
    – Seul Baek
    Jan 29, 2016 at 4:37
  • $\begingroup$ 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$. $\endgroup$ Jan 29, 2016 at 5:44

1 Answer 1


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$.

  • $\begingroup$ "The point is that f takes path concatenation to composition of equivalences, so that f^-1 does the opposite." This was one of the approaches I tried, but I couldn't prove this fact. If you don't mind, could you give a bit more detail on this? Taking @Pierre-Yves Gaillard's comment into consideration, I'm guessing the idea is that f acts like idtoequiv, so f(p ⬝ q) = (p ⬝ q)⁎ = q⁎ ∘ p⁎ = f(q) ∘ f(p). But I'm not sure this will work, since the endpoints of domain (a = a) and codomain (2 ≃ 2) of f are different, whereas they must be the same for idtoequiv. $\endgroup$
    – Seul Baek
    Jan 29, 2016 at 8:11
  • $\begingroup$ $f$ is idtoequiv composed with $\mathsf{ap}$ of the projection $X \to \mathcal{U}$, and $\mathsf{ap}$ always preserves concatenation. $\endgroup$ Jan 29, 2016 at 21:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.