Lax extensions (also called relators or relation liftings) are a categorical notion for reasoning about functors acting on functions and relations in a compatible way. They play a central role in developing sound proof principles for behavioral equivalence of state-based systems and are also important in establishing contextual equivalence for effectful programs. In this talk, I will present a theory of lax extensions for parametrized functors and monads, and consider notions of behavioral preorders, equivalence relations, and metrics that can be modulated by additional parameters. From an operational viewpoint, this leads to a refinement of contextual equivalence and metrics: instead of quantifying over all possible contexts, one can regulate the allowed contexts via chosen parameters. From a categorical perspective, ordinary lax extensions can be characterized as lax double functors on the double category of relations. In our setting, the guiding examples for parametrized lax extensions arise from monads induced by double parametrized adjunctions, such as the state monad.
Joint work with Ugo Dal Lago.