-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 base types
+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