[proofplan] Use the eliminator for the inductive type $\mathbb{N}_0$ with constant motive $C$, base value $c_0$, and step function $s$ to construct the recursive function. The defining computation rules of the eliminator give the equations at $0$ and at successors. For uniqueness, compare two candidate functions pointwise by induction on $n : \mathbb{N}_0$; the base case uses the common initial value, and the successor case applies congruence to the common step function. Function extensionality then upgrades pointwise equality to equality of functions. [/proofplan] [step:Construct the recursive function from the natural-number eliminator] Let $P : \mathbb{N}_0 \to \mathsf{Type}$ be the constant type family defined by \begin{align*} P(n) = C \end{align*} for every $n : \mathbb{N}_0$. The dependent induction principle for $\mathbb{N}_0$, understood as the type-valued natural-number eliminator, applied to the base term $c_0 : P(0)$ and the step term \begin{align*} \lambda n.\lambda y. s(n,y) : \prod_{n:\mathbb{N}_0} P(n) \to P(S(n)) \end{align*} gives a dependent function \begin{align*} r : \prod_{n:\mathbb{N}_0} P(n). \end{align*} Since $P$ is constant, this is a function \begin{align*} r : \mathbb{N}_0 \to C. \end{align*} Define \begin{align*} \operatorname{rec}_{\mathbb{N}_0}(c_0,s) := r. \end{align*} [guided] The construction is exactly the eliminator for the inductive type of natural numbers, specialized to a constant target type. We define a type family $P : \mathbb{N}_0 \to \mathsf{Type}$ by setting \begin{align*} P(n) = C \end{align*} for every $n : \mathbb{N}_0$. Thus proving an element of $\prod_{n:\mathbb{N}_0}P(n)$ is the same as defining a function from $\mathbb{N}_0$ into $C$. The assumed dependent induction principle for $\mathbb{N}_0$ is being used in its type-valued eliminator form. This eliminator requires two pieces of data: a value in the fiber over $0$, and a rule that constructs a value over $S(n)$ from a value over $n$. The base value is \begin{align*} c_0 : P(0), \end{align*} because $P(0)=C$. The step rule is the function \begin{align*} \lambda n.\lambda y. s(n,y) : \prod_{n:\mathbb{N}_0} P(n) \to P(S(n)). \end{align*} This has the required type because $P(n)=C$ and $P(S(n))=C$. Applying the eliminator gives \begin{align*} r : \prod_{n:\mathbb{N}_0} P(n). \end{align*} Since the family $P$ is constant, we regard $r$ as a function \begin{align*} r : \mathbb{N}_0 \to C. \end{align*} We name this function \begin{align*} \operatorname{rec}_{\mathbb{N}_0}(c_0,s) := r. \end{align*} [/guided] [/step] [step:Verify the computation rules at zero and successors] By the computation rule for the natural-number eliminator at $0$, the constructed function satisfies \begin{align*} \operatorname{rec}_{\mathbb{N}_0}(c_0,s)(0) = c_0. \end{align*} For every $n : \mathbb{N}_0$, the successor computation rule for the same eliminator gives \begin{align*} \operatorname{rec}_{\mathbb{N}_0}(c_0,s)(S(n)) = s(n,\operatorname{rec}_{\mathbb{N}_0}(c_0,s)(n)). \end{align*} Thus the asserted recursive equations hold. [/step] [step:Prove pointwise uniqueness by induction on the natural number] Let \begin{align*} f,g : \mathbb{N}_0 \to C \end{align*} be functions satisfying the two recursion equations propositionally. Denote their base witnesses by \begin{align*} p_0^f : f(0)=c_0 \end{align*} and \begin{align*} p_0^g : g(0)=c_0, \end{align*} and their successor witnesses by \begin{align*} p_S^f(n) : f(S(n)) = s(n,f(n)) \end{align*} and \begin{align*} p_S^g(n) : g(S(n)) = s(n,g(n)) \end{align*} for each $n : \mathbb{N}_0$. For terms $a,b : C$, write $\operatorname{Id}_C(a,b)$ for the identity type of paths from $a$ to $b$ in $C$. Define the proposition-valued family \begin{align*} Q : \mathbb{N}_0 \to \mathsf{Type} \end{align*} by \begin{align*} Q(n) = \operatorname{Id}_C(f(n),g(n)). \end{align*} For the base case, compose $p_0^f$ with the inverse of $p_0^g$ to obtain \begin{align*} q_0 : Q(0). \end{align*} For the successor step, assume $n : \mathbb{N}_0$ and $q_n : Q(n)$. Define \begin{align*} s_n : C \to C \end{align*} by \begin{align*} s_n(y)=s(n,y). \end{align*} By [citetheorem:9635] applied to $s_n$ and the path $q_n$, there is a path denoted by $\operatorname{ap}_{s_n}(q_n)$, where $\operatorname{ap}_{s_n}$ is the congruence action of the function $s_n$ on identity paths: \begin{align*} \operatorname{ap}_{s_n}(q_n) : s(n,f(n)) = s(n,g(n)). \end{align*} Composing $p_S^f(n)$, this path, and the inverse of $p_S^g(n)$ gives \begin{align*} q_{S(n)} : f(S(n)) = g(S(n)). \end{align*} The [citetheorem:9620] applied to the family $Q$ therefore gives \begin{align*} q : \prod_{n:\mathbb{N}_0} f(n)=g(n). \end{align*} [guided] We now show that two functions satisfying the same primitive-recursion equations must agree at every [natural number](/page/Natural%20Number). Let \begin{align*} f,g : \mathbb{N}_0 \to C \end{align*} be two such functions. Since the equations are assumed propositionally, we record the witnesses. The base witnesses are \begin{align*} p_0^f : f(0)=c_0 \end{align*} and \begin{align*} p_0^g : g(0)=c_0. \end{align*} For every $n : \mathbb{N}_0$, the successor witnesses are \begin{align*} p_S^f(n) : f(S(n)) = s(n,f(n)) \end{align*} and \begin{align*} p_S^g(n) : g(S(n)) = s(n,g(n)). \end{align*} The predicate for induction is pointwise equality of the two functions. For terms $a,b : C$, the notation $\operatorname{Id}_C(a,b)$ denotes the identity type of paths from $a$ to $b$ in $C$. Define \begin{align*} Q : \mathbb{N}_0 \to \mathsf{Type} \end{align*} by \begin{align*} Q(n)=\operatorname{Id}_C(f(n),g(n)). \end{align*} Thus proving $\prod_{n:\mathbb{N}_0}Q(n)$ means proving $f(n)=g(n)$ for each natural number $n$. For the base case, both $f(0)$ and $g(0)$ are equal to $c_0$. The path $p_0^f$ goes from $f(0)$ to $c_0$, while $p_0^g$ goes from $g(0)$ to $c_0$. Using symmetry and transitivity of identity paths, as supplied by the identity-type rules and justified by [citetheorem:9633], we compose $p_0^f$ with the inverse of $p_0^g$ and obtain \begin{align*} q_0 : f(0)=g(0). \end{align*} This is exactly an element of $Q(0)$. For the successor step, fix $n : \mathbb{N}_0$ and assume the induction hypothesis \begin{align*} q_n : Q(n). \end{align*} Unfolding $Q$, this says \begin{align*} q_n : f(n)=g(n). \end{align*} We must prove \begin{align*} f(S(n))=g(S(n)). \end{align*} The recursion equations reduce the left and right sides to expressions involving the same step function $s$: \begin{align*} p_S^f(n) : f(S(n)) = s(n,f(n)) \end{align*} and \begin{align*} p_S^g(n) : g(S(n)) = s(n,g(n)). \end{align*} The only remaining issue is to compare $s(n,f(n))$ and $s(n,g(n))$. For this fixed $n$, define the map \begin{align*} s_n : C \to C \end{align*} by \begin{align*} s_n(y)=s(n,y). \end{align*} By [citetheorem:9635], [congruence of functions](/theorems/9635) applied to $s_n$ and the path $q_n$ gives a path denoted by $\operatorname{ap}_{s_n}(q_n)$. Here $\operatorname{ap}_{s_n}$ is the operation that sends an identity path in the domain of $s_n$ to the induced identity path between the corresponding values of $s_n$: \begin{align*} \operatorname{ap}_{s_n}(q_n) : s(n,f(n)) = s(n,g(n)). \end{align*} Now we concatenate the three paths: first $p_S^f(n)$ from $f(S(n))$ to $s(n,f(n))$, then $\operatorname{ap}_{s_n}(q_n)$ from $s(n,f(n))$ to $s(n,g(n))$, and finally the inverse of $p_S^g(n)$ from $s(n,g(n))$ to $g(S(n))$. This yields \begin{align*} q_{S(n)} : f(S(n))=g(S(n)). \end{align*} We have produced a base term $q_0 : Q(0)$ and a successor operation taking $q_n : Q(n)$ to $q_{S(n)} : Q(S(n))$. Therefore the [citetheorem:9620] gives \begin{align*} q : \prod_{n:\mathbb{N}_0} f(n)=g(n). \end{align*} This is pointwise equality of $f$ and $g$. [/guided] [/step] [step:Apply function extensionality to conclude equality of functions] The term \begin{align*} q : \prod_{n:\mathbb{N}_0} f(n)=g(n) \end{align*} is pointwise equality of the functions $f$ and $g$. By [citetheorem:9638], function extensionality converts this pointwise equality into a path \begin{align*} f=g. \end{align*} Hence the function $\operatorname{rec}_{\mathbb{N}_0}(c_0,s)$ is unique among functions $\mathbb{N}_0 \to C$ satisfying the two primitive-recursion equations. [/step]