Internal completeness of categories of domains

Abstract

One of the objectives of category theory is to provide a foundation for itself in particular and mathematics in general which is independent of the traditional use of set theory. A major question in this programme is how to formulate the fact that Set is “complete”, i.e. it has all “small” (i.e. set- rather than class-indexed) limits (and colimits). The answer to this depends upon first being able to express the notion of a “family” of sets, and indexed category theory was developed for this purpose.

This paper sets out some of the basic ideas of indexed category theory, motivated in the first instance by this problem. Our aim, however, is the application of these techniques to two categories of “domains” for data types in the semantics ofprogramming languages. These Retr(Λ), whose objects are the retracts of a combinatory model of the λ-calculus, and beCont_ω, which consists of countably-based boundedly-complete continuous posets. They are (approximately) related by Scott's [1976] Pω model. In the case of Set we would like to be able to define an indexed family of sets as a function from the indexing set to the “set” of all sets. Of course Russell showed long ago that we cannot have this. However there is a trick with disjoint unions and pullbacks which enables us to perform an equivalent construction called a fibration.

Retr(Λ) and beCont_ω do not have all pullbacks. This of course means that they're not strictly speaking complete however we formulate smallness: what we aim to show is that they have all “small” products. More importantly, this pullback trick is on the face of it not available to us. They do, on the other hand, have a notion of “universal” set (of which any other is a retract), and indeed of a “set” of sets, though space forbids discussion of this. These we use in stead to provide the indexation.

Having constructed the indexed form of Retr(Λ) we discover that it does after all have enough pullbacks to present it as a fibration in the same way as Set. However whereas in Set any map may occur as a display map, in this case we have only a restricted class of them. We then identify this class for beContω and find that it consists of the projections (continuous surjections with left adjoint) already known to be of importance in the solution of recursive domain equations.

We formulate the abstract notion of a class of display maps and define relative cartesian closure with respect to it. The maximal case of this (as applies in Set, where all maps are displays, is known as local cartesian closure. The minimal case (where only product projections are displays) is known in computer science as (ordinary) cartesian clsoure, though in category theory it is now more common to use this term only when all pullbacks exist, though not necessarily as displays.

This work will be substantially amplified (including discussion of the “type of types”) in [Taylor 1986?].