Identity-Preserving Lax Extensions and Where to Find Them
Sergey Goncharov, Dirk Hofmaan, Pedro Nora, Lutz Schröder, Paul Wild
TL;DR
This work addresses the existence of identity-preserving (normal) lax extensions for endofunctors in universal coalgebra, which underpin robust notions of bisimulation across diverse system types. It proves a necessary condition: any functor with a normal lax extension must preserve $1/4$-iso pullbacks, and frames Barr extension as the canonical baseline. It then provides two broad sufficient criteria for the existence of a normal lax extension: (i) weak preservation of inverse images; or (ii) weak preservation of $1/4$-iso pullbacks together with $4/4$-epi pullbacks (and related variants). These results yield concrete consequences, such as a monoid-valued functor $M^{(-)}$ having a normal lax extension iff $M$ is positive, and establish bridges to monotone predicate liftings and expressive coalgebraic modal logics for relevant system types like neighbourhood and weighted transition systems.
Abstract
Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems.