A structural co-induction theorem

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.