Corecursion Up-to via Causal Transformations.

Up-to techniques are a widely used family of enhancements of corecursion and coinduction. The soundness of these techniques can be shown systematically through the use of distributive laws. In this paper we propose instead to present up-to techniques as causal transformations, which are a certain type of natural transformations over the final sequence of a functor. These generalise the approach to proving soundness via distributive laws, and inherit their good compositionality properties. We show how causal transformations give rise to valid up-to techniques both for corecursive definitions and coinductive proofs.