Elimination vs. Compuation – dissolving my confusion

Previously, I was confused about  how the inductor for the type A\times B could be well defined, since we aren’t assuming that every object of that type has the form (a, b). Though my resolution was basically correct, I didn’t realize until later when I was trying to understand identity types that my understanding of the issue was not complete. It wasn’t until after I had waded through appendix A.2 that I finally got this.

An elimination rule is only saying that given an object of our new type, along with some other things, we can create something of an already known type. This doesn’t tell us what exactly it is though – we need a computation rule to get that. And the computation rule only tells us how to compute this when we created it through an introduction rule.

For example, let’s look at the product type again. Our introduction rule says we can construct an object of type A\times B from an object a : A and an object b : B, with (a, b) : A\times B. We also have an elimination rule which tells us that given a type family C : A\times B\rightarrow \mathcal U, and a function g: \prod_{x: A}\prod_{y:B}C((x,y)), we have our inductor for the type, which is an object \mathsf {ind}_{A\times B} of type \displaystyle\prod_{C:A\times B\rightarrow\mathcal U}\left(\prod_{x: A}\prod_{y:B}C((x,y))\right)\rightarrow\prod_{x:A\times B}C(x). The computation rule then says that when we have an object of type A\times B which we constructed using our introduction rule,  then we can define what the inductor does in this case. So we can say that for a : A and b : B,  \mathsf {ind}_{A\times B}(C,g, (a,b)):\equiv g(a)(b).

I also said last time that the recursor was not just a baby version of the inductor, since I thought you needed the recursor to define the inductor. But actually, that’s not the case.

Using the above example again, consider your function of type C: A\times B \rightarrow \mathcal U. In the general case, you would need the elimination rule for A\times B to define such a function. But in the case where this is a constant function, you can just define the function using the computation rule for function types, since you don’t have to worry about the defining expression \mathbf\Phi having the correct type, being constant. And this case is just the recursor! So yes, you do need what is essentially the recursor to get your feet off the ground, but you don’t have to define the recursor seperately first.