[proofplan] For each inductive type, the corresponding non-dependent primitive recursor supplies the desired function and its beta computation rules. Uniqueness is proved by the matching structural induction principle: induction on natural numbers, list induction on the tail, and tree induction on both subtrees. In each inductive step, the recursion equation for the competing function and the recursion equation for the recursor reduce equality at a compound constructor to the induction hypothesis for its immediate recursive arguments. Finally, pointwise equality is upgraded to equality of functions exactly when function extensionality is assumed. [/proofplan]

[step:Construct the natural-number recursor and record its computation rules] Fix a type $B$, an element $b_0:B$, and a function \begin{align*} s:\mathbb N_0\to B\to B. \end{align*} By the [primitive recursion theorem for natural numbers](/theorems/9619), available as part of the stated structure on $\mathbb N_0$, applied to the constant target type $B$, the initial value $b_0$, and the step function $s$, there is a function \begin{align*} f:\mathbb N_0\to B \end{align*} satisfying the beta computation rules \begin{align*} f(0)=b_0 \end{align*} and, for every $n:\mathbb N_0$, \begin{align*} f(S(n))=s(n,f(n)). \end{align*} These are judgmental computation rules when the recursor is judgmental; otherwise they are the propositional computation equalities supplied with the recursor. [/step]

[step:Prove uniqueness for the natural-number recursor by induction]Let \begin{align*} g:\mathbb N_0\to B \end{align*} be a function satisfying \begin{align*} g(0)=b_0 \end{align*} and, for every $n:\mathbb N_0$, \begin{align*} g(S(n))=s(n,g(n)). \end{align*} Define the dependent predicate \begin{align*} P:\mathbb N_0\to\mathsf{Type} \end{align*} by \begin{align*} P(n)=\operatorname{Id}_B(g(n),f(n)). \end{align*} For $n=0$, the equation for $g$ gives $g(0)=b_0$, and the equation for $f$ gives $f(0)=b_0$. Applying symmetry to the second equality and then transitivity of identity, we obtain a term of $P(0)$. Now assume $n:\mathbb N_0$ and an induction hypothesis \begin{align*} p_n:\operatorname{Id}_B(g(n),f(n)). \end{align*} The successor equations give \begin{align*} g(S(n))=s(n,g(n)) \end{align*} and \begin{align*} f(S(n))=s(n,f(n)). \end{align*} Applying congruence of the function \begin{align*} s(n,-):B\to B \end{align*} to $p_n$ yields \begin{align*} s(n,g(n))=s(n,f(n)). \end{align*} Combining these three equalities by transitivity gives \begin{align*} g(S(n))=f(S(n)). \end{align*} Thus we have constructed a term of $P(S(n))$. The [induction principle for natural numbers](/theorems/9620), available as part of the stated structure on $\mathbb N_0$, applied to the family $P$, the base term just constructed, and the successor construction just described, yields \begin{align*} \prod_{n:\mathbb N_0}\operatorname{Id}_B(g(n),f(n)). \end{align*} Equivalently, $g(n)=f(n)$ for every $n:\mathbb N_0$.[/step]

[guided]In this step, $B$ is a fixed type, $b_0:B$ is the chosen initial value, $s:\mathbb N_0\to B\to B$ is the chosen step function, and $f:\mathbb N_0\to B$ is the function supplied by primitive recursion with equations $f(0)=b_0$ and $f(S(n))=s(n,f(n))$. We also have a competing function $g:\mathbb N_0\to B$ satisfying $g(0)=b_0$ and $g(S(n))=s(n,g(n))$ for every $n:\mathbb N_0$. We prove uniqueness by comparing $g$ and $f$ at each input number. The right predicate for induction is the pointwise equality predicate \begin{align*} P:\mathbb N_0\to\mathsf{Type} \end{align*} defined by \begin{align*} P(n)=\operatorname{Id}_B(g(n),f(n)). \end{align*} This choice is forced by the conclusion: to prove the two functions agree pointwise, we must prove $P(n)$ for every $n:\mathbb N_0$. For the base case, the defining equation for $g$ gives \begin{align*} g(0)=b_0, \end{align*} and the computation equation for $f$ gives \begin{align*} f(0)=b_0. \end{align*} Using symmetry on the second equality if necessary and then transitivity of identity, these two paths give \begin{align*} g(0)=f(0). \end{align*} This is precisely a term of $P(0)$. For the successor case, fix $n:\mathbb N_0$ and assume the induction hypothesis \begin{align*} p_n:\operatorname{Id}_B(g(n),f(n)). \end{align*} We must construct a path \begin{align*} \operatorname{Id}_B(g(S(n)),f(S(n))). \end{align*} The recursive equations reduce both sides at the successor input to applications of the same step function: \begin{align*} g(S(n))=s(n,g(n)) \end{align*} and \begin{align*} f(S(n))=s(n,f(n)). \end{align*} The only remaining difference is between $g(n)$ and $f(n)$, and that is exactly what the induction hypothesis supplies. Applying congruence to the map \begin{align*} s(n,-):B\to B \end{align*} and the path $p_n$ gives \begin{align*} s(n,g(n))=s(n,f(n)). \end{align*} Transitivity with the two successor computation equations gives \begin{align*} g(S(n))=f(S(n)). \end{align*} So the induction step produces a term of $P(S(n))$. The induction principle for natural numbers, available as part of the stated structure on $\mathbb N_0$, applies because we have defined a dependent family $P:\mathbb N_0\to\mathsf{Type}$, constructed a base term in $P(0)$, and constructed a successor operation sending each $p_n:P(n)$ to a term of $P(S(n))$. Its conclusion is \begin{align*} \prod_{n:\mathbb N_0}P(n), \end{align*} that is, \begin{align*} \prod_{n:\mathbb N_0}\operatorname{Id}_B(g(n),f(n)). \end{align*} Thus $g(n)=f(n)$ for every $n:\mathbb N_0$.[/guided]

[step:Construct the list recursor and prove its uniqueness by list induction] Fix a type $C$, an element $c_0:C$, and a function \begin{align*} c_1:A\to\mathsf{List}(A)\to C\to C. \end{align*} By the list primitive recursion principle for the inductive type $\mathsf{List}(A)$, applied to the constant target type $C$, the nil value $c_0$, and the cons step $c_1$, there is a function \begin{align*} h:\mathsf{List}(A)\to C \end{align*} with beta computation rules \begin{align*} h(\mathsf{nil})=c_0 \end{align*} and, for every $a:A$ and $\ell:\mathsf{List}(A)$, \begin{align*} h(\mathsf{cons}(a,\ell))=c_1(a,\ell,h(\ell)). \end{align*} Let \begin{align*} k:\mathsf{List}(A)\to C \end{align*} satisfy the same equations: \begin{align*} k(\mathsf{nil})=c_0 \end{align*} and, for every $a:A$ and $\ell:\mathsf{List}(A)$, \begin{align*} k(\mathsf{cons}(a,\ell))=c_1(a,\ell,k(\ell)). \end{align*} Define \begin{align*} Q:\mathsf{List}(A)\to\mathsf{Type} \end{align*} by \begin{align*} Q(\ell)=\operatorname{Id}_C(k(\ell),h(\ell)). \end{align*} At $\mathsf{nil}$, the two base equations give \begin{align*} k(\mathsf{nil})=c_0=h(\mathsf{nil}), \end{align*} so $Q(\mathsf{nil})$ holds. For the cons case, fix $a:A$, $\ell:\mathsf{List}(A)$, and an induction hypothesis \begin{align*} p_\ell:\operatorname{Id}_C(k(\ell),h(\ell)). \end{align*} The recursion equations give \begin{align*} k(\mathsf{cons}(a,\ell))=c_1(a,\ell,k(\ell)) \end{align*} and \begin{align*} h(\mathsf{cons}(a,\ell))=c_1(a,\ell,h(\ell)). \end{align*} Applying congruence of the function \begin{align*} c_1(a,\ell,-):C\to C \end{align*} to $p_\ell$ gives \begin{align*} c_1(a,\ell,k(\ell))=c_1(a,\ell,h(\ell)). \end{align*} Transitivity gives \begin{align*} k(\mathsf{cons}(a,\ell))=h(\mathsf{cons}(a,\ell)). \end{align*} The list induction principle applies because $Q:\mathsf{List}(A)\to\mathsf{Type}$ is a dependent predicate, $Q(\mathsf{nil})$ was constructed, and the cons construction sends each $p_\ell:Q(\ell)$ to a term of $Q(\mathsf{cons}(a,\ell))$. Therefore it gives \begin{align*} \prod_{\ell:\mathsf{List}(A)}\operatorname{Id}_C(k(\ell),h(\ell)). \end{align*} Thus $k(\ell)=h(\ell)$ for every $\ell:\mathsf{List}(A)$. [/step]

[step:Construct the tree recursor and prove its uniqueness by tree induction] Fix a type $D$, a function \begin{align*} d_0:A\to D, \end{align*} and a function \begin{align*} d_1:\mathsf{Tree}(A)\to\mathsf{Tree}(A)\to D\to D\to D. \end{align*} By the tree primitive recursion principle for the inductive type $\mathsf{Tree}(A)$, applied to the constant target type $D$, the leaf step $d_0$, and the node step $d_1$, there is a function \begin{align*} r:\mathsf{Tree}(A)\to D \end{align*} with beta computation rules, for every $a:A$, \begin{align*} r(\mathsf{leaf}(a))=d_0(a) \end{align*} and, for every $t_1,t_2:\mathsf{Tree}(A)$, \begin{align*} r(\mathsf{node}(t_1,t_2))=d_1(t_1,t_2,r(t_1),r(t_2)). \end{align*} Let \begin{align*} q:\mathsf{Tree}(A)\to D \end{align*} satisfy the same equations: \begin{align*} q(\mathsf{leaf}(a))=d_0(a) \end{align*} for every $a:A$, and \begin{align*} q(\mathsf{node}(t_1,t_2))=d_1(t_1,t_2,q(t_1),q(t_2)) \end{align*} for every $t_1,t_2:\mathsf{Tree}(A)$. Define \begin{align*} R:\mathsf{Tree}(A)\to\mathsf{Type} \end{align*} by \begin{align*} R(t)=\operatorname{Id}_D(q(t),r(t)). \end{align*} For a leaf $\mathsf{leaf}(a)$, the two leaf equations give \begin{align*} q(\mathsf{leaf}(a))=d_0(a)=r(\mathsf{leaf}(a)), \end{align*} so $R(\mathsf{leaf}(a))$ holds. For a node, fix $t_1,t_2:\mathsf{Tree}(A)$ and induction hypotheses \begin{align*} p_1:\operatorname{Id}_D(q(t_1),r(t_1)) \end{align*} and \begin{align*} p_2:\operatorname{Id}_D(q(t_2),r(t_2)). \end{align*} The recursion equations give \begin{align*} q(\mathsf{node}(t_1,t_2))=d_1(t_1,t_2,q(t_1),q(t_2)) \end{align*} and \begin{align*} r(\mathsf{node}(t_1,t_2))=d_1(t_1,t_2,r(t_1),r(t_2)). \end{align*} First applying congruence in the third argument of $d_1(t_1,t_2,-,q(t_2))$ to $p_1$, and then congruence in the fourth argument of $d_1(t_1,t_2,r(t_1),-)$ to $p_2$, gives \begin{align*} d_1(t_1,t_2,q(t_1),q(t_2))=d_1(t_1,t_2,r(t_1),r(t_2)). \end{align*} By transitivity with the two node computation equations, \begin{align*} q(\mathsf{node}(t_1,t_2))=r(\mathsf{node}(t_1,t_2)). \end{align*} The tree induction principle applies because $R:\mathsf{Tree}(A)\to\mathsf{Type}$ is a dependent predicate, $R(\mathsf{leaf}(a))$ was constructed for every $a:A$, and the node construction sends hypotheses for $t_1$ and $t_2$ to a term of $R(\mathsf{node}(t_1,t_2))$. Therefore it gives \begin{align*} \prod_{t:\mathsf{Tree}(A)}\operatorname{Id}_D(q(t),r(t)). \end{align*} Thus $q(t)=r(t)$ for every $t:\mathsf{Tree}(A)$. [/step]

[step:Upgrade pointwise equalities to equalities of functions under function extensionality] The previous steps give pointwise equalities \begin{align*} \prod_{n:\mathbb N_0}\operatorname{Id}_B(g(n),f(n)), \end{align*} \begin{align*} \prod_{\ell:\mathsf{List}(A)}\operatorname{Id}_C(k(\ell),h(\ell)), \end{align*} and \begin{align*} \prod_{t:\mathsf{Tree}(A)}\operatorname{Id}_D(q(t),r(t)). \end{align*} When function extensionality is available, applying it respectively to the constant families over $\mathbb N_0$, $\mathsf{List}(A)$, and $\mathsf{Tree}(A)$ shows that these pointwise paths induce paths \begin{align*} g=f, \end{align*} \begin{align*} k=h, \end{align*} and \begin{align*} q=r. \end{align*} This proves the claimed computation and uniqueness principles for natural numbers, lists, and binary trees. [/step]