 Shifting to intensional type theory deals with this difficulty. The intension of any expression X is a function from possible worlds to an extension of the type which that expression has in the extensional theory just sketched, if it has such an extension, otherwise to something appropriate for intensional vocabulary such as ‘it is contingent that’. An intension which is a function from possible worlds to items of type t is said to be of type st. sweater, for instance, will have as its intension a function from possible worlds to functions of type ib, providing for each possible world a function that specifies the individuals which are sweaters at that world; so sweater‘s intension is of type s(ib). However, a modal sentential operator such as ‘it is contingent that’ will have as its intension a function that, for each possible world, produces the very same function, which takes as input functions of type sb and produces truth-values as output. So the extension of ‘it is contingent that’ at each world is the same function, of type (sb)b. (The operator is said to be intensional because its extension at each world is a function taking intensions, such as functions of type sb, as input.)