Does the induction principle of the type of booleans imply its recursion principle?

Question

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?

Answer 1

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.