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 the existence of a dependent function ${\mathsf{rec}}_{\mathbf{2}}:\prod_{(C:{\mathcal{U}})} C\to C\to {\mathbf{2}}\to C$ defined by the equations ${\mathsf{rec}}_{\mathbf{2}}(C,c_0,c_1,0_{\mathbf{2}}):\equiv c_0$ and ${\mathsf{rec}}_{\mathbf{2}}(C,c_0,c_1,1_{\mathbf{2}}):\equiv c_1$.

Can we prove the recursor from the induction principle?

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 recursion principle of ${\mathbf{2}}$ states that to give a function $f:{\mathbf{2}}\to A$ is equivalent to give terms $a_0,a_1:A$. The function $f$ satisfies the defining equations $f(0_{\mathbf{2}}):\equiv a_0$, $f(1_{\mathbf{2}}):\equiv a_1$. This can be formalized as the existence of its recursor, which is a dependent function ${\mathsf{rec}}_{\mathbf{2}}:\prod_{(C:{\mathcal{U}})} C\to C\to {\mathbf{2}}\to C$ defined by the equations ${\mathsf{rec}}_{\mathbf{2}}(C,c_0,c_1,0_{\mathbf{2}}):\equiv c_0$ and ${\mathsf{rec}}_{\mathbf{2}}(C,c_0,c_1,1_{\mathbf{2}}):\equiv c_1$.

Can we prove the recursion principle from the induction principle?

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?

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 the existence of a dependent function ${\mathsf{rec}}_{\mathbf{2}}:\prod_{(C:{\mathcal{U}})} C\to C\to {\mathbf{2}}\to C$ defined by the equations ${\mathsf{rec}}_{\mathbf{2}}(C,c_0,c_1,0_{\mathbf{2}}):\equiv c_0$ and ${\mathsf{rec}}_{\mathbf{2}}(C,c_0,c_1,1_{\mathbf{2}}):\equiv c_1$.

Can we prove the recursor from the induction principle?