+Note that although this general *left* is sensitive to world of
+evaluation, it does not have the fully intensionalized type given in
+the chart above, which was `(s->e)->s->t`. This is because
+*left* does not exploit the additional resolving power provided by
+making the subject an individual concept. In semantics jargon, we say
+that *leave* is extensional with respect to its first argument.
+
+Therefore we will adopt the general strategy of defining predicates
+in a way that they take arguments of the lowest type that will allow
+us to make all the distinctions the predicate requires. When it comes
+time to combine this predicate with monadic arguments, we'll have to
+make use of various lifting predicates.
+
+Likewise, although *see* depends on the world of evaluation, it is
+extensional in both of its syntactic arguments:
+