Coinduction for recursive data types: Partial orders, metric spaces and Ω-categories

In this paper we prove coinduction theorems for final coalgebras of endofunctors on categories of partial orders and (generalized) metric spaces. These results characterize the order, respectively the metric, on a final coalgebra as maximum amongst all simulations. As suggested in [15], and motivate...