In HoTT Lecture, https://www.youtube.com/watch?v=VWmXF-P4-Z8&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z&index=7, Harper introduced a dependent form of recursion rule:
$$
\Gamma \vdash M : Nat ~~~ \Gamma,z: Nat \vdash C ~\text{type} ~~~ \Gamma \vdash N : [O/z] C ~~~ \Gamma, x : Nat, y : [x/z] C \vdash P : [S(x)/z] C\over \Gamma \vdash \text{rec}[z.C](M, N, xy.P) : [M/z]C
$$
and beta rules:
$$
\text{rec}[z.C](O, N, x,y. P) \equiv N \\
\text{rec}[z.C](S(M), N, x,y. P) \equiv [M, rec[z.C](M, N, x, y . P) / x, y]P \\
$$
And then an exercise was left as the following:
$$
\prod x: Nat. (\text{Id}_{Nat}(S(x), O) \to \bot)
$$
To proof this, I want to construct something like:
$$
\lambda x : \text{Nat} ~ \lambda m : \text{Id(S(x), O)}~ \text{rec}[…](…) : \bot
$$
But I have no idea how could I construct such recursion rule to lead to a bottom type.
Moreover, it seems to me that if my motive is bottom, then the rule implies that I need to first have some N that is of bottom type. But there is not any instance that is of bottom type, so how come I can construct such recursion rule?
Best Answer
I'll give you the informal answer.
First, construct a function $f : \mathbb{N} \to Type$ defined by $\DeclareMathOperator{Id}{Id}$
$$f(0) = \bot$$ $$f(S(n)) = \top$$
Then, prove $\prod n, m : \mathbb{N}, (\Id_\mathbb{N}(n, m) \to f(n) \to f(m))$ using path induction.
Then if we have $\Id(S(x), 0)$, then we have $f(S(x)) \to f(0)$. That is, we have $\top \to \bot$.
Now $\top$ is a true proposition, so we can conclude $\bot$. Or in other words, there is some element $* : \top$, so therefore we can use our function $\top \to \bot$ to get an element of $\bot$.
In order to give you a formal answer, you would need to include your rule for path induction.
Edit: let's proceed with a slightly more formal proof.
To define $f : \mathbb{N} \to Type$, we define
$$f :\equiv \lambda n . rec[z.Type](n, \bot, xy. \top)$$
Then, we define $g : \prod n, m : \mathbb{N}, (\Id_\mathbb{N}(n, m) \to f(n) \to f(m))$ by
$$g :\equiv \lambda n . \lambda m . \lambda p . J[n, m, z . f(n) \to f(m)](p; x . \lambda y . y)$$
Now, we define $h : \prod x : \mathbb{N}, \Id(S(x), 0) \to \bot$ by
$$h :\equiv \lambda x . \lambda p . g(S(x), 0, p)(*)$$
To proceed with maximum formality and with no intermediate definitions at all, we have
$$\lambda x . \lambda p . (\lambda n . \lambda m . \lambda . p . J[n, m, z . (\lambda n . rec[z.Type](n, \bot, xy. \top))(n) \to (\lambda n . rec[z.Type](n, \bot, xy. \top))(m)](p; x . \lambda y . y)) ((S(x), 0, p)(*) : \prod x : \mathbb{N}, \Id(S(x), 0) \to \bot$$