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.

  • 2
    $\begingroup$ 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. $\endgroup$
    – Zhen Lin
    Jul 17, 2020 at 15:56

1 Answer 1


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.

  • $\begingroup$ OOOH this is so nice. Thanks a lot! $\endgroup$ Jul 17, 2020 at 16:56
  • $\begingroup$ Ah, so you need function extensionality to prove this... $\endgroup$
    – Zhen Lin
    Jul 17, 2020 at 22:56
  • $\begingroup$ @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$. $\endgroup$
    – L. Garde
    Jul 18, 2020 at 5:35

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .