I'm reading the HoTT book, section 2.4, where for $f : A \to B$, they define $$\mathsf{qinv}(f) = \sum_{g:B\to A} \big( (f \circ g \sim \mathrm{id}) \times (g \circ f \sim \mathrm{id}) \big)$$ $$\mathsf{isequiv}(f) = \sum_{g:B\to A} (f \circ g \sim \mathrm{id})\ \times \sum_{h:B\to A} (h \circ f \sim \mathrm{id})$$
I can't understand how the following assertions don't result in a direct contradiction:
- "for a single function $f : A \to B$ there may be multiple unequal inhabitants of $\mathsf{qinv}(f)$."
- "For any two inhabitants $e_1,e_2 : \mathsf{isequiv}(f)$ we have $e_1 = e_2$."
considering there is a map $\mathsf{qinv}(f) \to \mathsf{isequiv}(f)$ which sends $(g,\alpha,\beta) : \mathsf{qinv}(f)$ to $(g,\alpha,g,\beta) : \mathsf{isequiv}(f)$.
How can it be that you have two elements $$(g,\alpha,\beta), (g',\alpha',\beta') : \mathsf{qinv}(f)$$ with $(g,\alpha,\beta) \neq (g',\alpha',\beta')$, but then when you map it over to $\mathsf{isequiv}(f)$, suddenly $(g,\alpha,g,\beta) = (g',\alpha',g',\beta')$?
I've tried reading the arguments in Chapter 4, but they are currently buried a few layers too deep for me to understand. If there's a simple example with $A, B$ as groupoids or something, that would be nice to see.
$\require{AMScd}$ $\newcommand{\base}{\mathsf{base}}$ $\newcommand{\loop}{\mathsf{loop}}$ $\newcommand{\refl}{\mathsf{refl}}$ $\newcommand{\qinv}{\mathsf{qinv}}$ Here's a particular example. Consider the circle type, $S^1$. It's defined inductively by:
$$\base : S^1 \\ \loop : \base = \base$$
So, there is a distinguished base point, and a non-trivial loop that is meant to be like winding around the circle once. We can also use this to define a generalized $\loop_x : x = x$ for $x : S^1$, which is a single closed loop around the circle beginning and ending at $x$. Importantly, this closed loop is distinct from $\refl$. Topologically, you cannot deform $\loop_x$ to $\refl$ without cutting the loop at $x$ and unwinding it. One way of visualizing this is that there is no square like this:
$$ \begin{CD} x @>{\refl}>> x \\ @V{\refl}VV ⇒ @VV{\loop}V \\ x @>>{\refl}> x \end{CD} $$
but there are squares like this:
$$ \begin{CD} x @>{\loop^{-1}}>> x \\ @V{\refl}VV ⇒ @VV{\loop}V \\ x @>>{\refl}> x \end{CD} $$
I.E. we can only deform $\refl$ into $\loop$ by winding one of the ends around the circle relative to the other. The top represents moving the origin point, and the bottom the destination point, while the sides are the paths we're transforming.
Now, let's consider $\qinv(f)$ where $f : S^1 → S^1$ defined as $f\ x = x$. That probably seems really trivial. $f$ can serve as its own inverse, and then we need to give two examples of $x = x$ for $x : S^1$. So, here are two examples of a $\qinv(f)$:
$$(f, λx. \refl_x, λx. \refl_x)$$ $$(f, λx. \refl_x, λx.\loop_x)$$
Are these the same? No. To prove that these values of $\qinv(f)$ are the same, we'd need to give $r_x : x = x$ (equivalent to a proof of $f = f$) such that there are squares:
$$ \begin{CD} x @>r_x>> x \\ @VpVV ⇒ @VVp'V \\ x @>>{\refl}> x \end{CD} $$
where $p$ and $p'$ are corresponding half-inverse proofs. However, this is a problem. If we want to mediate between two $\refl$ proofs, the correct choice for $r$ is $\refl$. If we want to mediate between $\refl$ and $\loop$, we need $\loop^{-1}$ mentioned above. So, whichever $r$ we choose will be wrong for one of the squares.
On the other hand to prove the corresponding $\mathsf{isequiv(f)}$ values equivalent we need to specify two mediators, $r_x : x = x$ and $s_x : x = x$, which each satisfy a corresponding square. So, we can give that proof, because of the extra degree of freedom. As András Kovács points out, just because there isn't a single $r$ that simultaneously satisfies both squares doesn't mean there isn't $r$ and $s$ that each satisfy a square.