Marta Bilkova ; Alexander Kurz ; Daniela Petrisan ; Jiri Velebil - Relation lifting, with an application to the many-valued cover modality

lmcs:742 - Logical Methods in Computer Science, October 25, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:8)2013
Relation lifting, with an application to the many-valued cover modalityArticle

Authors: Marta Bilkova ORCID; Alexander Kurz ORCID; Daniela Petrisan ; Jiri Velebil

    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.


    Volume: Volume 9, Issue 4
    Published on: October 25, 2013
    Imported on: March 7, 2012
    Keywords: Computer Science - Logic in Computer Science

    7 Documents citing this article

    Consultation statistics

    This page has been seen 1088 times.
    This article's PDF has been downloaded 490 times.