Computing Id on eliminators

[mikeshulman]

Since Id doesn't reduce to the first component of ap, it should have all the same computation rules as the latter (as should the other pieces of IdU: tr, lift, etc.). The only cases when this is possible is for eliminators, like function application, projection, induction, etc. But those are important to achieve definitional Id-naturality in the object-language.

• [x] function application
• [ ] projections
• [ ] sum case
• [ ] bool case
• [ ] nat ind
• [ ] int case