-In general, there is no way for a function to have a type that can
-take itself for an argument. It follows that there is no way to
-define the identity function in such a way that it can take itself as
-an argument. Instead, there must be many different identity
-functions, one for each type. Some of those types can be functions,
-and some of those functions can be (type-restricted) identity
-functions; but a simply-types identity function can never apply to itself.
+In fact, we can't even type the parts of Ω, that is, `ω
+\equiv \x.xx`. In general, there is no way for a function to have a
+type that can take itself for an argument.
+
+It follows that there is no way to define the identity function in
+such a way that it can take itself as an argument. Instead, there
+must be many different identity functions, one for each type. Some of
+those types can be functions, and some of those functions can be
+(type-restricted) identity functions; but a simply-types identity
+function can never apply to itself.