Fix some old names in a comment in contrib/HoTTBookExercises.v