Relation lifting, with an application to the many-valued cover modality

TL;DR

This paper develops a framework for relation liftings in categories enriched over a commutative quantale, generalizing classical results and enabling applications like predicate liftings in metric spaces and the coalgebraic cover modality.

Contribution

It introduces necessary and sufficient conditions for functorial relation liftings in enriched categories, extending classical set-based results to more general settings.

Findings

Derived conditions for relation liftings in enriched categories

Generalized classical results for set functors

Applied to predicate liftings and coalgebraic modalities in metric spaces

Abstract

We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the "powerset monad" on categories, one is the preservation by T of "exactness" of certain squares. Both characterisations are generalisations of the "classical" results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks. The results presented in this paper enable us to compute predicate liftings of endofunctors of, for example, generalised (ultra)metric spaces. We illustrate this by studying the coalgebraic cover modality in this setting.