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

• It is not necessary to assume you have a proposition. I do not remember the proof, but you can show that every map into $0$ is an equivalence. Jul 17, 2020 at 15:56

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.
• @Zhen Lin no, you need function extensionality to prove $\psi\circ\phi = \mathsf{id}_{A\times(A\to 0)}$ but to prove an equivalence you only need an homotopy $\sim$. Jul 18, 2020 at 5:35