 since in evaluating this formula at a world w we would find ourselves trying to apply the reference of contingent at w, namely, the function c just defined, to the reference of (every(woollen(sweater)))(woollen) at w, namely, the truth-value TRUE. But c requires an input of type sb, not b. So we introduce a new operator, written ^, such that if X is an expression and t is the type of X’s reference at each w, then at each w, the reference of ^X is of type st. ^X may be read as ‘the intension of X’, since the rule for ^ is that at each world, ^X refers to that function which for each world w, outputs the reference of X at w.