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

DOI10.2168/LMCS-9(4:8)2013zbMATH Open1287.18008arXiv1307.4682OpenAlexW2027667533MaRDI QIDQ2856480FDOQ2856480

Authors: Marta Bílková, Daniela Petrişan, Jiří Velebil, Alexander Kurz 

Publication date: 29 October 2013

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1307.4682

Recommendations

• Many-valued relation lifting and Moss' coalgebraic logic
• Relation lifting, a survey
• Relation liftings on preorders and posets
• Lax extensions of coalgebra functors and their logic
• Algebra and Coalgebra in Computer Science

zbMATH Keywords

coalgebramodal logicenriched categoriesrelation liftingmodulecover modalitycommutative quantaleexact square

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Categorical logic, topoi (03G30) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Enriched categories (over closed or monoidal categories) (18D20) Quantales (06F07)

Cited In (15)

• Title not available (Why is that?)
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• A quantified coalgebraic van Benthem theorem
• Many-valued coalgebraic logic over semi-primal varieties
• Relation lifting, a survey
• Stone duality for relations
• Lambek-Grishin calculus: focusing, display and full polarization
• Relation liftings on preorders and posets
• Generalised powerlocales via relation lifting
• Lax extensions of coalgebra functors and their logic
• Predicate liftings versus nabla modalities
• Predicate and relation lifting for parametric algebraic specifications
• Extending set functors to generalised metric spaces
• Transporting many-valued sets along many-valued relations
• Many-valued relation lifting and Moss' coalgebraic logic

This page was built for publication: Relation lifting, with an application to the many-valued cover modality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2856480)