[proofplan]
The natural numbers are being used as an inductive type with constructors $0$ and $S$. The proof is therefore the dependent eliminator for that inductive type: to define a term in the family $P(n)$ for arbitrary $n:\mathbb{N}_0$, it suffices to give the base term at $0$ and a successor step taking a proof at $n$ to a proof at $S(n)$. The two displayed computation rules are exactly the beta rules for this eliminator at the two constructors.
[/proofplan]
[step:Invoke the dependent eliminator for the inductive type $\mathbb{N}_0$]
Fix a universe $\mathcal U$, a type family $P:\mathbb{N}_0\to\mathcal U$, a base term $p_0:P(0)$, and a dependent step function
\begin{align*}
p_S:\prod_{n:\mathbb{N}_0} P(n)\to P(S(n)).
\end{align*}
Since $\mathbb{N}_0$ is assumed to be the inductive type generated by $0$ and $S$, its dependent elimination rule applies to the motive $P$, the base branch $p_0$, and the successor branch $p_S$. It yields a dependent function
\begin{align*}
\operatorname{ind}_{\mathbb{N}_0}(P,p_0,p_S):\prod_{n:\mathbb{N}_0} P(n).
\end{align*}
[guided]
We must construct, for each [natural number](/page/Natural%20Number) $n:\mathbb{N}_0$, a term of the type $P(n)$. Because the target type depends on $n$, this is not ordinary recursion into a fixed type; it is dependent elimination with motive
\begin{align*}
P:\mathbb{N}_0\to\mathcal U.
\end{align*}
The data required by the dependent eliminator are exactly the two pieces given in the statement. First, the base constructor $0:\mathbb{N}_0$ must be assigned a term of the fiber over $0$, and this is
\begin{align*}
p_0:P(0).
\end{align*}
Second, for a successor $S(n)$, the eliminator may assume that the desired term has already been constructed in the previous fiber $P(n)$. The step datum is therefore a dependent function
\begin{align*}
p_S:\prod_{n:\mathbb{N}_0} P(n)\to P(S(n)).
\end{align*}
For each $n:\mathbb{N}_0$, this means $p_S(n)$ is a function from $P(n)$ to $P(S(n))$. Applying the dependent elimination rule for the inductive type $\mathbb{N}_0$ to the motive $P$, the base branch $p_0$, and the successor branch $p_S$ gives a dependent function
\begin{align*}
\operatorname{ind}_{\mathbb{N}_0}(P,p_0,p_S):\prod_{n:\mathbb{N}_0} P(n).
\end{align*}
This is the formal expression of induction: once a term is supplied at $0$, and once terms can be transported from the fiber over $n$ to the fiber over $S(n)$, the eliminator supplies a term in every fiber $P(n)$.
[/guided]
[/step]
[step:Verify the computation rule at the base constructor]
The first computation rule for the dependent eliminator of $\mathbb{N}_0$ states that evaluating the eliminator at the constructor $0$ returns the base branch. Hence
\begin{align*}
\operatorname{ind}_{\mathbb{N}_0}(P,p_0,p_S)(0)\equiv p_0.
\end{align*}
Both sides have type $P(0)$, so the displayed definitional equality is well typed.
[/step]
[step:Verify the computation rule at successor constructors]
Let $n:\mathbb{N}_0$ be arbitrary. The second computation rule for the dependent eliminator of $\mathbb{N}_0$ states that evaluating the eliminator at the constructor $S(n)$ returns the successor branch applied to $n$ and to the recursively produced term at $n$. Therefore
\begin{align*}
\operatorname{ind}_{\mathbb{N}_0}(P,p_0,p_S)(S(n))\equiv p_S(n)(\operatorname{ind}_{\mathbb{N}_0}(P,p_0,p_S)(n)).
\end{align*}
The right-hand side is well typed: the eliminator gives
\begin{align*}
\operatorname{ind}_{\mathbb{N}_0}(P,p_0,p_S)(n):P(n),
\end{align*}
and $p_S(n):P(n)\to P(S(n))$, so its application has type $P(S(n))$. This is the same type as the left-hand side.
[/step]
[step:Conclude the dependent induction principle]
The construction supplies a dependent function
\begin{align*}
\operatorname{ind}_{\mathbb{N}_0}(P,p_0,p_S):\prod_{n:\mathbb{N}_0} P(n)
\end{align*}
and the preceding two steps establish its computation rules at $0$ and at every successor $S(n)$. Since $P$, $p_0$, and $p_S$ were arbitrary, this proves the induction principle for natural numbers.
[/step]
