Error messages should not mention Sigma and Pi

[david-christiansen]

Trying to take the car of a Nat or trying to apply an Atom as a function leads to error messages that readers of the book may not understand before they've gotten a few chapters in. It would be better if it said "not a pair type:" and "not a function type: ".

[xieyuheng]

This issue must be an invitation for PR.

[david-christiansen]

I had in fact intended it as a reminder for myself, when and/or if I got free time, but thanks!