Liftings of endofunctors on sets to endofunctors on relations are commonly used to capture bisimulation of coalgebras. Lax versions have been used in those cases where strict lifting fails to capture bisimilarity, as well as in modeling other notions of simulation. This paper provides tools for defining and manipulating lax liftings. As a central result, we define a notion of a lax distributive law of a functor over the powerset monad, and show that there is an isomorphism between the lattice of lax liftings and the lattice of lax distributive laws. We also study two functors in detail: (i) we show that the lifting for monotone bisimilarity is the minimal lifting for the monotone neighbourhood functor, and (ii) we show that the lattice of liftings for the (ordinary) neighbourhood functor is isomorphic to P(4), the powerset of a 4-element set.
翻译:集合上自函子到关系上自函子的提升常被用于捕获余代数的互模拟。在严格提升无法捕获互拟似性的情形,以及模拟其他模拟概念时,已使用了Lax版本。本文提供了定义和操作lax提升的工具。作为核心结果,我们定义了函子在幂集幺半群上的lax分配律概念,并证明了lax提升格与lax分配律格之间存在同构。我们还详细研究了两个函子:(i) 证明了单调互拟似性的提升是单调邻域函子的最小提升;(ii) 证明了(普通)邻域函子的提升格与P(4)(即4元集幂集)同构。