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.
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.