How to prove $\sqrt{2}$ is irrational in Type Theory? Using Intuitionistic Type Theory, how would one go about proving $\sqrt{2}$ is irrational?
I read that we can not use law of excluded middle. (So does this mean we cannot use proof by contradiction).
So I assume we want to prove $\forall a,b\in \mathbb{N^2}: \lnot (a^2 = 2 b^2)$. In type theory this means we need to find an instance  $P$ of the type corresponding to the theorem. The type would be something like $\prod \limits_{a:\mathbb{N}}\prod \limits_{b:\mathbb{N}} NotEqualsQ(Square(a),Times(Two,Square(b))$. I assume. Then we might have to define these function recursively?
I'm not sure how you would find an instance of this proof.
 A: Negation is defined $\neg A := A\to \bot$, the type of naturals $\mathbb N$ is defined inductively, and addition and multiplication are defined recursively.
To prove $\Pi_{a,b:\mathbb N}\neg(a^2=2b^2)$ we can introduce variables $a,b:\mathbb N$ and a proof that $a^2=2b^2$ like so:
$$a,b:\mathbb N, p : (a^2=2b^2) \vdash \bot$$
and the goal is to construct a term of type $\bot$. (Note: I suppose this could be called a "proof by contradiction" because we derive $\neg A$ from $A\vdash\bot$, but it does not require the excluded middle. A problematic "proof by contradiction" is when we derive $A$ from a proof of $\neg A\vdash \bot$.)
The idea is to construct $c,d:\mathbb N$ such that $(c^2=2d^2)$ and $\neg(2\div d)$, and then prove that $2\div d$, from which you obtain $\bot$. Constructing $c$ and $d$ can be done by splitting cases on whether $a$ and $b$ are even or odd, assuming you've proved something of the form $$(\forall k.\phi(2k)\times\phi(2k+1))\to(\forall n.\phi(n)).$$
For a more concrete justification, you could check out this proof in Coq.
