一句话：把共归纳 companion 提升到 universal coalgebra，证明 final distributive law 是 codensity monad，并用因果性刻画 up-to 技术。
论文研究抽象共归纳证明原理的增强技术。在完备格中，最大相容函数（companion）可统一多数 up-to 技术；本文将其提升到 universal coalgebra，对应概念为 final distributive law。作者证明：当 final distributive law 存在时它是一个 monad，并与给定函子的 final sequence 的 codensity monad 重合。在集合范畴上，他们引入一种抽象的因果性概念来刻画该 codensity monad。由此可恢复经典结果：在流上，由 distributive law 或 GSOS 规约定义的函数恰为因果函数。最后回到共归纳证明，证明任意因果函数都能产生有效的 up-to-context 技术。
In the context of abstract coinduction in complete lattices, the notion of compatible function makes it possible to introduce enhancements of the coinduction proof principle. The largest compatible function, called the companion, subsumes most enhancements and has been proved to enjoy many good properties. Here we move to universal coalgebra, where the corresponding notion is that of a final distributive law. We show that when it exists, the final distributive law is a monad, and that it coincides with the codensity monad of the final sequence of the given functor. On sets, we moreover characterise this codensity monad using a new abstract notion of causality. In particular, we recover the fact that on streams, the functions definable by a distributive law or GSOS specification are precisely the causal functions. Going back to enhancements of the coinductive proof principle, we finally obtain that any causal function gives rise to a valid up-to-context technique.