# How to prove $0\neq1$ using the J rule?

Suppose I have a simple dependent type theory with bottom, unit, sums, dependent pairs, dependent functions, natural numbers and homogeneous identity with J-elimination.

Is there a way to prove $(0 = 1) \rightarrow \bot$? Or do I need K for that?

• Welcome to Computer Science Stack Exchange. Please read cs.stackexchange.com/tour, if you have not yet done so. – babou Aug 6 '15 at 12:05

## 1 Answer

First define a type family $P : \mathtt{Nat} \to \mathtt{Type}$ such that $P\,0 \equiv \top$ and $P\,1 \equiv \bot.$ For instance, we could define it by induction as \begin{align} P\, 0 &\equiv \bot \\ P\, (\mathtt{succ}(n)) &\equiv \top. \end{align} Let $\mathtt{tt}$ be the inhabitant of $\top$.

Suppose $e : 0 = 1$. Then, using $J$ we can formulate the transport map $\mathtt{transport}^P_e : P\,0 \to P\,1$, and use that to transport $\mathtt{tt} : P \, 0$ to $$\mathtt{transport}^P_e(\mathtt{tt}) : P \, 1.$$ We are done because $P\,1 \equiv \bot$.