 The translations above can be extended to first-order hybrid logic, in which case the relevant target logic is two-sorted first-order logic with equality, one sort for worlds and one sort for individuals, see Chapter 6 of Braüner (2011a). In the case of intensional first-order hybrid logic, three sorts are employed, the third sort being for intensions, see Chapter 7 of Braüner (2011a).