Previously, I was confused about how the inductor for the type could be well defined, since we aren’t assuming that every object of that type has the form 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.
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 . In the general case, you would need the elimination rule for 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 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.