snippetMinor
How to prove $0\neq1$ using the J rule?
Viewed 0 times
theruleneq1proveusinghow
Problem
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?
Is there a way to prove $(0 = 1) \rightarrow \bot$? Or do I need K for that?
Solution
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$.
$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$.
Context
StackExchange Computer Science Q#45056, answer score: 7
Revisions (0)
No revisions yet.