How to prove $0\neq1$ using the J rule?
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 &amp;\equiv \bot \\
P\, (\mathtt{succ}(n)) &amp;\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$.