-The type we gave the `pair` function above is a specific instance of
-the more general type, with `α`, `β`, and `ρ` all set to `N`.
-Many practical type systems guarantee that under reasonably general
-conditions, there will be a ***principle type***: a type such that
-every other possible type for that expression is a more specific
-version of the principle type.
+The number specific type we gave the `pair` function above (i.e.,
+`N->N->(N->N->N)->N`) is a specific instance of the more general type,
+with `α`, `β`, and `ρ` all set to `N`. Many practical type systems
+guarantee that under reasonably general conditions, there will be a
+***principal type***: a type such that every other possible type for
+that expression is a more specific version of the principal type.