December 29th
Today I learned some examples of type-theoretic recursion and induction. On a high level, recursion (and induction) tell us how we can define (dependent) functions on a type. Often these are best thought of as rules/axioms the way that a group or ring has rules/axioms.
I think the clearest way that this works is with products. We would like to say that we can define a function $f:A\times B\to C$ (for $A,B,C:\mathcal U$) based on (say) curried two-variable functions $A\to B\to C.$ (Ordered pairs are primitive objects.) The way we formalize this is by creating a machine which creates functions $A\times B\to C$ based on our curried functions. This machine is\[\op{rec}_{A\times B}:\prod_{C:\mathcal U}(A\to B\to C)\to(A\times B\to C).\]The way I'm thinking about this is as what we described—a function which takes our output type $C:\mathcal U$ (hidden in the $\prod$) and a curried function $g:A\to B\to C$ and outputting a function $A\times B\to C.$ Well, what does $\op{rec}$ do? We write\[\op{rec}_{A\times B}(C,g)((a,b)):\equiv g(a)(b).\]Because of how loose we're being with currying over functions with multiple inputs, we could also think about this like\[\op{rec}_{A\times B}(C,g,(a,b)):\equiv g(a)(b),\]but I find this less enlightening.
It's a bit more complicated to do this with dependent functions, which is induction. Instead of taking a type $C$ as input, we have to take a family $C:A\times B\to\mathcal U.$ Then we may write\[\op{ind}_{A\times B}:\prod_{C:A\times B\to\mathcal U}\left(\prod_{a:A}\prod_{b:B}C((a,b))\right)\to\prod_{x:A\times B}C(x).\]Again, read this as taking a family $C:A\times B\to\mathcal U$ and a dependent function $g:\prod_{a:A}\prod_{b:B}C((a,b))$ and then outputting the natural dependent function in $\prod_{x:A\times B}C(x).$ (Danger: $\prod_{x:A}$ refers to a function with a variable in $A.$) Which function? Well, we have\[\op{ind}_{A\times B}(C,g)((a,b)):\equiv g(a)(b).\]Again, one might get more mileage thinking about this like $\op{ind}_{A\times B}(C,g,(a,b))\equiv g(a)(b).$
The generalized example of these is with dependent pairs. Again, we'd like to say that we can define a function on the pair $\sum_{x:A}B$ (for family $B:A\to\mathcal U$) by some sufficiently curried function. This is done with the recursor, writing\[\op{rec}_{\sum_{x:A}B(x)}:\prod_{C:\mathcal U}\left(\prod_{x:A}(B(x)\to C)\right)\to\left(\sum_{x:A}B(x)\to C\right).\]This notation means that the recursor takes our output type $C:\mathcal U$ and a curried dependent function $g:\prod_{x:A}B(x)\to C$ and outputs a function on the dependent pair. (Danger: $\prod_{x:A}B(x)\to C$ is indeed curried! Its first input is $a:A.$) It does so in the natural way, by\[\op{rec}_{\sum_{x:A}B(x)}(C,g)((a,b)):\equiv g(a)(b).\]Similarly, we have the induction\[\op{ind}_{\sum_{x:A}B(x)}:\prod_{C:\sum_{x:A}B(x)\to\mathcal U}\left(\prod_{x:A}\prod_{y:B(x)}C((x,y))\right)\to\prod_{p:\sum_{x:A}B(x)}C(p).\]As usual, this is taking a family $C:\sum_{x:A}B(x)\to\mathcal U$ as input in addition to a dependent curried function $g:\prod_{x:A}\prod_{b:B}C((x,y))$ and then outputs a dependent function on the dependent pair. This is done in the natural way, by\[\op{ind}_{\sum_{x:A}B(x)}(C,g)((a,b)):\equiv g(a)(b).\]Don't mind the subscripts in subscripts.
I guess I should say what this has to do with induction and recursion in $\NN.$ Well, recursion is usually the way we define functions on $\NN$ using the successor structure of $\NN.$ Abstractly, this is what we've been doing above with pairs—we're describing how to define functions on our type to use its structure. To be explicit, we define recursion as\[\op{rec}_\NN:\prod_{C:\mathcal U}C\to(\NN\to C\to C)\to(\NN\to C).\]Before actually defining what recursion, we say that it's a curried dependent function (as usual) taking out output type $C,$ a base case $c_0:C,$ and a successor function $c_s:\NN\to C\to C$; we output the desired function $\NN\to C.$ Now, $\op{rec}_\NN$ is defined as \[\begin{cases} \op{rec}_\NN(C,c_0,c_s)(0):\equiv c_0, \\ \op{rec}_\NN(C,c_0,c_s)(\op{succ}(n)):\equiv c_s(\op{rec}_\NN(C,c_0,c_s,n)).\end{cases}\]Induction is similar but for dependent functions, defined as\[\op{ind}_\NN:\prod_{C:\NN\to\mathcal U}C(0)\to\left(\prod_{n:\NN}C(n)\to C(\op{succ}(n))\right)\to\prod_{n:\NN}C(n).\]Again, we take a family $C:\NN\to\mathcal U,$ a base case $c_0:C(0),$ and a successor (curried!) dependent function $g:\prod_{n:\NN}C(n)\to C(\op{succ}(n)).$ We output the corresponding function in $\prod_{n:\NN}C(n).$ Explicitly, we have\[\begin{cases} \op{ind}_\NN(C,c_0,c_s)(0):\equiv c_0. \\ \op{ind}_\NN(C,c_0,c_s)(\op{succ}(n)):\equiv c_s(\op{ind}_\NN(C,c_0,c_s)(n)).\end{cases}\]This is like the induction that we're used to because we'll have propositions as types later. Namely, if we think about the family $C$ as a property that we want to prove over all $n:\NN,$ then induction is saying that if we can exhibit a certificate $C(0)$ and show how to generate certificates $C(n+1)$ "given'' $C(n),$ then there is a certificate $C(n)$ for each $n:\NN.$ This is the induction we're used to.