Behavioural distances of transition systems modelled as coalgebras for endofunctors generalize the 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 Kantorovich lifting of a functor on 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. These results are essential ingredients for adopting 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 conclude by illustrating the results of our paper in two case studies.

翻译：行为距离将转移系统的传统行为等价概念推广到定量设置中，在该设置中状态被赋予一种度量其（不）相似程度的方法。为转移系统赋予此类距离本质上依赖于将描述转移系统单步行为的函子提升至伪度量空间范畴的能力。我们考虑基于quantale值关系的函子的Kantorovich提升，该提升涵盖了等价关系、预序关系及（有向）度量。我们利用纤维范畴理论中的工具，将Kantorovich提升视为由适当的纤维伴随所产生。我们的主要贡献在于Kantorovich提升的复合性结果，证明了复合函子的提升与提升的复合相一致。此外，我们描述了当两个函子之一为多项式函子时如何提升分配律。这些结果是将up-to技术应用于quantale值行为距离的关键要素。Up-to技术是一种成熟的余归纳方法，用于高效证明行为距离的下界。最后，我们通过两个案例研究展示了本文的结果。