Locating reaction with 2-categories

Groupoidal relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. In this paper, we develop the theory of GRPOs further, proving that well-known equivalences, other than bisimulation, are congruences. To demonstrate the type of category theoretic arguments which are inherent in the 2-categorical approach, we construct GRPOs in a category of 'bunches and wirings.' Finally, we prove that the 2-categorical theory of GRPOs is a generalisation of the approaches based on Milner's precategories and Leifer's functorial reactive systems.