Internal Completeness of Categories of Domains Paul Taylor 1985

This paper was presented at Category Theory and Computer Programming bf 1, University of Surrey (Guildford), September 1985. It was published in Springer-Verlag Lecture Notes in Computer Science 240 (1986) 449–465.

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 of programming languages. These are Retr(Λ), whose objects are the retracts of a combinatory model of the λ-calculus, and bcCont_{ω}, 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 bcCont_{ω} 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 bcCont_{ω} 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 closure, 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?].

1. Indexed Families

We begin by formalising the notion of an indexed family of objects. For basic category theory see [Arbib and Manes 1975], [Mitchell 1965] or [Mac Lane 1971]. This account of indexed categories is very loosely based on [Johnstone et al. 1978] and [Johnstone 1983]. [Kock and Reyes 1977] and [Lawvere 1969] provide excellent introductions to some of the underlying ideas of categorical logic.

Let S be some category, whose objects we are thinking of as sets — in the first instance S = Set. In order to talk about products, coproducts and so on in S we need some notion of an A-indexed family of objects of S, for each A ∈ obS. A naive notation for such a thing might be (X_{a} : a ∈ A). Between these there are A-indexed functions, (f_{a} : X_{a} → Y_{a} : a ∈ A), so that we have a category S^{A}. In the basic example this category is simply the A-fold power of the category S = Set.

As well as A-indexed families, we have substitution or relabelling functors. If α : B → A is any S-map and X_{a} : a ∈ A) is an A-indexed family, we have a B-indexed family (X_{αb} : b ∈ B). The same applies to morphisms, so this is in fact a functor S^{α} : S^{A} → S^{B}. The assignment α ↦ S^{α} is itself (pseudo) (contra) functorial, in that S^{id} ≅ id and S^{αβ} ≅ S^{β}S^{α}. These natural isomorphisms will have to satisfy some coherence conditions, but we shall not pay too much attention to them.

(X_{a} : a ∈ A) appears to be a function from A to the class of all sets, which is a very troublesome notion. As has been remarked, we shall be able to think in this way in Retr(Λ), but not in Set. The trick in Set is to code this up using the disjoint union, making use of our a priori knowledge of the structure of the category but quietly subsuming the Axiom of Replacement. The indexed set (X_{a} : a ∈ A) is represented by its disjoint union together with the display map which identifies the index:

\begin{matrix}X = ∐_{a∈A} X_{a} & x ∈ X_{a} \\ A & & a & \end{matrix}

An object of S^{A} is therefore just a function, or S-morphism; X_{a} is picked out as the inverse image of a, i.e. the pullback of the singleton function a : 1 → A against the display map. In the case S = Set any map may occur as a display map.

The substitution functor S^{α} : S^{A} → A^{B} over α : B → A is easily seen to be given by pullback along α and is consequently written Pα or α^{∗}:

[figure: ∐_{b∈B} X_{αb} ≅ X ×_{A} B; X ≅ ∐_{a∈A} X_{a}; B; α; A]

There is an alternative description of this set-up in terms of fibrations. The objects over A ∈ S are the S-maps with codomain A, but besides forming categories over each A (called fibres) all the objects together form a category called S^{2} because it is the category of functors from 2 = (• → •) to S; the morphisms are just the commutative squares in S. There is then a functor cod : S^{2} → S with the property that X ∈ S^{A} iff cod(X) = A and the maps X → Y over α : B → A (i.e. the squares whose lower side is α) correspond bijectively to the maps X → PαY in S^{B}. The maps within a single fibre (i.e. the squares with an identity along the bottom) are (for obvious reasons) called vertical whilst those which give pullback squares are called horizontal or cartesian.

The fibred (as opposed to indexed) approach was pioneered by Bénabou [1975] in recognition of the fact that substitution is in practice defined only up to isomorphism.

The fibre over A is in this case may be seen as either the A-fold power of S or as the slice category S/A whose objects are the S-morphisms with codomain A and whose morphisms are the S-morphisms making the triangles commute. In the relative case the objects of the slice will be display maps but the morphisms will still be arbitrary maps.

There is, however, nothing in the definition of a general fibration to require the fibre over an arbitrary A to be the A-fold power of that over the terminal object of S. Indeed the difference is quite crucial to this and many other applications. We shall denote the fibre over A by PA and the substitution functor over α : B → A by Pα.

Let us conclude this introduction by considering the form of (binary) products in the fibre categories. Let X and Y be objects over A, presented either as A-indexed things or as displays (S-morphisms with codomain A), and write X ×_{A} Y for their product according to either interpretation. Naively this is (X_{a} × Y_{a} : a ∈ A), but as a display it turns out to be precisely the pullback, hence the alternative name fibre product for the latter. In English we may therefore say “fibre products are pullbacks”, although the (Gaullist) French can’t make the a priori distinction! Fibred equalisers can also be described quite straightforwardly.

2. Indexed Products

In this section we shall look at products in Set from the “indexed family” point of view and justify the Lawvere [1969] dictum that quantification is adjoint to substitution. This gives us a notion of “internal product” applicable to bcCont_{ω} and Retr(Λ).

Given an B-indexed family of sets, (X_{b} : b ∈ B), their product has elements the indexed families (x_{b} : b ∈ B) where (∀b)(x_{b} ∈ X_{b}). This is a B-indexed family of choices of elements, which is the same as specifying a B-indexed family of maps from the (constant) singleton to the X_{b}, i.e. a map 1_{B} → X from the terminal object in the fibre over B. Now the display map of the terminal object over B is precisely (as an S-morphism) the identity on B (which to some extent excuses the ambiguous notation 1_{B}) so this is just a section or splitting of the display map.

Write ∏_{B} X for the product set, and think of it as an object of the fibre over the terminal object (i.e. of the category of single sets). It has elements 1_{1} → ∏_{B} X, and these are to correspond to the maps 1_{B} → X over B. Now 1_{B} is the pullback of 1_{1} against the terminal projection α =!_{B} : B → 1, i.e. its image under the substitution functor Pα. Thus ∏_{B} is the right adjoint of Pα:

1_{B}  ≅ Pα1_{1} →  X over B
1_{1}  → ∏_{B} X over 1

Now let us do this indexedly. So given ((X_{b} : b ∈ B_{a}) : a ∈ A), an A-indexed family of B_{a}-indexed families of objects, we need to show how to construct the ath product, (∏_{b∈B_{a}} : a ∈ A), and present it as a member of an A-indexed family.

To do this we begin by displaying the B_{a}’s over A, i.e. we construct a morphism α : B → A, where B = ∐ B_{a}; then we present the objects ((X_{b} : b ∈ B_{a}) : a ∈ A) as a B-indexed family (X_{b} : b ∈ B). The elements of the member (ΠαX)_{a} = ∏_{b∈B_{a}} X_{b} of the product are maps to 1 → (ΠαX)_{a} which are to correspond to indexed families (1 → X_{b} : b ∈ B_{a}) and so the maps 1_{B} → ΠαX over A correspond to those 1_{B} → X over B. In other words Πα (or α_{∗} is the right adjoint to the substitution or pullback Pα (or α^{∗}).

1_{B} ≅ Pα1_{A}  \overline{}X  overB
1_{A}  \overline{}ΠαX ≅  ( ∏_{b∈B_{a}} X_{b} : a ∈ A)  overA

Definition An internal product in an indexed category is a right adjoint to substitution over a display map.

The are no conceptual difficulties in doing this for Set: collections of maps may be understood naively, and any morphism in the base category S occurs as a display map. This is not so in bcCont_{ω} or Retr(Λ): we have to make our indexing “continuous”, and not every map occurs as a display map (though we have yet to define them).

Likewise the collections of maps (cones) in the definition of product have to be “continuously varying”. Whilst clearly Retr(Λ) and bcCont_{ω}, being (very) small, do not have all products externally, they still “think” they have them in this sense. Where the “continuously varying” is taken to mean computable or definable we have the appropriate restriction on the definitions to make them appropriate to programming or intuitionistic type theory.

Let us consider the corresponding notion to product for Natural Deduction, which is universal quantification. In order to prove (∀b)Y (b) from X, where the bound variable is of type B and there are no free variables, it is necessary and sufficient to prove Y (b) from the same hypotheses (in which the variable b does not occur freely). This rule corresponds formally to the natural bijection

X  ⇒  Y (b)  over  B
X  ⇒ (∀b)(Y (b)) over  1

(in which, as is usual, we have written in invisible ink above the line the substitution functor which gives X an invisible free variable) which says that (∀b) is right adjoint to the substitution.

If we had allowed Y to have other free variables besides b, we should have been performing the same argument indexedly over the type(s) of these other free variables, and the relevant substitution functors would have been over product projections in the base category. Now a product projection is the display of a constant family; in the case of a general display map α : B → A the quantifier becomes (at a) (∀b)(αb = a ⇒ ...).

There is a mild technicality in this called the Beck condition. We want to be sure that substitution and quantification interact properly, in the sense that if Pα is the introduction of a variable b and Πβ the quantification over c (where α : B × A → A and β : C × A → A) we have Pα(ΠβY) = Πβ(PαY). More generally, if the left-hand figure is a pullback in the base category then the right-hand square must commute (at least up to isomorphism):

[figure: C ×_{A} B; γ; C; B; δ; α; A; β] P(C ×_{A} B) \overline{\begin{matrix}Πγ \\  \end{matrix}}PC

[figure: PB; Pδ; Πα; PA; Pβ]

Seely [1983] has given a detailed discussion of the meaning of the Beck condition. Since our interest is in certain concrete examples (where it holds automatically) rather than the abstract formulation, we shall pay little attention to it.

Now let us consider this adjoint to substitution in the context of the fibration cod : S^{2} → S, in which the substitution functors are pullbacks. Take first the case of the terminal projection α : B → 1; pulling X → 1 back along this yields simply the product X × B, so Pα = (−) × B. The right adjoint to this is quite familiar and is written (−)^{B}:

X × B →  Y over B
X  → Y^{B} over 1

Thus S (qua indexed category cod : S^{2} → S) has global products iff it (qua category) has exponentials. We have deliberately avoided the discussion in terms of fibrations, but more generally,

Proposition The fibration cod : S^{2} → S is complete (has all indexed limits) iff S is locally cartesian closed.

This at first struck me as somewhat remarkable, but of course it is because of the idea (which there is a tendency to push to the back of one’s mind as too childish) that powers are iterated products.

In fact the above result is really a definition of local cartesian closure since we haven’t yet formally given one.

3. Indexed Coproducts

The case for sums is very similar, although we are not allowed to argue in terms of elements any more. The corresponding deduction rule for the existential quantifier is formally the same as the definition of left adjoint to substitution For the cod fibration the following easily-overlooked triviality is appropriate:

Proposition For an S-morphism α : B → A, the pullback functor Pα : S/A → S/B along α has a left adjoint Σα (or α_{!}) given by postcomposition with α.

Definition An internal coproduct or sum in an indexed category is a left adjoint to substitution over a display map.

Proposition The fibration cod : S^{2} → S is cocomplete iff S has all finite (limits and) colimits.

Starting from the indexed approach we now have a direct route to the display map: recall that this was originally given as a disjoint union. Let X be an A-indexed family (object of the fibre over A). It has a terminal projection X → 1_{A} in this fibre, and the image of this under the sum functor is of course ∑_{A} X → ∑_{A}1_{A} over 1; but ∑_{A} 1_{A} is (isomorphic to) A (in the canonical identification of S with the fibre over 1).

Proposition In the fibration cod : S^{2} → S, the fibre over the terminal object is equivalent to S and the display X → A corresponds to the map ∑_{A} X → ∑_{A} 1_{A} in this fibre.

This is the method by which we shall identify displays of retracts.

The analogue of coproducts or sums in natural deduction is existential quantification; the reader is invited to demonstrate that this is indeed left adjoint to substitution. The ordinary case (∃c)(ϕ) arises as before from a product projection C × A → A; for a general morphism α : B → A in the base category we have the idiom (∃b)(αb = a ∧ ϕ). We also need a Beck condition, but those for Σ and Π (or ∃ and ∀) are equivalent (so long as they both exist) because a diagram of left adjoints commutes up to isomorphism iff the corresponding diagram of right adjoints does so.

4. Local Cartesian Closure

So far we have been using the term “locally cartesian closed” to mean having right adjoints to pullback functors, without giving any explanation of what it has to do with “ordinary” cartesian closure in the sense of having exponentials. In this section we shall rectify this omission.

Recall that for an object Y in the fibre over A in cod : S^{2} → S, the product with Y in this fibre, and substitution from the fibre over A to that over Y, are both given by pullback along the display map Y → A.

Lemma The object Y in the fibre over A of cod : S^{2} → S is exponentiable iff pullback along Y → A has a right adjoint; moreover in this case exponentiation by Y is preserved by any pullback.

Proof Let β : Y → A be the display of Y and Πβ be the right adjoint to the pullback Pβ; then

X ×_{A} Y →  Z  over A
X ×_{A} Y ≅ PβX → PβZ ≅ Y ×_{A} Z over Y
X  → Πβ(PβZ) ≅ Z_{A}^{Y} over A

Conversely suppose (−)_{A}^{Y} is right adjoint to − ×_{A} Y in the fibre over A and let W be over Y. Then

X ×_{A} Y  ≅  PβX  →  W  over  Y
X ×_{A} Y → W ×_{A} Y  over  A
X  → (W ×_{A} Y)_{A}^{Y} ≅  ΠβW  over  A

By preservation we mean that Pα(Z_{A}^{Y}) ≅ (PαZ)_{B}^{(PαY)} for any map α : B → A.

U  → Pα(Z_{A}^{Y}) ≅ Z_{A}^{Y} ×_{A} B over  B
U  →  Z_{A}^{Y}  over  A
U ×_{A} Y →  Z  over  A
U ×_{A} Y  ≅ PαY ×_{B} U →  PαZ  over  B
U  → (PαZ)_{B}^{(PαY)}  over  B

The particularly alert reader will have noticed in following this an implicit use of the Beck condition, which is essentially equivalent to the preservation of exponentials, but is of course a theorem in this case.

Proposition The fibres of cod : S^{2} → S are cartesian closed and substitution preserves arbitrary limits and exponentials iff S is locally cartesian closed. In this case substitution also preserves any colimits which exist.

It is essential here to include the condition that exponentials be preserved, since otherwise we have a strictly weaker notion.

5. Local Smallness and other Internal Notions

The word “local” is used in the context of (indexed) category theory with reference to the fibres or slices S/A. This is a generalisation of the fact that for the open set lattice of a topological space (considered as a poset and hence a category), the slice over (i.e. open subsets of) an open set gives (the open set lattice of) the corresponding open subspace. A local notion in category theory is therefore one which is preserved by pullbacks, so that it happens in the fibres (slices) and is preserved by substitution.

We can use these methods to formulate definitions and constructions internally (say in a locally cartesian closed category). This usually takes the form of finding a generic construction, of which any other is obtained by substitution (pullback), preferably uniquely.

We shall illustrate this by formulating the idea of a category having small hom-sets or being locally small. Since cartesian closure is concerned with exponentials, i.e. sets of functions, it will not come as a surprise that these are equivalent. We can formulate local smallness as having a generic morphism, i.e. one from which any other may be obtained by substitution (pullback).

Thus if Y ∈ PB and X ∈ PA with α : B → A, by a generic morphism from Y to X over α we mean a diagram of the form

Y′  \overline{}Y

[figure]

[figure: Pα′X′; PαX]
[figure]
X′  \overline{}X

[figure: B′; B]
[figure]
[figure: A′; A]

in which the squares are pullbacks, which is generic in the sense that any other diagram of the same shape (but with ′′ for ′ ) is obtained by pulling back this one by a unique A′′ → A′.

Proposition S is locally small iff it is locally cartesian closed.

Proof Suppose Y is exponentiable in its fibre. Put B′ = (PαX)_{B}^{Y} and A′ = A ×_{B} B′. Then

Y′′  →  X′′  over  α′′
Y ×_{B} B′′  ≅  Y′′  → Pα′′X′′  ≅ PαX ×_{B} B′′ over  B′′
B′′ ×_{B} Y →  PαX  over  B
B′′  → (PαX)_{B}^{Y} =_{def}  B′  over  B

and it’s not difficult to see that the correspondence is obtained by pullback.

Conversely if B′ is generic then

B′′ ×_{B} Y →  X  over B
B′′ ×_{B} Y → B′′ ×_{B} X  over B′′
B′′ → B′ =_{def} X_{B}^{Y} over B

The same approach gives a notion of a generic subobject. A category with finite limits and generic subobjects is called an elementary topos. Unfortunately, although bcCont_{ω} does have something which might serve as an objectof-subobjects, the display of a generic subobject is (not surprisingly) a mono, whilst the displays in Retr(Λ) and bcCont are all epi because of global habitation. Consequently we shall not discuss these ideas.

Finally we might ask for a generic family of objects, i.e. a display map of which any other is a pullback. The codomain of this would be a “type of types”, each type occurring as the inverse image of an element of it. From any family of objects (display map G → V) we may construct the full subcategory whose objects are in the family; its object set is V and its morphism set G_{V ×V}^{G} over V × V. The inverse image of ⟨X, Y ⟩ ∈ V × V is just Y^{X} = hom_{S}(X, Y).

However it may be shown that if a locally cartesian closed category has a generic family then it has both a generic subobject, {true} ⊂ Ω, (making it a topos) and a “universal set”, G, (of which any other, in particular its own powerset Ω^{G}, is a subobject). Cantor’s theorem shows that this is impossible. But if we drop the requirement for equalisers we find the paradox disappears, and indeed more or less any category of domains has this property.

6. The Category of Retracts of a Combinatory Model

We now introduce the first of our two categories of domains, which may be constructed from any combinatory model of the λ-calculus, Λ. For a comprehensive account see [Barendregt 1981] or [Curry and Feys 1958].

A combinatory model is a set Λ with a binary operation (application) and constants K, S satisfying Kab = a, Sabc = ac(bc) and five other equations originally formulated by Curry. We adopt the usual convention for omitting brackets, so abc means (ab)c. This enables us to interpret λ-terms in Λ by the scheme

[λx.x] = SKK
[ab] = [a][b]
[λx.a] = K[a]  if x is not free in a
[λx.ab] = S[λx.a][λx.b]  otherwise

Given a combinatory model Λ, we can define a cartesian closed category Retr(Λ) in which any term is typable, called the category of retracts. I shall now use the term cartesian closed in the weak sense of having products and exponentials, not necessarily all finite limits.

The combinators I = λx.x = SKK and P = λxyz.y(xz) define a monoid M ⊂ Λ as follows. M = {f : PI(PfI) = f}, the composition is f · g = Pgf and the identity is I.

An object of Retr(Λ) is an idempotent of M, i.e. an element A ∈ Λ satisfying PAA = A. Unfortunately this operation is not itself idempotent: indeed in general there is no retract of Λ whose image is obRetr(Λ) ⊂ Λ. The morphisms α : A → B are the elements α ∈ Λ with α = PAα = PαB. The identity on A is A itself, whilst the composite of α : A → B and β : B → C is PP αβ : A → C.

Notice that we have dropped the category-theoretic convention that the various hom-sets be disjoint, so we do not have functions dom and cod; however it is a straightforward but unenlightening exercise to code these things in if they are required.

Idempotents split in Retr(Λ), so if α : A → A satisfies α^{2} = α, i.e. Pαα = α, then there is an object B and a pair of maps B \overrightarrow{←}A such that B → A → B is the identity and A → B → A is α; in fact of course both B and the two maps are represented by α. B is then both the equaliser and the coequaliser of α with the identity. Idempotents split in a category iff it has all finite filtered colimits (or limits).

Retr(Λ) is in fact the universal idempotent splitting category containing the monoid M (considered as a category with one object, identified with I ∈ Retr(Λ)). So if M → D is a functor to a category in which idempotents split then there is a unique (up to unique isomorphism) functor Retr(Λ) → D making the triangle commute. This means that if M is the (external) endomorphism monoid of an object in a category in which idempotents split (as they will if the category has all finite limits) then Retr(Λ) is embedded “concretely” as the category of retracts of the object.

Retr(Λ) has a terminal object T = K⊥, where we choose ⊥ = (λx.xx)(λx.xx) = (SII)(SII), and this also denotes the terminal projection, the unique map A → T. If Λ is a model (Koymans [1984]) then T is in fact a generator, i.e. if α, β : A\overrightarrow{→}B are two maps whose composites with all maps T → A are equal then α = β.

The type A can be interpreted as the set ∥A∥ = {a : a = Aa} ⊂ Λ and the map α : A → B as the function a → αa. The type T has a unique set-theoretic element, viz. ⊥ ∈ ∥T∥, so we may think of T as the one-element set. An arrow T → A is called a global (category-theoretic) element of A. The set-theoretic and category-theoretic elements of A now correspond using K and ⊥ (“dropping a variable”): given a ∈ ∥A∥ we have KaT → A, and given α : T → A we have α⊥ ∈ ∥A∥.

That T is a generator for Retr(Λ) means exactly that functions are extensional, i.e. they are equal iff they have the same effect on elements. Finally every type A has at least one element, A⊥ ∈ ∥A∥. This is the property of global habitation which is an important feature of these models. The representation of A by ∥A∥ makes Retr(Λ) into a concrete category, i.e. ∥ − ∥ : Retr(Λ)) → Set is faithful.

For an arbitrary a ∈ Λ, we call Aa a reduced to A; many constructions are of the form of general or untyped constructions reduced to appropriate types.

We shall construct finite products and exponentials in Retr(Λ), and show that its objects have internal fixpoints. It is a consequence of this that Retr(Λ) cannot have binary coproducts or all finite limits.

We now have to choose pairing and unpairing combinators ⟨⟩ = λxyz.zxy, 0 = λxy.x = K and 1 = λxy.y = KI, so that ⟨⟩ab0 = a and ⟨⟩ab1 = b for all a, b ∈ Λ. Write ⟨a, b⟩, c_{0} and c_{1} for ⟨⟩ab, (c0), (c1) respectively, noting carefully the positions of the digits.

The product A × B of A and B in Retr(Λ) is λc.⟨Ac_{0}, Bc_{1}⟩, which is our abbreviation for λc.⟨⟩(A(c0))(B(c1)), with projections π_{0} = λc.Ac_{0}, π_{1} = λc.Bc_{1}, i.e. 0 and 1 reduced to (domain A×B and) codomain A or B. Given α : D → A and β : D → B, ⟨α, β⟩ = λd.⟨αd, βd⟩ is the unique map (pair) D → A × B making the two triangles commute. There is a combinator × = λAB.A × B which, when restricted to obRetr(Λ) × obRetr(Λ) → Λ, yields (idempotents representing) products. The forgetful functor ∥ − ∥ : Retr(Λ) → Set creates finite products and preserves all limits which exist in Retr(Λ).

Retr(Λ) also has function spaces, because λf.PAf and λf.PfB are commuting idempotents (assuming A = PAA and B = PBB) so that their composite, B^{A} = λf.PA(PfB) = λf.P(PAf)B, is (idempotent, i.e. ) a type. Given α : C × A → B we have the exponential transpose α̃ = λca.α⟨c, a⟩ : C → B^{A} and conversely α = λd.α̃d_{0}d_{1}; this is the ancient trick of Currying. The evaluation map ev : B^{A} × A → B is given by λd.C(d_{0}(Bd_{1}). Again there are obvious combinators doing these things. B^{A}f is called f reduced to domain A and codomain B, but one should beware that this reduction is not functorial (it does not preserve identity and composition).

Each type A ∈ obRetr(Λ) has internal fixpoints: put

Y_{A} = λf.(λx.xx)(λx.A(f(A(xx))))

Then Y_{A} : A^{A} → A makes a certain diagram commute, which says f(Y_{A}f) = Y_{A}f for all f ∈ ∥A^{A}∥. This is just the reduction of Y to A^{A} → A. Observe that the canonical fixpoint of the identity is the “bottom” element, A⊥, of the type; this is a deliberate and crucial choice.

7. Indexed Category of Retracts

The method used in the opening sections for making Setinto an indexed category over itself requires the existence of all pullbacks, which are not available in the categories which interest us. On the other hand, this pullback trick was required for Set because of the size problem with Cat, in other words we have no universal set. In Retr(Λ), the category of retracts of a combinatory model of the λ-calculus, we do have a kind of universal set, namely the model itself. In the large category bcCont there is no “global” universal set, but there is a sense in which it has “local” ones. In this section we shall construct the indexed category of retracts, then in section 9 the display maps will be identified (along with some of the indexed sums and products).

For A ∈ Retr(Λ), an A-indexed type is a (“continuous”) function X : A → Λ taking type values, i.e. X = PAX = PXΛ (although, since Λ = I, PXΛ = X is tautologous) such that P(Xa)(Xa) = Xa for all a ∈ ∥A∥. We may rewrite this as X = PAX = QXX where Q = λwxyz.xy(wyz). Thus obP(A = {X : PAX = X = QXX}.

The structure of P(A) is given in the same fashion as that of Retr(Λ), except that the combinators take an extra argument (this is only a notational complication, but it provides an ample supply of pitfalls). Again, as with our presentation of Retr(Λ), there is no information coded in to define domain, codomain and fibration, but these may be recoded as before. As before, note that Q has four variables and that Q(Q)fg)h = Qf(Qgh) and Q(Pαf)(Pαg) = Pα(Qfg).

The objects of P(A), for A ∈ obRetr(Λ), are those X ∈ Λ with X = PAX = QXX. The morphisms X → Y are those f ∈ Λ with f = PAf = QXf = QfY; these conditions say respectively that f is fibred over A and that in each fibre a ∈ A it has domain Xa and codomain Y a. The identity on X is X itself, and the composite of f : X → Y and g : Y → Z is Qfg : X → Z. Note that PA preserves the fixed points of λx.Qxx and that λf.PAf, λf.QXf and λf.QfY are commuting idempotents for A ∈ obRetr(Λ) and X, Y ∈ obP(A).

P(A) has terminal object U = K(K⊥), and this also represents the terminal projection X → U. As before we may consider (A-indexed) elements: x ∈_{A} X is a function A → Λ such that xa ∈ Xa for each a ∈ A; the type of all such indexed elements of X is the (global) product, ∏ X = λpa.Xa(p(Aa)).

The product X ×_{A} Y of X and Y over A is given by λaz.⟨Xaz_{0}, Y az_{1}⟩; the projection maps are π_{0} = λaz.Xaz_{0} and π_{1} = λaz.Y az_{1}, and if f : Z → X, g : Z → Y are two maps in PA then the pair is ⟨f, g⟩ = λaz.⟨faz, gaz⟩ : Z → X ×_{A} Y.

Because of the observation about commuting idempotents, we have fibred exponential types.

Y_{A}^{X} = λaf.P(Xa)(P(fa)(Y a)) = λaf.Q(QY f)Za = λaf.QY (QfZ)a = λafx.Y a(fa(Xax))

This is obtained by an interchange of variables from the reduction of f to a solution of f = PAf = QXf = QfY; the latter is a “global section” of the former. The evaluation map ev : Y_{A}^{X} → Y is given by λap.Y a(p_{0}(Xap_{1})) and the transpose identifies f : W ×_{A} X → Y with g : W → Y_{A}^{X} by g = λawx.fa⟨w, x⟩ and f = λap.gap_{0}p_{1}.

Now let α : B → A be any map in the base category Retr(Λ); what is the corresponding substitution functor P(α) : P(B) → P(A), and does it have adjoints? The first question has an easy answer, which gives a pleasing consonance of notation: P(α) = Pα. In the same way as the naive indexing of Set over itself performed substitution by composition, so does this.

Thus P(α)(X) is simply PαX and P(α)(f) = Pαf; moreover PαU = U, PαX ×_{A} Y = (PαX) ×_{B} (PαY) and Pα(Y_{A}^{X}) = (PαY)_{B}^{(PαX)} exactly. The product projections, pairings, evaluation maps and transposes are also preserved exactly. Because of this notational coincidence (which I hope justifies the switch of variables in the combinator P to the even the most uncompromising users of left-handed notation), P(A) and P(α) will in future be written PA and Pα respectively.

The fibration cod : Set^{2} → Set of the category of sets over itself had the property that the fibre PT over the singleton (terminal object) T was equivalent to Set itself, and the fibre PA over A was its A-indexed power. The former remains the case for indexed retracts (by dropping a variable, i.e. A ∈ Retr(Λ) corresponds to KA ∈ PT and X ∈ PT to X⊥ ∈ Retr(Λ); but not the latter.

In fact PA should be regarded as the category of continuously A-indexed types, where continuously may in suitable circumstances be interpreted as definably or computably. If A is in fact some kind of “type of types” the way is open for the interpretation of polymorphic languages, or of type expressions (not functors) of which fixpoints might be sought, i.e. the solution of recursive domain equations.

To sum up, we have a fibration p : P → Retr(Λ) (or indexed category P : Retr(Λ)^{op} → Cat) over a cartesian closed category, such that each fibre is itself cartesian closed and this structure is preserved exactly by the substitution functor. The fibre PT over the terminal object is isomorphic to Retr(Λ) itself.

8. Relatively Cartesian Closed Categories

We have now seen a category without all pullbacks ostensibly indexed over itself, and so not by the cod : S^{2} → S fibration we used for Set. We now introduce the notion of relative cartesian closure, which enables us to unify these constructions. In the next section we identify the display maps in Retr(Λ).

In the sections 2 and 4 the (well-known) connection between internal completeness and local cartesian closure was described. Throughout the account, however, it has been hinted that there is a more general construction in which not all maps map occur as display maps, and that this applies to our Retr(Λ) and bcCont. In this section this more general version will be formulated.

Recall that the slice category C/A has objects the C-morphisms with codomain A and morphisms the C-morphisms making the triangle commute. If α : B → A is a C-morphism there is a functor α_{!} : C/B → C/A given by postcomposition with α. The right adjoint to α_{!}, if it exists, is called Pα and is given by pullback along α. If Pα itself has a right adjoint, written Πα, then α is said to be exponentiable.

More generally let D be a class of C-maps the relative slice C/_{D}A has objects the D-maps with codomain A but still all C-maps as morphisms (so long as the triangle still commutes in C). Thus C/_{D}A is a full subcategory of C/A.

Definition A category C is said to be cartesian closed relative to a class of (display) maps D ⊂ C if

(i) The pullback of any D-map against any C-map exists and is in D,

(ii) The composite of any two D-maps is in D,

(iii) C has a terminal object and any terminal projection is in D, and

(iv) For α : B → A in D, pullback Pα : C/_{D}A → C/_{D}B has a right adjoint Πα.

Examples

(i) Set, or any locally cartesian closed category, is cartesian closed relative to all maps.

(ii) Any cartesian closed category is cartesian closed relative to the class of all product projections.

From these data we can construct a fibred category p : P → C, where the objects over A ∈ C are the display maps X → A with codomain A, and the morphisms over α : B → A from Y → B to X → A are the commutative squares of which three sides have already been given. The fibre PA over A is therefore C/_{D}A.

Lemma If (C, D) satisfy axiom (i) above, then this is a fibration; the fibres are relative slices and the horizontal maps are the pullback squares.

This coincides with the standard construction in the case of Set; for the minimal class of display maps the families are all “constant” ones, so this isnt very interesting.

Axiom (ii) serves a dual role: it performs mundane categorical bookkeeping, but also provides indexed sums. The purpose of axiom (iii) is that we should be able to speak of the fibration as actually being the indexed form of the original category. Henceforward (C, D) are assumed to satisfy axioms (i) to (iii).

Lemma C is canonically identified with the fibre over its terminal object.

Lemma C has finite products, and their projections (including all isomorphisms) are in D

Lemma The fibres have finite products (given by pullback) and these are preserved (up to isomorphism) by arbitrary pullback functors.

Lemma Pullback along display maps has a left adjoint (namely postcomposition with the display map). The display map in the sense constructed at the end of section 2 coincides with that defining the indexed type.

Finally axiom (iv) deals with products and exponentials, as was proved in section 4.

Lemma The fibres are cartesian closed (and this structure is preserved (up to isomorphism) by pullback functors) iff axiom (iv) holds.

Theorem A relatively cartesian closed category gives rise to an indexed category whose fibres are cartesian closed and whose substitution functors preserve this structure. It is complete and cocomplete in the sense that substitution along display maps has adjoints on both sides which satisfy the Beck condition.

Proof It remains only to show that the Beck condition holds, but this is yet another application of the definitions of pullbacks.

Having now set up the theoretical machinery for talking about internal products, sums and function spaces in categories we devote the remainder of the paper to the identification of the display maps in Retr(Λ) and bcCont, showing that these categories are relatively cartesian closed.

9. Displays of Retracts

The next objective is to identify and construct the display maps in Retr(Λ) and hence show that this has indexed products and sums. For this it will be enough to know (in the first instance) about global sums, although in fact we shall need to do the local (indexed) case implicitly in the course of the proof of the final lemma of this section; we have already done the work for the indexed products in our study of exponentials.

Recall that the substitution functor over α : B → A is written Pα and is given by precomposition with α; its adjoints (where they exist) are called Σα and Πα for reasons which were discussed in sections 2 and 3. These take values in the fibre over A. The “global” sum and product functors, which take values in C itself (but recall that this is canonically identified with PT, the fibre over the terminal object) will be written simply ∑ and ∏, so (under this identification), ∏ = ΠT = Π!_{B} in the various notations, and likewise with Σ.

Let B ∈ C and Y ∈ PB. The basic idea of ∏ Y is the set

{p : B → Λ | (∀b)(pb ∈ Y b)}

which is the set of solutions of p = PBp = SY p; these are commuting idempotents (given that B = PBB and Y = PBY = QY Y), so their composite gives the required type. Likewise ∑ Y is based on

{⟨b, y⟩ | b ∈ B ∧ yb ∈ Y b}

so the corresponding retract is λp.⟨Bp_{0}, Y p_{0}p_{1}⟩.

Instead of tryingto specify those adjoints which exist in terms of combinators, we rely on the general theorem of the previous section. Unfortunately we have lost the preservation of structure “on the nose” because of the need to choose representations for these functors; in particular the global sum and product for the terminal object (singleton family) are not identities because they include redundant coding which is residual from the structure of the indexing set. The remainder of this section concerns the properties of display maps.

Recall that the indexing of Set over itself used disjoint unions together with their indicator maps. As a result of section 3 we can describe this in terms of the global sum. If X = (X_{a} : a ∈ A) is an A-indexed set, the display map occurs as both the left and top sides of the following commutative square:

[figure: X = ∐_{a∈A} X_{a}; A; A; A]

The significance of this banal observation is that this square represents a morphism of S^{2}, specifically one over A, and the right-hand map is the terminal object of A. Composing below with the terminal projections from A, we get a morphism over the terminal object 1, which is the global sum applied to X →_{A} 1_{A}.

The same can of course be done in our case, so

Definition A display map in Retr(Λ) is the composite of an invertible followed by a map of the form π_{0} : ∑ Y → A where Y ∈ PA. π_{0} is in fact λp.Bp_{0}.

We shall take as read a number of trivial properties of pullbacks, including the fact that this definition allows invertibles to be “passed through” display maps.

Lemma The pullback of a display map exists and is a display map.

Proof Let α : B → A in C and X ∈ PA. Put Y = PαX; then the following is a pullback square:

[figure: ∑ Y = λq.⟨Bq_{0}, Y q_{0}q_{1}⟩; λq.⟨αq_{0}, Y q_{0}q_{1}⟩; ∑ X = λp.⟨Ap_{0}, Xp_{0}p_{1}⟩; B; π_{0}; α; A; π_{0}]

Given any other β : C → B and γ : C → ∑ X making the square commute, the pair is λc.⟨βc, (γc)_{1}⟩.

Lemma Any terminal projection is a display map.

Proof Given B → T, put X = KB and A = T. Then X ∈ PA and ∑ X = λp.⟨⊥, Bp_{1}⟩ ≅ B.

Lemma Any composite of display maps is a display map.

Proof Given X ∈ PA and Y ∈ PB where B = ∑ X we want to construct Z ∈ PA with ∑ Y ≅ ∑ Z over A. Put Z = λap.⟨Xap_{0}, Y ⟨a, p_{0}⟩p_{1}⟩; then i : ∑ Z → ∑ Y and j : ∑ Y → ∑ Z are mutually inverse where

i = λu.⟨⟨Au_{0}, Xu_{0}u_{10}⟩, Y ⟨u_{0}, u_{10}⟩u_{11}⟩
j = λv.⟨Av_{00}, ⟨Xv_{00}v_{01}, Y v_{0}v_{1}⟩⟩

Lemma Pullback against a display map, considered as a functor between relative slices, has a right adjoint.

Proof This is equivalent by section 4 to the fact (which we have already proved) that the fibres have exponentials which are preserved by substitution.

Theorem Retr(Λ) is cartesian closed relative to the class of display maps identified above; consequently it has internal sums, products and function spaces.

The class of display maps constructed is the largest possible in the following sense. Suppose some map α : B → A in C has a pullback against any map with the same codomain, and that this can be done internally. By this we must mean (restricting to the case of maps from the terminal object, i.e. elements of A) that there is a continuous function assigning to each a ∈ A a type X_{a} and a pair of maps forming a pullback square. Then X would itself be an A-indexed type and B ≅ ∑ X.

10. Continuous Lattices

Continuous lattices are a generalisation of algebraic lattices (which occur as lattices of subobjects in finitary algebraic theories such as groups and modules), making the notion of finiteness or compactness a relative one. They provide the answers to a number of questions in general topology relating to injectivity and exponentiability as well as “nice” behaviour in the theory of topological (semi)lattices. For an authoritative discussion see Gierz et al. [1980]. Johnstone and Joyal [1981] have given a generalisation to categories which answers the corresponding questions for toposes.

Let A be a poset with directed sups. We say a is well below b (notation a ≪ b) if whenever b ≤ ^{⋁↑}U for some (directed, which is what the arrow means) set U, there is some c ∈ U with a ≤ c. In the case of the lattice of open sets of the real line, R, this means that there is a compact set lying between a and b. Then A is called a continuous poset if b = ^{⋁↑}{a : a ≪ b} for all b ∈ A. Scott [1972] gave an argument that continuous posets are the appropriate notion of approximate computation, although most of his followers have since retreated to the algebraic condition.

There is a topology, the Scott topology, which is appropriate for A, in which the basic open sets are those of the form {↑ \atop ↑}a = \{b : a ≪ b\} (likewise we write {↓ \atop ↓}b = \{a : a ≪ b\}). Conveniently, a function f : A → B between two continuous posets is continuous w.r.t. this topology iff it preserves directed sups, whilst separate and joint continuity coincide for functions of two variables.

The previous remark gives a topology from an order: there is also a converse operation called the specialisation order on a topological space. Let x ≤ y if y lies within any open set which contains x; this relation is antisymmetric iff the space is T_{0} and discrete iff it is T_{1}. The specialisation order on a sober space has directed sups, but the converse is false [Johnstone 1982].

We say that a topological space I is injective if given any subspace inclusion A ⊂ B and a continuous map f : A → I, there is some (not necessarily unique) continuous g : B → I making the triangle commute. Likewise I is densely injective if this holds for dense subspace inclusions. An easy (but important) example of an injective space is the Sierpinski space, which has two points exactly one of which is open.

Proposition The following are equivalent for an ordered T_{0} space I:

(i) I is injective

(ii) I is a continuous lattice with the Scott topology

(iii) I is a retract of a (Tychonov) power of the Sierpinski space

(iv) I is has arbitrary infs (⋀) which distribute over directed sups (⋁^{↑})

(v) I is an algebra for the filter monad.

Pω is the first infinite example of part (iii); it carries a well-known combinatory algebra structure [Scott 1976] and Retr(Pω) ≃ ContLat_{ω}, the category of countably based continuous lattices and Scott continuous maps.

We shall have occasion to make extensive use of these characterisations. In particular, part (iv) suggests that there is another class of maps of importance between continuous lattices. These are the homomorphisms of the (⋁^{↑}, ⋀) structure, i.e. functions preserving these operations. Of course these are just continuous functions with left adjoint, so a surjective homomorphism is the same as a projection. Write CL for the algebraic category of continuous lattices and homomorphisms. Part (v), due to Day [1975], identifies the free functor Set → CL, left adjoint to the forgetful functor.

We shall need a few fragments of universal algebra for the proofs in the next section (see, for example, [Cohn 1965] or [Manes 1975]). In particular the forgetful functor CL → Set creates arbitrary limits (i.e. we calculate them at the level of Set and impose the obvious algebra structure); this means we can talk about pullbacks of continuous lattices and homomorphisms.

Secondly, a congruence on an algebra A is a reflexive, symmetric and transitive subalgebra of A × A, i.e. a subset R containing the diagonal and closed under the operations such that (a, b) ∈ R iff (b, a) ∈ R and if (a, b), (b, c) ∈ R then (a, c) ∈ R. In Set, Gp, K − Vect and Rng these are usually presented as equivalence relations, normal subgroups, subspaces and ideals, respectively. Given a congruence, we may construct the quotient, A/R, whose elements are the classes [a] = {b : (a, b) ∈ R}, together with the function A → A/R by a ↦ [a]. A/R carries a unique algebra structure making this a homomorphism.

Slightly more generally, a partial congruence is the same thing but without reflexivity, so the union of the classes may be a proper subalgebra. We can still construct A/R, but now it is a subquotient, i.e. a quotient of a subalgebra.

Finally, a poset is boundedly-complete if any bounded (but possibly empty) set has a least upper bound; equivalently any nonempty set has a greatest lower bound. We shall assume the posets to be inhabited (nonempty) and so have a least element, although this conflicts with the definition naturally provided by universal algebra. An easy generalisation of the characterisation of continuous lattices, as it turns out more appropriate to our studies, is

Proposition The following are equivalent for an inhabited T_{0} space I:

(i) I is densely injective

(ii) I is a boundedly complete continuous poset (with the Scott topology)

(iii) I is a closed subset of some continuous lattice.

11. bcCont is Relatively Cartesian Closed

In this section we shall show that bcCont, the category of inhabited boundedly complete continuous posets and Scott-continuous maps, has a nontrivial relatively cartesian closed structure, in which D is the class of projections, i.e. surjective maps with left adjoint.

In order to avoid developing a separate theory for boundedly complete continuous posets we shall add top elements where convenient (denoted by X^{⊤}) and make extensive use of the algebraic and topological characterisations of continuous lattices. We shall work in the category IPO of posets with directed sups and least element and Scottcontinuous maps.

Lemma Suppose α : B → A in bcCont has a pullback against any map f : X → A. Then α is a projection.

Proof Consider the special case of the inclusion of the element a ∈ A. By hypothesis the pullback

[figure: α^{−1}(a); ⊂; B; 1; a; A; α]

exists in bcCont, so in particular α^{−1}(a) has a least element. Write β(a) for the corresponding element of B. Then β(α(a)) = a and α(β(b)) ≤ b so β is left adjoint to α (and so preserves all sups, in particular directed ones) and α is surjective.

If we were to insist on working with (total) continuous lattices, we should have to have right as well as left adjoints in order to preserve top. Intuition seems, however, to suggest on the one hand that top is a red herring and on the other that the projections are the important class of maps.

Write −−−▷ for projections. We shall show that C = bcCont is cartesian closed relative to the class D of projections. Conditions (ii) and (iii) are trivial.

Proposition The forgetful functor CL → IPO has a left adjoint F.

Proof Recall that CL, the category of continuous lattices and homomorphisms, is algebraic and in particular there is a free algebra functor Set → CL and CL has all limits. If X ∈ IPO then we may take the continuous lattice generated by the elements of X subject to the equations that directed sups in X remain so in the continuous lattice.

Lemma Let X ∈ C. Then X is a (Scott-continuous) retract of a (Scott-) closed subset of FX.

Proof Consider the map X → X^{⊤}; then X^{⊤} ∈ CL so by the universal property of FX there is a unique homomorphism FX → X^{⊤} making the triangle commute. Let W ⊑ FX be the inverse image under this of the closed subset X ⊑ X^{⊤}.

W ^{⊂} FX

[figure]

[figure: X; ⊂; X^{⊤}]

Clearly X → FX factors through this so X is a retract of W.

Lemma A closed subset or a retract of a boundedly complete continuous poset is another such.

We now have the machinery to prove axiom (i) for relative cartesian closure.

Proposition Pullbacks of D maps against C maps exist and are in D.

Proof Let α : B → A in D and f : X → A in C; let β : A → B be the left adjoint to α. There is no difficulty in constructing the pullback X ×_{A} B in IPO ; it consists of the pairs (x, b) ∈ X × B with fx = αb and by the continuity of f and α this equation respects directed sups. Moreover it has a least element (⊥_{X}, β(f⊥_{X})) and the left adjoint to the projection onto X takes x to (x, β(fx)). The problem is to show that X ×_{A} B is continuous.

By the universal property of FX and the fact that A^{⊤} ∈ CL, there is a unique homomorphism FX → A^{⊤} making the base of the following pentagonal prism commute; the top of the prism is given by pulling back along B^{⊤} → A^{⊤}. The aim is to show successively that FX ×_{A^{⊤}} B^{⊤}, W ×_{A^{⊤}} B^{⊤} and X ×_{A^{⊤}} B^{⊤} ≅ X ×_{A} B are continuous.

B ^{⊂} B^{⊤}
[figure]
[figure: X ×_{A} B ≅ X ×_{A^{⊤}} B^{⊤}; ⊂; W ×_{A^{⊤}} B^{⊤}; ⊂; FX ×_{A^{⊤}} B^{⊤}]

A^{▽}  \overline{}A^{⊤}^{▽}
[figure]
[figure: X; ▽; ⊂; W; ▽; ⊂; FX; ▽]

The right-hand square forms a pullback in CL because the bottom and right-hand maps are homomorphisms. Next we have the inverse image of the closed set W ⊑ FX under a continuous map, so by the lemma this is continuous. Finally the required pullback is the fixed-point set of the image under the pullback functor of the retract of W which gives X.

Finally we prove axiom (iv).

Lemma Let A and B be continuous lattices and [A → B] the poset of Scott-continuous functions from A to B with the pointwise order (arising from that on B). Then [A → B] is a continuous lattice in which ⋁^{↑} and ⋀ are evaluated pointwise.

Proposition Let α : B → A in D. The pullback functor α^{∗} : C_{D}A → C/_{D}B has a right adjoint, (−)_{A}^{B}.

Proof Let ξ : X → B in D. Working in Set and then in IPO , X_{A}^{B} has to be

{(a, f : α^{−1}(a) → X) | (∀b.αb = a)(ξ(fb) = b)}

Indeed for υ : Y → A in D we have a bijection

\begin{aligned}Y ×_{A} B & →_{B} & X & (y, b) & ↦ & g(y, b) \\ Y & →_{A} & X_{A}^{B} & y & ↦ & (υy, g(y, −)) \end{aligned}

which preserves directed sups and is natural in X and Y. The bottom element of X_{A}^{B} is (⊥_{A}, ζ|_{α^{−1}(⊥)}) where ζ : B → X is the left adjoint to ξ. Once again, the problem is in showing that this is a continuous poset.

Again it is convenient to move to continuous lattices, but this time in order to make use of the injectivity. Then any continuous map α^{−1}(a) → X can be extended to one B^{⊤} → X^{⊤}, and we can recover the information we want by identifying functions which agree on α^{−1}(a).

[figure: α^{−1}(a); ⊂; B^{⊤}; X; ⊂; X^{⊤}]

Let U be the continuous lattice A^{⊤} × [B^{⊤} → X^{⊤}] and R ⊂ U × U be the subset

{(a_{1}, f_{1}, a_{2}, f_{2}) : a_{1} = a_{2} ≠ ⊤ ∧ (∀b.αb = a_{1})(f_{1}b = a_{2}b ∧ ξ(f_{1}b) = b)}

This is symmetric, transitive and closed under directed sup and nonempty inf, i.e. it is a partial congruence of (^{⋁↑}, ⋀^{≠∅}-algebras. Thus the subquotient U/R which consists of the equivalence classes under R (which do not exhaust U) carries a (^{⋁↑}, ⋀^{≠∅}-algebra, i.e. boundedly-complete continuous poset, structure.

But this is isomorphic as a poset to the required X_{A}^{B} which is therefore in C as required.

Theorem bcCont is cartesian closed relative to the projections, and is therefore fibred over itself so that each fibre is cartesian closed, this structure is preserved up to isomorphism by pullback against arbitrary maps, and pullback against projections has adjoints on both sides.

This theorem is true in rather greater generality. We have implicitly proved it for IPO already (just delete the “difficult” bits), but inclusion of categories is not the same as specialisation of proof. To demonstrate it for, say, retracts of Plotkin’s “SFP” objects, requires more conceptual technology.

The intuition behind this result is that a display of domains is given by a “patchwork” of components (each of which has a least element). In order for the component posets to be “continuously indexed” it is sufficient that the composite be itself continuous (qua domain). In fact these display maps are themselves fibrations of domains, as will be shown in [Taylor 1986?].

By way of a corollary, “raised sums” of domains (in which we take the disjoint union of two domains and add a new bottom element) are seen as a special case of indexed sums in which the indexing domain is ⋁-shaped and the ⊥-component is the singleton.

Acknowledgements

I should like to acknowledge the help and advice of Martin Hyland (without whom this paper would never have been thought of, let alone written) and my supervisor Peter Johnstone. I have been supported financially by the Science and Engineering Research Council, by Trinity College and by DPMMS. Finally I should also like to thank David Rydeheard, David Pitt and the other organisers of the Category Theory and Computer Programming workshop for providing this opportunity for the two disciplines to exchange ideas.

Bibliography Arbib, M.A. and Manes, E.G., Arrows, Structures and Functors — the Categorical Imperative, Academic Press, 1975 Barendregt, H., The Lambda Calculus — its Syntax and Semantics, North-Holland, 1981 Bénabou, J., Fibrations Pétites et Localement Pétites, Comptes Rendues Acad. Sci. Math., Paris, 281 (1975) 831–834 and 897–900 Cohn, P.M., Universal Algebra, Harper and Row, 1965 Curry, H.B. and Feys, R., Combinatory Logic I, North-Holland, 1958 Day, A., Filter Monads, Continuous Lattices and Closure Systems, Canad. J. Math., 27 (1975) 50–59 Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M. and Scott, D.S., A Compendium of Continuous Lattices, Springer, 1980 Hyland, J.M.E., Function Spaces in the Category of Locales, Continuous Lattices, (Ed. Banuschewski, B. and Hoffman, R.-E.), Springer LNM, 871 (1981) 264–281 Hyland, J.M.E., The Effective Topos, L.E.J. Brouwer Centenary Symposium, (Ed. Troelstra, A.S. and van Dalen, D.), North-Holland, (1982) 165–216 Johnstone, P.T., Paré, R., Roseburgh, R.D., Schumacher, D., Wood, R.D. and Wraith, G.C., Indexed Categories and their Applications, Springer, 1978 Johnstone, P.T., Hyland, J.M.E. and Pitts, A.M., Tripos Theory, Math. Proc. Camb. Philos. Soc., 88 (1980) 205–232 Johnstone, P.T., Scott is not always sober, Continuous Lattices, (Ed. Banuschewski, B. and Hoffman, R.-E.), Springer LNM, 871 (1981) 282–283 Johnstone, P.T. and Joyal, A., Continuous Categories and Exponentiable Toposes, J. Pure Appl. Alg., 25 (1982) 255–296 Johnstone, P.T., Fibred Categories, Part III Lecture Course, Cambridge, Michaelmas 1983 Johnstone, P.T., Stone Spaces, CUP, 1983 Kock, A. and Reyes, G.E., Doctrines in Categorical Logic, Handbook of Mathematical Logic, (Ed. Barwise, J.), North-Holland Studies in Logic and the Foundations of Mathematics, 90 (1977) 283–313 Koymans, C.P.J., Models of the Lambda Calculus, Centrum voor Wiskunde en Informatica, Amsterdam, 9 (1984) Lawvere, F.W., Adjointness in Foundations, Dialectica, 23 (1969) 281–296 Manes, E.G., Algebraic Theories, Springer Graduate Texts in Mathematics, 26 (1975) Mac Lane, S., Categories for the Working Mathematician, Springer, 1971 Mitchell, B., Theory of Categories, Academic Press, 1965 Pitts, A.M., The Theory of Triposes, Ph.D. dissertation, Cambridge, 1981 Scott, D.S., Data Types as Lattices, SIAM J. Comp., 5 (1976) 522–587 Seely, R.A.G., Natural Deduction and the Beck Condition, Zeitschr. Math. Logik und Grundlagen d. Math., 29 (1983) 505–542 Taylor, P., Ph.D. dissertation, Cambridge, 1986 (I hope!)