HOTT 2.1 and the example on page 36 (correct or not?)