Here's my opinion: the exercises should not be in `HoTTBook.v`; instead, they should be separated into their own file. Exercises in general will need a bit more explanation and contain more code, and generally one isn't going to be flipping through the exercises looking for a theorem they need in the main library.

(The fuss, by the way, is because the exercise asks for it, and isn't actually an important distinction.)