Continuous endofunctors F of locally finitely presentable categories carry a natural metric on their final coalgebra. Whenever F(0) has an element, this metric is proved to be a Cauchy completion of the initial algebra of F. This is illustrated on the poset of real numbers represented as a final coalgebra of an endofunctor of Pos by Pavlovic' and Pratt. Under additional assumptions on the locally finitely presentable category, all finitary endofunctors are proved to have a final coalgebra constructed in w + co steps of the natural iteration construction.
展开▼
