A point-free perspective on lax extensions and predicate liftings

DOI10.1017/S096012952300035XarXiv2112.12681MaRDI QIDQ6149965

Dirk Hofmann, Paul Wild, Pedro Nora, Lutz Schröder, Sergei S. Goncharov

Publication date: 5 March 2024

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Abstract: In this paper we have a fresh look at the connection between lax extensions and predicate liftings of a functor from the point of view of quantale-enriched relations. Using this perspective, in particular we show that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is represented by a class of predicate liftings and discuss several implications of this result.

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

zbMATH Keywords

lax extensioncoalgebraic modal logicKantorovich extensionMoss lifting

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An introduction to quantaloid-enriched categories
• Relation lifting, a survey
• Expressive logics for coalgebras via terminal sequence induction
• Simulations in coalgebra
• Lawvere completion and separation via closure
• Quantales and continuity spaces
• Taut monads and \(T0\)-spaces.
• A quantified coalgebraic van Benthem theorem
• On finitary functors and their presentations
• Lax extensions of coalgebra functors and their logic
• Expressivity of coalgebraic modal logic: the limits and beyond
• Equational Coalgebraic Logic
• Predicate Liftings Versus Nabla Modalities
• Monoidal Topology
• Presentation of Set Functors: A Coalgebraic Perspective
• Rank-1 Modal Logics are Coalgebraic
• Metric spaces, generalized logic, and closed categories
• (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• On Finitary Functors
• Algebra and Coalgebra in Computer Science

This page was built for publication: A point-free perspective on lax extensions and predicate liftings