Companions, Causality and Codensity

TL;DR

This paper explores the concept of the companion in coinduction within universal coalgebra, linking it to the codensity monad and causality, and demonstrating its applications in defining causal functions and proof techniques.

Contribution

It introduces a new characterization of the final distributive law as a codensity monad and connects it to causality, enhancing coinductive proof methods.

Findings

Final distributive law is a monad and equals the codensity monad of the final sequence.

On sets, causal functions are characterized via distributive laws and GSOS specifications.

Causal functions enable valid up-to-context coinductive proof techniques.

Abstract

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.