Abstract
A type theory constructed with reference to a particular language will associate with each monadic predicate P of that language a class of individuals C(P) of which it is categorically significant to predicate P (or which P spans, for short). The extension of P is a subset of C(P), which is a subset of the language’s universe of discourse. The set C(P) is a category discriminated by the language. The relation 'is spanned by the same predicates as' divides the language’s universe of discourse into equivalence classes. These are the types discriminated by the language. This paper criticizes an attempt by Peter Strawson to explain terms peculiar to type theory in terms of other notions not peculiar to type theory