  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.
