# Up-To Techniques for Behavioural Metrics via Fibrations

arXiv: https://arxiv.org/abs/1806.11064 · HTML: https://mlsanity.com/paper/1806.11064/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Jun 2018.

## Built on by (most cited first, 2 of 2)

- [Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down](https://mlsanity.com/paper/2105.04817/) (2021)
- [Foundations of Stochastic Lexical Calculus: Semantic Descent and Random Dynamics on Probability Simplices](https://mlsanity.com/paper/2609.20207/) (2026)

## Abstract (arXiv)

Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their oundness in a compositional way. In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.