Behavioural equivalences for coalgebras with unobservable moves

• Categories enriched over the category of CPOs with binary joins and continuous maps are studied as a host for endomorphism saturation.
• A construction to embed CPO-enriched categories into a category admitting saturation is presented and shown to be equivalent to any such embedding.
• Weak behavioural equivalences are defined in terms of homomorphisms-of-endomorphisms (cf. kernel bisimulation) from a saturated system.
• Implications of left (resp. right) distributivity of binary joins w.r.t. weak and strong behavioural equivalences are investigated.
• The framework is shown to instantiate to several existing weak behavioural equivalences and to be applicable to complex settings like presheaves.

We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on special order enriched categories, i.e. categories whose hom-sets are endowed with suitable complete orders. Using this structure we provide an abstract notion of saturation, which allows us to define various (weak) behavioural equivalences. We show that the Kleisli categories of many common monads are categories of this kind. On one hand, this allows us to instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences; on the other, we can readily provide new weak behavioural equivalences for more complex behaviours, like those definable on presheaves, topological spaces, measurable spaces, etc.