In the view of logic in terms of type theory (cf. the Curry-Howard correspondence), the type $\neg P$ is defined as $P\to False$, and a proof of $\neg P$ is therefore a function that takes a proof of $p$ and outputs an element of $False$.
It is easy to see how one might prove a negation $neg P$ from for example a negation $t_1:\neg Q$ and $t_2:P\to Q$: simply compose the two proofs: $t_3:\neg P := \lambda p:P, t_1 (t_2 (p))$.
But how do you prove the “first” negation, which cannot make use of other proofs of negation? To make it concrete, how do we prove $1\neq 2$? (Where $1$ is defined as $succ(0)$ and $2$ as $succ(succ(0))$ in a standard inductive definition of the natural numbers).
Best Answer
If two terms are equal, then they have the same properties. Let me state this more formally. Recall that equality satisfies the following elimination principle (the Leibniz principle, sometimes called transport) in Martin-Löf Type Theory: if $x = y : A$ and $\varphi : A \rightarrow \mathcal{U}$ is a predicate, then $\varphi(x) \rightarrow \varphi(y)$. You can either take this as one of the axioms of Martin-Löf Type Theory, or if you want to be really redundant, you can prove it immediately by applying Equality Axiom J (see slide 7 for a statement) to the term $\lambda x:A. \lambda x:A. \lambda p:x=y. \varphi(x) \rightarrow \varphi(y)$.
Now, take any two types $A,B:\mathcal{U}$ and assume that $A=B$. By Leibniz's principle, for any predicate $\varphi: \mathcal{U} \rightarrow \mathcal{U}$ we have $\varphi(A) \rightarrow \varphi(B)$. So set $\varphi$ to $\lambda x: \mathcal{U}. x$ to get that $A \rightarrow B$. Discharging the assumption, we have that $(A = B) \rightarrow (A \rightarrow B)$ for any two types $A,B$.
Setting $A$ to $\top$ and $B$ to $\bot$ yields $(\top = \bot) \rightarrow (\top \rightarrow \bot)$. But by the introduction principle for $\top$, we have $(\top = \bot) \rightarrow \top$ as well. Hence, $(\top = \bot) \rightarrow \bot$ holds as I claimed.
Using the Leibniz principle, we can prove the following congruence theorem: if $x=y:A$ and $f: A \rightarrow \mathcal{U}$, then $f(x) = f(y) : \mathcal{U}$. To do this, set $\varphi$ to $\lambda z. f(x) = f(z)$ in Leibniz's principle. We obtain that if $x=y$, then $f(x) = f(x) \rightarrow f(x) = f(y)$. But $f(x)=f(x)$ holds by the reflexivity of equality, so we can conclude $f(x) = f(y)$.
Now, we can apply the trick from L. Garde's answer: define the function $g: \mathbb{N} \rightarrow \mathcal{U}$ that sends zero to $\top$ and everything successor to $\bot$ (use the induction principle for $\mathbb{N}$ to obtain this function), then use the congruence theorem on $g$ to obtain $(0 = 1) \rightarrow (\top = \bot)$. We already know that $(\top = \bot) \rightarrow \bot$, so we conclude that $(0 = 1) \rightarrow \bot$ as well.