Are type abstraction values and universal types not for non functions, but only for functions?
Short Answer: In λX₁. λX₂. ... λXₙ. t it doesn't matter if t is not a function, but if so, it may not be an interesting example for introduction.

Long Answer:

First of all, technically speaking, the type system defined in Figure 23-1 does NOT have any base types such as Bool or Nat. A type of t in λX. t is either a type variable X, a function type T → T, or a universal type ∀X. T.

Section 23.4, however, takes Nat as an example. So let's consider an extended type system by adding some base types and its values, terms, typing rules, etc. like Section 11.1 does.

Then we can consider, for example, a term λX. 42. This is a well-typed term. Proof:

\[
  \cfrac{}{
  \cfrac{\mathrm{X} ⊢ \mathrm{42} : \mathrm{Nat}}{
  ∅ ⊢ \mathrm{λ X. 42} : \mathrm{∀ X. Nat}
  }}
\]

This term, however, is not very interesting; polymorphism doesn't play any important role here.

Also, we can consider a type ∀X. X. But there is no term of type ∀X. X (i.e. there is no inhabitant of ∀X. X). This can be proved through the Curry-Howard correspondence. But this example may not be suitable for introduction of System F.

Section 23.7 writes a bit more interesting example. If we extend the type system by adding errors, we can consider a term λX. error. This term doesn't throw an error during an evaluation because of the type-abstraction. This observation gives an idea of a new type erasure method, described in Section 23.7.