Behavioural distances of transition systems modelled via coalgebras for endofunctors generalize traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition systems to the category of pseudometric spaces. We consider the category theoretic generalization of the Kantorovich lifting from transportation theory to the case of lifting functors to quantale-valued relations, which subsumes equivalences, preorders and (directed) metrics. We use tools from fibred category theory, which allow one to see the Kantorovich lifting as arising from an appropriate fibred adjunction. Our main contributions are compositionality results for the Kantorovich lifting, where we show that that the lifting of a composed functor coincides with the composition of the liftings. In addition, we describe how to lift distributive laws in the case where one of the two functors is polynomial (with finite coproducts). These results are essential ingredients for adapting up-to-techniques to the case of quantale-valued behavioural distances. Up-to techniques are a well-known coinductive technique for efficiently showing lower bounds for behavioural distances. We illustrate the results of our paper in two case studies.

翻译：通过自函子余代数建模的转移系统的行为距离，将传统的行为等价概念推广至定量场景，其中状态配备了衡量其（不）相似程度的度量。为转移系统赋予此类距离本质上依赖于将描述转移系统单步行为的函子提升至伪度量空间范畴的能力。我们考虑将运输理论中的 Kantorovich 提升范畴论地推广至将函子提升为量值化关系的情形，该推广涵盖了等价关系、预序关系及（有向）度量。我们使用纤维范畴论的工具，使得 Kantorovich 提升可被视为源于一个恰当的纤维伴随关系。我们的主要贡献在于 Kantorovich 提升的组合性结果，我们证明了复合函子的提升与各提升的复合相一致。此外，我们描述了当两个函子之一为多项式函子（具有有限余积）时，如何提升分配律。这些结果是使 up-to 技术适应于量值化行为距离情况的关键要素。Up-to 技术是一种著名的共归纳技术，用于高效地证明行为距离的下界。我们通过两个案例研究展示了本文的结果。