I have two questions regarding the empty type, $0$, in Martin-Löf type theory:
I was reading that, in intuitionistic logic, one has $\neg\neg\neg P\rightarrow \neg P$. This amounts to finding a term of $$ (P\times 0\times 0\rightarrow 0)\rightarrow (P \rightarrow 0) $$
Is it true that $0\rightarrow P$ for any $P$? If $P$ is inhabited, then we have $p:P$ and we can just define the constant function. If $P=0$, then identity works. But, I can't seem to find a general proof of this fact.