A Categorical Powerdomain Construction

The class of countably based bifinites (SFP objects) is the usual mathematical framework for carrying out the constructions that arise in the semantics of programming languages. However, A. Jung showed that the construction used to define the domain-theoretic semantics of polymorphic lambda calculus, is not closed on this category. This motivates the search for a suitable category that is closed under all the constructions used in programming language semantics. T. Coquand developed categories of embeddings as a categorical generalization of the domain-theoretic structures used to give semantics of polymorphism. In this paper, we present a category- theoretic powerdomain construction that is closed on the (extensional) categories of embeddings. The construction is shown to have universal properties that resemble the universal properties of the Plotkin powerdomain