Do we always have $(A\times (A \to 0)) \simeq 0$? I'm skimming through the HoTT book.
Let $A:\mathcal U$. We have a function $\phi:\equiv((x,f)\mapsto f x):A\times(A\to 0)\to 0$ witnessing the principle of non-contradiction, and the "absurd" function $\psi:0\to A\times(A\to 0)$ satisfies $\phi\circ\psi=\text{id}_0$.
I can see that if $A$ is a mere proposition, then $A\times(A\to 0)$ is also a mere proposition because $A\to 0$ always is, so $\psi\circ\phi=\text{id}_{A\times(A\to 0)}$ and hence we have the isomorphism in the title. Then my question is:

is it neccesary to assume $\mathsf{isProp}(A)$ for this to be the case?

or equivalently, is $A\times(A\to 0)$ always a mere proposition? I have a feeling that this should be the case, but since I come from proof-irrelevant classical logic I'm not sure whether I should trust my intuition hahah. Anyway I don't see an obvious way to prove this. Really any hint would be great. Thanks in advance.

Suppose $x : A \times (A \to 0)$. Then $\phi(x):0$. You also have a function $\psi':0\to (\psi\circ\phi(x)=x)$, so you have $\psi'(\phi(x)):\psi\circ\phi(x)=x$.
And therefore $\lambda(x).\psi'(\phi(x)) :\psi \circ\phi\sim\mathsf{id}_{A \times (A \to 0)}$, which is what you were missing.
