一句话：提出在代数与余代数层面使用 codensity 提升，给出分配律可提升的充分条件，统一证明各类状态系统上行为等价的组合性。
论文研究状态系统上行为等价相对于代数运算的组合性证明。已有范畴方法把运算建模为函子间分配律，并需证明该分配律从集合提升到关系。本文聚焦 codensity 提升，将其同时用于代数与余代数层面，并给出 codensity 提升的新推广；由此把分配律提升问题化为构造 codensity 提升间分配律，并提出简化充分条件。该条件可实例化为多种状态系统上运算组合性的具体证明方法。作者验证确定性自动机的定性与定量性质，并讨论概率系统实例；还提出组合式 codensity 博弈变体，可组合获胜位置不变量。
Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical formulation of this problem, where operations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws between functors. To prove compositionality, it then suffices to show that this distributive law lifts from sets to relations, giving an explanation of how behavioral equivalence on smaller systems can be combined to obtain behavioral equivalence on the composed system. In this paper, we refine this approach by focusing on so-called codensity lifting of functors, which gives a very generic presentation of various notions of (bi)similarity as well as quantitative notions such as behavioral metrics on probabilistic systems. The key idea is to use codensity liftings both at the level of algebras and coalgebras, using a new generalization of the codensity lifting. The problem of lifting distributive laws then reduces to the abstract problem of constructing distributive laws between codensity liftings, for which we propose a simplified sufficient condition. Our sufficient condition instantiates to concrete proof methods for compositionality of algebraic operations on various types of state-based systems. We instantiate our results to prove compositionality of qualitative and quantitative properties of deterministic automata. We also explore the limits of our approach by including an example of probabilistic systems, where it is unclear whether the sufficient condition holds, and instead we use our setting to give a direct proof of compositionality. In addition, we propose a compositional variant of Komorida et al.'s codensity games for bisimilarities. A novel feature of this variant is that it can also compose game invariants, which are subsets of winning positions. Under our sufficient condition of the liftability of distributive laws, composed games give an alternative proof of the preservation of bisimilarities under the composition.