A categorical outlook on relational modalities and simulations

We characterise bicategories of spans, relations and partial maps universally in terms of factorisations involving maps. We apply this characterisation to show that the standard modalities □ and ⋄ arise canonically as extensions of a predicate logic from functions to (abstract) relations. When relations and partial maps are representable, we exhibit logical predicates for the power-object and partial-map-classifier monads. We also show that the □ modality gives the relevant pullbacks of subobjects in the internal logic of categories of partial maps. Organising modal formulae fibrationally, we exhibit an intrinsic relationship between their satisfaction relative to transition systems and the notion of simulation. In this setting, we use the biclosed structure of the bicategory of relations to give a new proof of the standard fact that observational similarity implies similarity.