Exercise 4.6 (iii) in the HoTT Book Being unable to solve Exercise 4.6 (iii) in the HoTT Book, I'd be most grateful for any help.
Recall the statement of Exercise 4.6:
For $A,B:\mathcal U$, define
$$
\mathsf{idtoqinv}_{A,B}:(A=B)\to\sum_{f:A\to B}\mathsf{qinv}(f)
$$
by path induction in the obvious way. Let $\mathsf{qinv}$-$\mathsf{univalence}$ denote the modified form of the univalence axiom which asserts that for all $A,B:\mathcal U$ the function $\mathsf{idtoqinv}_{A,B}$ has a quasi-inverse.
(i) Show that $\mathsf{qinv}$-$\mathsf{univalence}$ can be used instead of univalence in the proof of function extensionality in $\S$4.9.
(ii) Show that $\mathsf{qinv}$-$\mathsf{univalence}$ can be used instead of univalence in the proof of Theorem 4.1.3.
(iii) Show that $\mathsf{qinv}$-$\mathsf{univalence}$ is inconsistent (i.e. allows construction of an inhabitant of 0). Thus, the use of a "good" version of $\mathsf{isequiv}$ is essential in the statement of univalence.
 A: I think you have to show that $\mathsf{qinv}(f)$ is a mere proposition
for all $f$. This clearly contradicts Theorem 4.1.3 which you proved in (ii).
This answer is wrong, there's a problem pointed out by Pierre-Yves Gaillard, see his answer for a correct one.
Lets rewrite $\sum_{f:A\to B} \mathsf{qinv}(f)$ as $A \backsimeq B$, so we do not confuse it with the 'correct' definition of equivalence.
To prove this we'll use Lemma 4.1.1. You'll notice that the proof of this lemma
uses the (normal) univalence axiom, but this is not a problem. If you look
closer, in the proof one first uses the logical equivalence of $\mathsf{isequiv}$ and $\mathsf{qinv}$, and only then, one applies $\mathsf{ua}$. In our case, we just don't make the first step, as our (incorrect) version of univalence gives us the desired equivalence.
We write formally the type of the lemma:
$$\mathsf{lemma} : \prod_{A,B:U} \prod_{f:A\to B} \mathsf{qinv}(f)\to(\mathsf{qinv}(f)\simeq\prod_{a:A}(a=a))$$
The hypothesis of the lemma is exactly that $f$ is an equivalence in the incorrect sense. So the lemma is equivalent to:
$$\mathsf{lemma'} : \prod_{A,B:U} \prod_{i:A\backsimeq B} (\mathsf{qinv}(\pi_1(i))\simeq\prod_{a:A}(a=a))$$
Now, what we want to prove is:
$$\prod_{A,B:U} \prod_{i:A\backsimeq B} \prod_{a:A}\pi_1(\mathsf{lemma'}_{A,B}(i))(\pi_2(i))(a) = \mathsf{refl}_a$$
Because this shows that, if $\mathsf{qinv}(f)$ is inhabited, every inhabitant
is equal, under the equivalence given by the lemma, to the function $(\lambda a.\mathsf{refl}_a)$. And thus, the type is a mere proposition.
Note that we are using function extensionality, because we only prove the
equality by evaluating in every $a:A$. We are also using function extensionality in the proof of the lemma. So item (i) is necessary.
The last goal is easy to prove. By $\mathsf{\text{qinv-univalence}}$
we can assume that $i$ comes from a path in $A=B$. And then, by path induction,
we can assume that the path is reflexivity. Then we assume:
$$i \equiv \mathsf{idtoqinv}_{X,X}(\mathsf{refl}_X)$$ 
At this point we just use the definitions of $\mathsf{lemma'}$, $\mathsf{lemma}$
in the trivial case.
This is basically the same argument given in:
https://groups.google.com/forum/#!msg/homotopytypetheory/EXWVbQNRAdE/ct89FgY1kVUJ
A: As observed by Luis, it suffices to show that, for any map $f:A\to B$, the type $\mathsf{qinv}(f)$ is a mere proposition. 
For any types $A$ and $B$ we put 
$$
(A\simeq B):\equiv\sum_{f:A\to B}\mathsf{ishae}(f),\quad(A\backsimeq B):\equiv\sum_{f:A\to B}\mathsf{qinv}(f).
$$ 
(Recall that $\mathsf{ishae}(f)$ stands for "$f$ is a half-adjoint equivalence".) By Theorem 4.2.3 and the comment preceding it, there are dependent functions 
$$
i:\prod_{A,B:\mathcal U}\prod_{f:A\to B}\mathsf{ishae}(f)\to\mathsf{qinv}(f),\quad p:\prod_{A,B:\mathcal U}\prod_{f:A\to B}\mathsf{qinv}(f)\to\mathsf{ishae}(f).
$$ 
For all $A,B:\mathcal U$ let $e(A,B):(A=B)\to(A\backsimeq B)$ be the natural map (which we assume to admit a quasi-inverse).
Claim: if $f:A\to B$ and $x:\mathsf{qinv}(f)$, then $i(A,B,f,p(A,B,f,x))=x$.
Since $(f,x):A\backsimeq B$, we can assume by $\mathsf{qinv}$-univalence and path induction that 
$$
B\equiv A,\quad f\equiv\mathsf{id}_A,\quad x\equiv e(A,A,\mathsf{refl}_A),
$$ 
and the claim follows easily from the definition of $i,p$ and $e$.
For $f:A\to B$ and $x,y:\mathsf{qinv}(f)$ we have $p(A,B,f,x)=p(A,B,f,y)$ because $\mathsf{ishae}(f)$ is a mere proposition, and the claim implies $x=y$, as required.
