5
$\begingroup$

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?

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

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$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.