-fragment---involved a simply-typed version of the Predicate Calculus
-with lambda abstraction. More specifically, Montague called the
-semantic part of the PTQ fragment `Intensional Logic'. Montague's IL
-had three base types: `e`, for individuals, `t`, for truth values, and
-`s` for evaluation indicies (world-time pairs). The set of types was
-defined recursively:
-
- e, t, s are types
+fragment---included a simply-typed version of the Predicate Calculus
+with lambda abstraction.
+
+Montague called the semantic part of his PTQ fragment *Intensional
+Logic*. Without getting too fussy about details, we'll present the
+popular Ty2 version of the PTQ types, roughly as proposed by Gallin
+(1975). [See Zimmermann, Ede. 1989. Intensional logic and two-sorted
+type theory. *Journal of Symbolic Logic* ***54.1***: 65--77 for a
+precise characterization of the correspondence between IL and
+two-sorted Ty2.]
+
+We'll need three base types: `e`, for individuals, `t`, for truth
+values, and `s` for evaluation indicies (world-time pairs). The set
+of types is defined recursively:
+
+ the base types e, t, and s are types