The metric closure powerspace construction

Abstract

In this paper we develop a natural powerobject construction in the context of enriched categories, a context which generalizes the traditional order-theoretic and metric space contexts. This powerobject construction is a subobject transformer involving the dialectical flow of closed subobjects of enriched categories. It is defined via factorization of a comprehension schema over metrical predicates, followed by the fibrational inverse image of metrical predicates along character, the left adjoint in the comprehension schema. A fundamental continuity property of this metrical powerobject construction vis-a-vis greatest fixpoints is established by showing that it preserves the limit of any Cauchy ωop-diagram. Using this powerobject construction we unify two well-known fixpoint semantics for concurrent interacting processes.