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.

*construct*an object of type from an object and an object , with . We also have an elimination rule which tells us that given a type family , and a function , we have our inductor for the type, which is an object of type . The

*rule then says that*

**computation***when*we have an object of type which we constructed

*using our introduction rule,*

**then**we can define what the inductor does in this case. So we can say that for and , .

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.