HoTT/book

Exercise 11.2 refers to a term "boundedness" which is not defined

Closed this issue · 1 comments

Exercise 11.2 says "Suppose we remove the boundedness condition in Definition 11.2.1". However, Definition 11.2.1 does not use the word boundedness anywhere. My first idea about a fix is to just change "the boundedness condition" to "the inhabited condition". I open this as an issue because (1) maybe there is another better way to word this, and (2) is it important to refer to "boundedness" as a term or a concept?

With respect to (2) I notice that [BT09] says "A real number represented as a cut is therefore a pair of subsets, i.e. an element of P(Q) × P(Q), that is rounded, bounded (i.e. inhabited), disjoint and located." but I'm not sure whether we prefer (1) to choose one term and don't try to go too deeply into the words that other works use for the same concept, or (2) to mention other terms which are "sufficiently widely" used.

I would probably prefer a double fix:

  • Change Definition 11.2.1(i) to say "inhabited (i.e. bounded)".
  • Change Exercise 11.2 to say "the boundedness condition (i)".

Then there is no possible ambiguity anywhere.