-In the definition of the types, "`c`" is a type constant (e.g., `e` or
-`t`, or in arithmetic contexts, `N` or `Int`). "`'a`" is a type
-variable (the tick mark just indicates that the variable ranges over
-types rather than over values). "`τ1 -> τ2`" is the type of a
-function from expressions of type `τ1` to expressions of type `τ2`.
-And "`∀'a. τ`" is called a universal type, since it universally
-quantifies over the type variable `'a`. (You can expect that in
-`∀'a. τ`, the type `τ` will usually have at least one free occurrence
-of `'a` somewhere inside of it.)
+In the definition of the types, "`c`" is a type constant. Type
+constants play the role in System F that base types play in the
+simply-typed lambda calculus. So in a lingusitics context, type
+constants might include `e` and `t`. "`'a`" is a type variable. The
+tick mark just indicates that the variable ranges over types rather
+than over values; in various discussion below and later, type variable
+can be distinguished by using letters from the greek alphabet
+(α, β, etc.), or by using capital roman letters (X, Y,
+etc.). "`τ1 -> τ2`" is the type of a function from expressions of
+type `τ1` to expressions of type `τ2`. And "`∀'a. τ`" is called a
+universal type, since it universally quantifies over the type variable
+`'a`. You can expect that in `∀'a. τ`, the type `τ` will usually
+have at least one free occurrence of `'a` somewhere inside of it.