Right. In practice one would want to use more complicated types (such as the type of Turing machines, explained in Clift’s thesis) but in the talk I did not have time to explain more interesting examples.