NOTE: Nat recursor
A recursor of \(\mathbb{N}\) is like the following
\[
\begin{aligned} & R^\mathbb{N} : C \to (C \to C) \to \mathbb{N} \to C \\& R^\mathbb{N} \; z \; s \; 0 :\equiv z \\& R^\mathbb{N} \; z \; s \; (suc \; n) :\equiv s \; (R \; z \; s \; n) \end{aligned}\]
1. double
\[
\begin{aligned} & double : \mathbb{N} \to \mathbb{N} \\& double \; 0 :\equiv 0 \\& double \; (suc \; n) :\equiv suc \; (suc \; (double \; n)) \end{aligned}\]
Can be
\[ double \; n :\equiv R^\mathbb{N} \; 0 \; (\lambda n.suc \; (suc \; n)) \]
2. Addition
\[
\begin{aligned} & + : \mathbb{N} \to \mathbb{N} \to \mathbb{N} \\& 0 \; + \; n :\equiv n \\& (suc \; m) \; + \; n :\equiv suc \; (m \; + \; n) \end{aligned}\]
Can be
\[ m \; + \; n :\equiv R^\mathbb{N} \; n \; (\lambda n.suc \; n) \; m \]