Lax Liftings and Lax Distributive Laws

TL;DR

This paper develops a theoretical framework for lax liftings and lax distributive laws, establishing a correspondence between them and analyzing specific functors relevant to bisimulation and neighborhood structures.

Contribution

It introduces a formal notion of lax distributive laws over the powerset monad and proves an isomorphism with lax liftings, advancing the theoretical understanding of these concepts.

Findings

Lax distributive laws form a lattice isomorphic to lax liftings.

The minimal lifting for monotone bisimilarity is characterized.

The lattice of liftings for the neighborhood functor is isomorphic to P(4).

Abstract

Liftings of endofunctors on sets to endofunctors on relations are commonly used to capture bisimulation of coalgebras. Lax versions have been used in those cases where strict lifting fails to capture bisimilarity, as well as in modeling other notions of simulation. This paper provides tools for defining and manipulating lax liftings. As a central result, we define a notion of a lax distributive law of a functor over the powerset monad, and show that there is an isomorphism between the lattice of lax liftings and the lattice of lax distributive laws. We also study two functors in detail: (i) we show that the lifting for monotone bisimilarity is the minimal lifting for the monotone neighbourhood functor, and (ii) we show that the lattice of liftings for the (ordinary) neighbourhood functor is isomorphic to P(4), the powerset of a 4-element set.