# Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 32 references that are in the map.
- First posted on arXiv 11 May 2021.

## Builds on (most cited first, 5 of 5)

- [Categorical Liveness Checking by Corecursive Algebras](https://mlsanity.com/paper/1704.04872/) (2017)
- [Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs](https://mlsanity.com/paper/1805.10749/) (2018)
- [Up-To Techniques for Behavioural Metrics via Fibrations](https://mlsanity.com/paper/1806.11064/) (2018)
- [Reflecting Algebraically Compact Functors](https://mlsanity.com/paper/1906.09649/) (2019)
- [Codensity Games for Bisimilarity](https://mlsanity.com/paper/1907.09634/) (2019)

## Abstract (arXiv)

The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata.