Coinductive Predicates as Final Coalgebras

We show that coinductive predicates expressing behavioural properties of infinite objects can be themselves expressed as final coalgebras in a category of relations. The well-known case of bisimulation will simply be a special case of such final predicates. We will show how some useful pointwise and mixed properties of streams can be modelled in this way.