Coinductive Predicates and Final Sequences in a Fibration

Coinductive predicates express persisting “safety” specifications of transition systems. Previous observations by Hermida and Jacobs identify coinductive predicates as suitable final coalgebras in a fibration—a categorical abstraction of predicate logic. In this paper we follow the spirit of a seminal work by Worrell and study final sequences in a fibration. Our main contribution is to identify some categorical “size restriction” axioms that guarantee stabilization of final sequences after ω steps. In its course we develop a relevant categorical infrastructure that relates fibrations and locally presentable categories, a combination that does not seem to be studied a lot. The genericity of our fibrational framework can be exploited for: binary relations (i.e. the logic of “binary predicates”) for which a coinductive predicate is bisimilarity; constructive logics (where interests are growing in coinductive predicates); and logics for name-passing processes.