A Point-free Perspective on Lax extensions and Predicate liftings

TL;DR

This paper explores the relationship between lax extensions of set functors and predicate liftings using quantale-enriched relations, revealing that all lax extensions can be derived from predicate liftings with simplified proofs.

Contribution

It introduces a novel point-free perspective connecting lax extensions and predicate liftings, demonstrating that every lax extension is induced by a class of predicate liftings.

Findings

Lax extensions are naturally connected to predicate liftings.

Elementary proofs are achieved through the quantale-enriched relations perspective.

Every lax extension can be induced by a class of predicate liftings.

Abstract

Lax extensions of set functors play a key role in various areas including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is induced by a class of predicate liftings; we discuss several implications of this result.