The Structural Induction Theorem (Lehmann and Smyth, 1981; Plotkin, 1981) characterizes initial F-algebras of locally continuous functors F on the category of cpo’s with strict and continuous maps. Here a dual of that theorem is presented, giving a number of equivalent characterizations of final coalgebras of such functors. In particular, final coalgebras are order strongly-extensional (sometimes called internal full abstractness): the order is the union of all (ordered) F-bisimulations. (Since the initial fixed point for locally continuous functors is also final, both theorems apply.) Further, a similar co-induction theorem is given for a category of complete metric spaces and locally contracting functors.

International Conference on Mathematical Foundations of Programming Semantics
Centrum Wiskunde & Informatica, Amsterdam, The Netherlands

Rutten, J.J.M.M. (1994). A structural co-induction theorem. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 83–102).