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?



Does the induction principle of the type of booleans imply its recursion principle?
Recursion principles are usually special cases of induction principles in dependent type theory. For example, for the boolean type $\mathbf{2}$, given $a\_0, a\_1 : A$, we may form (using the induction principle) the function $f : \prod\_{x : \mathbf{2}} A$ where $f (0\_{\mathbf{2}}) \equiv a\_0$ and $f(0\_{\mathbf{1}}) \equiv a\_1$; but $\prod\_{x : \mathbf{2}} A \equiv (\mathbf{2} \to A)$ (see §1.4 of the HoTT book; formally, the RHS abbreviates the LHS), so we we deduce the recursion principle. One can then use $\lambda$-abstraction to obtain the recursor $\mathsf{rec}\_{\mathbf{2}}$ if so desired. Alternatively, we could take
$$\mathsf{rec}\_{\mathbf{2}} \equiv (\lambda C : \mathcal{U}) (\lambda c\_0 : C) (\lambda c\_1 : C) (\lambda x : \mathbf{2}) \mathsf{ind}\_{\mathbf{2}} ((\lambda y : \mathbf{2}) C, c\_0, c\_1, x) $$
and then verify that it does what we want.


