The type of booleans, denoted by ${\mathbf{2}}$, has two terms $0_{\mathbf{2}}:{\mathbf{2}}$ and $1_{\mathbf{2}}:{\mathbf{2}}$. The induction principle of ${\mathbf{2}}$ states that, given a dependent family $C:2\to {\mathcal{U}}$ and terms $c_0:C(0_{\mathbf{2}})$, $c_1:C(1_{\mathbf{2}})$, there exists a dependent function $f:\prod_{(x:{\mathbf{2}})} C(x)$ such that $f(0_{\mathbf{2}})=c_0$ and $f(1_{\mathbf{2}})=c_1$.

The recursor of ${\mathbf{2}}$ states that to give a function $f:{\mathbf{2}}\to A$ is equivalent to give terms $a_0,a_1:A$ and add the defining equations $f(0_{\mathbf{2}}):\equiv a_0$, $f(1_{\mathbf{2}}):\equiv a_1$. This can be formalized as a dependent function, but I will not repeat this formalization here.

Can we prove the recursor from the induction principle?