MFPS X111 (1997) 17 pages

The category of cpos from a synthetic viewpoint

Marcelo Fiore^{1}

LFCS, University of Edinburgh The King’s Buildings Edinburgh EH9 3JZ, Scotland

Giuseppe Rosolini^{2}

Dipartimento di Matematica via Dodecaneso 35 16146 Genova, Italy

Abstract We provide an internal characterization of the category ω-Cpo of ω-complete posets and ω-continuous functions within the model H of SDT recently introduced by the authors. It follows that ω-cpos lie between the two extreme synthetic notions of domain given by repleteness and well-completeness.

Introduction

Synthetic Domain Theory aims at giving a few simple axioms to be added to an intuitionistic set theory in order to obtain domain-like sets. The idea at the core of the study was proposed by Dana Scott in the late 70’s: domains should be certain “sets” in a mathematical universe where domain theory would be available; in particular, domains would come with intrinsic notions of approximation and passage to the limit with respect to which all functions will be continuous. Various suggestions for the notion of domain (typically within a set-theoretic universe given by a topos [18]) appeared in the literature, e.g. in [12,26,10,24,21,17]. All these notions enjoy the properties needed in denotational semantics, e.g. closure under sums, products, and exponentials, the admission of fixed-point operators, and the solution of recursive domain equations. However, it is not clear whether some choice is preferable to others, mostly because of lack of distinguishing examples.

1 Research supported by EPSRC grant GR/J84205, Frameworks for Programming Language Semantics and Logic. 2 Research supported by MURST 40%.

This is a preliminary version. The final version can be accessed at

            URL: http://www.elsevier.nl/locate/entcs/volume5.html

Fiore and Rosolini

In a recent paper the authors introduced two Grothendieck toposes, H and H_{2}, and studied them as models of SDT; see [8]. Each model respectively embeds the following standard categories of domains: the category of ω-complete posets and ω-continuous functions, and the category of ω-complete posets with ω-continuous pullbacks (= ω-continuous bounded binary meets) and ω-stable (= ω-continuous and pullback preserving) functions.

In each topos it was possible to check that the replete objects [12,26] were included among the embedded domains; thus showing that the synthetic theory encompasses some of the traditional models used in denotational semantics. In this paper we characterize the embedding of the category of ω-cpos in the model H, and use it to compare the notions of repleteness and wellcompleteness which are two extreme synthetic notions of domain respectively suggested in [12,26] and [16,17].

The paper is organized as follows. First, we recall some category-theoretic background material and some internal notions in a topos. Then, we recall some facts of Synthetic Domain Theory, and the presentations of the topos H. Finally, we characterize the embedding of the category of ω-cpos, and compare it with the replete objects and the well-complete ones.

1 Basic concepts

The internal logic of a topos explains the intuition to follow when working within a topos: it is like working with sets, provided that one does so intuitionistically, see [18]. Everything in this section about objects and structures can be understood as about sets, but most of the notions would reduce to trivialities in the case of standard sets. It is in different toposes that they give rise to interesting structures.

Lifting monad Let C be a category with finite limits. A monad L = (L, η, μ) internalizing possibly non-terminating computations is usually named lifting and it is axiomatized by requiring that the unit η classifies (certain) partial maps that are closed under composition; see e.g. [22,4]. Precisely, the conditions are that the naturality diagrams for the unit η are pullbacks (= the natural transformation η is cartesian), and, in the situation

\begin{aligned}1 & \underline{←} & D & \overline{→} & B \\ L1 & ^{η_{1}↓ ∨} & \underline{←} & A, & ^{↓ ∨} \end{aligned}

there exists a unique classifying map A → LB such that the diagram

\begin{aligned}D & \overline{→} & B \\ A & ^{↓ ∨} & \overline{→} & LB & \begin{matrix}↓ & ∨ \\ η_{B} \end{matrix} \end{aligned} ; (1)

2 is a pullback.

Monos obtained as pullbacks of η_{1} (as, for example, D ^{>} → A above) are called admissible and are denoted with ^{⊂} → .

Examples of lifting monads on a topos are: the monad classifying total maps (i.e. the identity monad), the monad classifying partial maps defined on a decidable subobject (i.e. the monad on 1 + ( )), and the monad classifying all partial maps; see e.g. [15].

An example that will illustrate at an elementary level what will follow is given by (an extension of) the bottom-adding monad ( )_{⊥} —that classifies partial maps defined on upper-closed subsets— on Pos, the category of posets and monotone functions. Consider the topos of simplicial sets Δ̂, i.e. the topos of presheaves on the category Δ of monotone functions between the finite nonempty ordinals; see [18]. The category Pos embeds fully into Δ̂ via the nerve functor N mapping a poset P to the simplicial set N (P) = Pos(J , P), where J: Δ^{⊂} → Pos is the inclusion functor.

For a simplicial set A, define LA at the ordinal \underline{n} as

L(A)(\underline{n}) = 1 + ∐_{1≤m≤n}A(\underline{m}).

Then the natural transformation η_{A}: A → LA which, at the ordinal \underline{n}, injects A(\underline{n}) into (LA)(\underline{n}) is a partial map classifier yielding a lifting monad. The monad L on Δ̂ extends the monad ( )_{⊥} on Pos: for a poset P, there is a canonical isomorphism N (P_{⊥}) ≅ L (N (P)).

Orthogonality The crucial property of a model of Synthetic Domain Theory is stated in terms of orthogonality. This is a very useful notion that appeared in relation with factorization systems and limit-preserving functors. Recall from [9] that, in a category C, an object A is said to be orthogonal to a map D → C whenever, for every map D → A, there exists a unique map C → A such that (D → C → A) = (D → A). If C is cartesian closed, an object A is internally orthogonal to a map f: D → C if the arrow A^{f}: A^{C} → A^{D} is iso. Internal orthogonality corresponds to a parameterised version of orthogonality.

Proposition 1.1 In a cartesian closed category C, the following are equivalent:

(i) A is internally orthogonal to a map f: D → C. (ii) A is orthogonal to f × id_{X}: D × X → C × X, for every X.

If C is a (pre)topos, another equivalent condition is

(iii) C ^{∥−} ∀δ ∈ A^{D}. ∃!γ ∈ A^{C}. δ = γ ∘ f.

Path relation and path-transitivity Consider a topos with a lifting monad L on it such that its underlying functor L has a global element (i.e. a natural transformation from the functor constantly valued 1 into L) ⊥: 1 → L for which 1 ^{⊥_{1}}→ L1 ←^{η_{1}} 1 are disjoint—recall that a mono m: M ^{>} → A is disjoint from a mono n: N ^{>} → A if the diagram

\begin{aligned}0 & ^{>} → & M \\ N & ^{↓ ∨} & ^{>} n→ & A & \begin{matrix}↓ & ∨ \\ m \end{matrix} \end{aligned}

where 0 denotes the initial object, is a pullback. We shall write ⊥ for the map ⊥_{1}: 1 → L1 and ⊤ for the map η_{1}: 1 → L1.

For n ≥ 0, set Σ_{n} = L^{n}1 (omitting the index in the case n = 1), and let 2 =^{def} 1 + 1 and d =^{def} [⊥, ⊤]: 2 → Σ. For an object A, define the path relation p_{A} ^{>} → A × A as the image of the map A^{d}: A^{Σ} → A^{2} ≅ A × A. Consider the following notion, used implicitly in [5,6]: an object is path-transitive when it is internally orthogonal to the unique mediating map t in

1 \overline{⊥ →} Σ
[figure: η_{Σ}]
Σ \begin{matrix}⊤ \\ ↓ \end{matrix} \overline{→} Σ ∨ Σ ↓
[figure: L⊥]^{...}t_{...}_{}
Σ_{2}.

The name is justified by the fact that when an object is path-transitive, the path relation on it is transitive.

In the topos of simplicial sets, Σ_{n} is (isomorphic to the image under the nerve functor N of) the ordinal \underline{n}. For a poset P, the path relation on N (P) is (isomorphic to) N (O_{P}), where O_{P} is the poset on {(x, y) ∈ P^{2} | x ≤_{P} y} with the pointwise order; moreover, N (P) is path-transitive.

As follows from the proposition below, in all examples of interest Σ ∨ Σ is not path-transitive.

Proposition 1.2 The following are equivalent:

(i) Σ ∨ Σ is path-transitive.

(ii) The diagram \begin{matrix}1 & \overline{⊥→} & Σ \\ Σ & \begin{matrix}⊤ \\ ↓ \end{matrix} & \overline{_{L⊥→}} & Σ_{2} & ^{↓η_{Σ}} \end{matrix} is a pushout.

(iii) Every object is path-transitive.

(iv) 1 ^{⊥}→ Σ ←^{⊤} 1 is a coproduct diagram.

Double-negation topology The double-negation topology is a Lawvere-Tierney topology j: Ω → Ω on a topos defined in terms of the internal negation, see [18]. It may also be described as follows. A mono m: S ^{>} → A is ¬¬-closed if every mono m′: S′ ^{>} → A, disjoint from all those monos which are in turn disjoint from m, factors through m. In other words, consider the collection of those monos disjoint from m, then m is the largest mono disjoint from all these.

Given a topology j, the internal definition of the j-closure m′: S′ ^{>} → A of m: S ^{>} → A is given in terms of the classifying maps into Ω: if χ: A → Ω classifies m, then j ∘ χ: A → Ω classifies m′. Once the notion of closure is available, one can introduce the notion of density: a mono is j-dense if its j-closure is the identity.

Sheaves for a topology j are those objects which are orthogonal to all j-dense monomorphisms. An object A is said to be j-separated if for every j-dense mono D ^{>} → C and every map D → A there exists at most one map D → A such that (D ^{>} → C → A) = (D → A). Equivalently, j-separated objects are those A for which the diagonal mono δ_{A}: A^{>} → A×A is ¬¬-closed.

Basic properties about the above notions, and about the ¬¬-topology in particular, are stated in the following two propositions; see [3,18] for the proofs.

Proposition 1.3 (i) An object is j-separated if and only if the reflection

into its associated j-sheaf is monic. (ii) A mono m: X ^{>} → A is j-dense if and only if the associated j-sheaf

functor turns it into an isomorphism.

We write Ĉ for the topos of presheaves on a small category C, and Y_{C} for the Yoneda embedding C^{⊂} → Ĉ. Further, we let γ: Ĉ → Set be the global-sections functor Ĉ(1, ) and we define γ_{∗}: Set → Ĉ by γ_{∗}(S) = Set(γY_{C}( ), S).

Proposition 1.4 Let C be a small category with a terminal object.

(i) The functor γ_{∗} is right adjoint to the global-sections functor γ. The induced geometric morphism γ ^{−|} γ_{∗}: Set → Ĉ is an inclusion which defines the topos of ¬¬-sheaves on Ĉ.

(ii) Assume C is given a topology J such that γY_{C}: C → Set maps covers in J to epimorphic families in Set. Then γ_{∗} factors through sh(C, J)^{⊂} → Ĉ. Moreover, if covers in J are non-empty then the topos defined by the geometric morphism γ ^{−|} γ_{∗}: Set → sh(C, J) is that of ¬¬-sheaves.

So, in the cases of Proposition 1.4, we have an explicit description of the associated sheaf functor with respect to the double-negation topology as the composite γ_{∗} ∘ γ. The reflector is the composite

{A(C) ≅ Ĉ(Y_{C}(C), A) ^{γ}→ Set(γY_{C}(C), γ(A)). \atop (2)}

Moreover, by Proposition 1.3(i), we know that an object A is ¬¬-separated precisely when the maps in the family (2) are 1-1; see Corollary 3.2 below. A similar remark applies to density.

2 Notions of domain in SDT

A model of Synthetic Domain Theory is a topos equipped with a chosen object Σ, whose rôle is to determine the “computational properties” of other objects in the topos, and with a lifting monad L = (L, μ, η) which provides the notion of “computation”. In all the studied models, the computational properties are the possible computations at the terminal object; i.e. Σ = L1. Henceforth we will restrict attention to this situation.

The intuition is that the universe topos incorporates some sort of internal computational power and, as a consequence, all functions between domainlike objects are intrinsically continuous. In the literature there are at least four related suggestions for selecting the objects in the topos which are to be thought of as domains; see [10,12,13,16,17,23,24,26]. They all concentrate on abstracting peculiar properties of Σ: they range from asking as many as possible (repleteness) to as few as acceptable (well-completeness). In all the various cases, it is made sure, one way or the other, that the chosen domains are closed under the action of the monad of computations. We refer the reader to the cited literature and [25] for more on the subject of SDT. Here we recall some of the basic definitions and the facts we need in the paper.

The underlying functor L of a lifting monad always has an initial algebra and a final coalgebra, call these ι: LI → I and φ: F → LF respectively. By a lemma noticed by Lambek, ι and φ are isomorphisms. Let c: I → F be the canonical map determined by inverting one of the two and recalling universality of the other; that is, unique making the following diagram commute

\begin{matrix}LI & \overline{\underrightarrow{Lc}} & LF \\ I & \begin{matrix}ι \\ ↓ \end{matrix} & \overline{_{c→}} & F. & ↑ ; φ \end{matrix}

The main infinitary axiom of a model of SDT is that Σ thinks that the initial L-algebra and the final L-colgebra coincide. By this we mean the Completeness Axiom of [16,17]: Σ is internally orthogonal to c, that is,

Σ^{c}: Σ^{F} → Σ^{I} is iso.

We shall refer to a topos with a lifting monad in which the completeness axiom holds as a model of SDT . In models of SDT, various intrinsic notions of “domain” are available; we review two of them below.

Well-completeness Recall from [16,17] that an object A is complete if it is internally orthogonal to c; it is well-complete if LA is complete. As in a model of SDT the terminal object is well-complete, we have the following proposition, cf. [17,7].

Proposition 2.1 (i) Well-complete objects are closed under lifting, (ii) a well-complete object is complete, (iii) an object is well-complete if and only if it is orthogonal to all pullbacks

of c × id: I × X → F × X along an admissible mono.

Proof. (i) One sees that the composite

LLA ^{⟨μ_{A},L!⟩} → LA × L1 ^{t_{A,1}} → L(LA × 1) ≅ LLA

is the identity by pulling back η_{LA}. This produces LLA as a retract of a product of two complete objects. Hence LLA is also complete; see [25].

(ii) We show that the commutative diagram

\begin{matrix}A^{F} & \overline{A^{c} →} & A^{I} \\ (LA)^{F} & ^{η^{F}↓} & \overline{_{(LA)^{c} →}} & (LA)^{I} & ^{↓η^{I}} \end{matrix}

is a pullback. Hence, if the bottom arrow is iso then so is the top one. Indeed, consider a span (LA)^{F} ←^{a} X ^{b}→ A^{I}. Using the classifying property of η one sees that the condition of commutativity η^{I} ∘ b = (LA)^{c} ∘ a translates as the commutativity of the following diagram

\begin{matrix}I × X & \overline{b̂ →} & A \\ I × X & ‖ & \overline{_{c × id →}} & F × X & \overline{_{â→}} & LA & \begin{matrix}↓ & ∩ \\ η \end{matrix} \end{matrix}

where ˆ( ) denotes the exponential transpose. We are interested in determining the partial map represented by â; the one determined by â ∘ (c × id) is b̂: I × X → A defined on id_{I×X}. The fact that L1 is complete means that there is a bijective correspondence between monos classified by L1 on I × X and those on F × X given by pulling back. Hence the only mono classified by L1 which pulls back to the identity on I × X is the identity on F × X. Thus the diagram

I × X \overline{\underrightarrow{c × id}} F × X \overline{x̂→} A

I × X^{id↓ ∩}  \overline{_{c × id →}} F × X^{id↓ ∩}  \overline{_{â→}} LA \begin{matrix}↓ & ∩ \\ η \end{matrix}

commutes for a unique x: X → A^{F} which is what we wanted.

(iii) By Proposition 1.1 and (1), one has only to check that there is a bijective correspondence between commutative triangles into LA and commutative triangles on pullbacks along an admissible mono as follows

[figure: I × X; F × X \begin{matrix}c × id \\ ↓ \end{matrix}  \overline{→} LA; I × X ←  ^{⊃} U  \overline{→} A; F × X \begin{matrix}c × id \\ ↓ \end{matrix} ←  ^{⊃} C ↓]

This follows again from the completeness of L1. □

Repleteness The definition of repleteness fits into a general scheme to produce reflective subcategories; see [9,13,1]. In a model of SDT, an object is replete [12,26] (with respect to Σ) if it is orthogonal to all those maps f: X → Y such that Σ^{f}: Σ^{Y} → Σ^{X} is an iso. Roughly speaking, the replete objects are those objects which are completely recoverable from their Σ-definable properties.

Also replete objects are closed under lifting (see [12]) and hence, by the completeness axiom, are well-complete.

3 Domains in the model H of SDT

Two models of SDT have been recently introduced in [8]; the model H was shown to embed the category ω-Cpo of ω-complete posets and ω-continuous functions.

The model H The model H of SDT is the topos of sheaves for the canonical topology on the category F of continuous functions between finite products of \overline{ω} (the countable chain with a top). Though this is a complete definition, it is useful to give some more intuitions about it.

The canonical topology on F can be described as those non-empty families R on an object in F such that:

(i) for every pair of elements x ≤ y there is a function f ∈ R such that x, y ∈ im(f),

(ii) for each infinite chain there is a function f ∈ R such that im(f) contains a final subchain of the infinite chain.

There is a wide collection of sites of definition for H.

Theorem 3.1 Let G be a dense generating set in ω-Cpo, and write G for the full subcategory of ω-Cpo determined by G. Then H is equivalent to the topos of sheaves on G for the canonical topology.

It follows that other sites of definition for H are the monoid L of continuous endofunctions of \overline{ω} endowed with its canonical topology and those obtained by splitting the idempotents of L and F: the first splitting S(L) gives the category of ω-continuous functions between \overline{ω} and the finite non-empty chains, see [8] for details.

The different sites of definition for H give us various presentations of the sheaves which are useful: for example, give succint definitions (in the case of L), or grasp the intrinsic structure of the sheaves (in the case of S(F)).

Cpos The category F is a small dense generator in ω-Cpo. This allows us to define a “Yoneda embedding” from ω-Cpo into the topos of presheaves F̂, which results in a full embedding Y: ω-Cpo^{⊂} → H. The embedding Y maps an ω-cpo D to the sheaf of \overline{ω}-continuous paths Y(D) defined as ω-Cpo(J , D), where J denotes the inclusion of F into ω-Cpo. The (closure under isomorphisms of the) image of the embedding Y produces a reflective exponential ideal of H. Again consult [8] for details. We shall refrain from writing Y when this causes no confusion.

Many of the investigations to follow maybe carried out in the topos of presheaves on any small dense generator in ω-Cpo, rather than in H. However, the topos H provides a more accurate view of ω-Cpo. Indeed, the embedding Y: ω-Cpo^{⊂} → H preserves limits and also, as follows from Theorem 3.1, stable colimits. In particular, it preserves coproducts, and so the discretely ordered natural numbers ℕ in ω-Cpo becomes the natural number object N of the topos H.

Double-negation topology It is important to notice that Y(D) is defined in terms of functions into a fixed set, and that the action of the arrows is given by composition on the right presenting the category ω-Cpo in a general form already considered in [3]. In fact, as a consequence of Proposition 1.3 and (2), we can derive the descriptions of ¬¬-separation and ¬¬-density in H (although we shall not use them in this form).

Corollary 3.2 (i) A sheaf A in H is ¬¬-separated if and only if, for all

f, g: \overline{ω} → A, if fx = gx for all x: 1 → \overline{ω} then f = g. (ii) For every ω-cpo D and mono S ^{>} → D in H, S ^{>} → D is ¬¬-dense if

and only if ⋃_{f∈S(\overline{ω})} im(f) = D.

The lifting monad The model H admits a lifting monad L extending that of ω-Cpo and Δ̂. For a sheaf A in H, the sheaf LA (considered as defined on L) has underlying set 1 + ∐_{m≥1} A(\underline{m}).

The following diagram, where U: H → Δ̂ is the forgetful functor induced by the full embedding Δ^{⊂} → S(L), summarises the relationship between the various lifting monads introduced so far.

ω-Cpo^{⊂}  Y  → H
[figure: ( )_{⊥}; L; γ]
ω-Cpo^{⊂}  Y  → H
[figure: γ]

Pos ↓ ^{⊂}  N  → Δ̂^{↓U}  \overline{_{γ  →}} Set
[figure: ( )_{⊥}; L; 1 + ( )]
Pos ↓ ^{⊂}  N  → Δ̂^{↓U}  \overline{_{γ  →}} Set

The final L-coalgebra and the initial L-algebra The cone

\begin{aligned}1 & ← ! & Σ & \underline{←} & ⋯ & \underline{←} & Σ_{n+1} & ← L^{n}! & ⋯ \\ & & & ⋯ & & & ⋯ \\ \overline{ω} & ^{L!↑} & \overline{\underrightarrow{≅}} & L\overline{ω} & ^{L!↑} & \overline{→} & ⋯ & \overline{→} & L^{n}\overline{ω} & ↑ ; L^{n}! & \overline{\underrightarrow{≅}} & ⋯ \end{aligned} ; (3)

is limiting in ω-Cpo, and hence also in H. Thus, \overline{ω} ≅ L\overline{ω} is a final Lcoalgebra. The final L-coalgebra can be described as a retract of Σ^{N} (the object of admissible subsets of the natural number object N) as follows

\{p ∈ Σ^{N} | ∀n ∈ N. p_{n} ⇒ p_{n+1}\} \overleftarrow{> →} Σ^{N},

see [12].

The initial L-algebra is the smallest L-subalgebra of the (inverse of the) final L-coalgebra, see [14] for an explicit description. In our situation, since L: H → H preserves non-empty connected colimits that are computed as in L̂, the initial L-algebra LI → I is obtained from the colimit of the diagram

\begin{aligned}& 0 & \overline{! →} & 1 & \overline{\underrightarrow{L!}} & Σ & \overline{→} & ⋯ & \overline{→} & Σ_{n+1} & \overline{\underrightarrow{L^{n}!}} & ⋯ \\ (4) \end{aligned}

It follows that the canonical map c: I → \overline{ω} is the unique mediating morphism from (4) to the cone

\begin{aligned}0 & \overline{! →} & 1 & \overline{\underrightarrow{L!}} & Σ & \overline{→} & ⋯ & \overline{→} & Σ_{n+1} & \overline{\underrightarrow{L^{n}!}} & ⋯ \\ & & & & ⋯ & & & ⋯ \\ \overline{ω} & !↓ & ←≅ & L\overline{ω} & \begin{matrix}L! \\ ↓ \end{matrix} & ←≅ & L^{2}\overline{ω} & \begin{matrix}L^{2}! \\ ↓ \end{matrix} & \underline{←} & ⋯ & \underline{←} & L^{n}\overline{ω} & ^{↓L^{n}!} & ←≅ & ⋯ \end{aligned} ; (5)

Complete and well-complete objects The completeness axiom is satisfied in H because of the following general result.

Proposition 3.3 Consider a diagram Γ in ω-Cpo. For α: Γ .→ C colimiting in H and β: Γ .→ B colimiting in ω-Cpo, let f: C → B be the unique mediating morphism in H from α to β. In H, every ω-cpo is internally orthogonal to f.

Proof. The diagram D^{α}: D^{C} .→ D^{Γ} is limiting in H, and D^{β}: D^{B} .→ D^{Γ} is limiting in ω-Cpo, hence D^{β}: D^{B} .→ D^{Γ} is limiting in H. Since f mediates between α and β, it follows that D^{f} mediates between D^{β} and D^{α}; and hence it is an iso. □

It is furthermore interesting to note that in H the notions of completeness and well-completeness coincide.

Theorem 3.4 In H, complete objects are well-complete.

Proof. Since the category F is a dense generator in H (and colimits are stable under pullbacks in a topos), by Proposition 2.1(iii), an object is well-complete if and only if it is orthogonal to all pullbacks of c × id: I × \overline{ω}^{n} → \overline{ω} × \overline{ω}^{n} along an admissible mono. This result follows from the characterisation of these pullbacks obtained from the lemma below using that colimits are stable under pullbacks.

Lemma 3.5 (i) Every admissible mono U ^{⊂} → \overline{ω}^{ℓ} (ℓ ∈ ℕ) in H is a finite

colimit of admissible monos of the form \overline{ω}^{ℓ} ^{⊂} → \overline{ω}^{ℓ}. (ii) Let

\begin{matrix}V & \overline{z →} & \overline{ω} × \overline{ω}^{n} \\ I × \overline{ω}^{n} & ^{↓ ∩} & \overline{_{c × id →}} & \overline{ω} × \overline{ω}^{n} & ^{↓ ∩} \end{matrix}

be a pullback in H. Then, we have a canonical isomorphism V ≅ I × \overline{ω}^{n} such that the composite I × \overline{ω}^{n} ≅ V ^{z}→ \overline{ω} × \overline{ω}^{n} equals c × id.

Proof. (i) Admissible subsets of \overline{ω}^{ℓ} are pullbacks of ⊤: 1 → Σ. Since ω-Cpo is closed under limits in H, these can be computed in ω-Cpo. Thus an admissible subset U of \overline{ω}^{ℓ} is a Scott-open subset: the set M of its minimal points is finite and U equals ⋃_{∅≠P ⊆M}(∨∨ P)^{↑} in ω-Cpo as well as in H (because the union is stable under pullbacks). Clearly every subset p^{↑} is isomorphic to \overline{ω}^{ℓ}.

(ii) An admissible subset V of I × \overline{ω}^{n} in H is an increasing chain (V_{ℓ})_{ℓ∈ℕ} of Scott-open subsets as in the following diagram.

0 = V_{0} ^{>}  → V_{1} ^{>}  → V_{2} ^{>} → ⋯^{>} → V_{n+1} ^{>}  → ⋯

0 × \overline{ω}^{n}^{↓ ∩}  ^{>}! × id → 1 × \overline{ω}^{n}^{↓ ∩}  ^{>}L! × id → Σ × \overline{ω}^{n}^{↓ ∩}  ^{>} → ⋯^{>} → Σ_{n+1} × \overline{ω}^{n}^{↓ ∩}  ^{>}L^{n}! × id → ⋯

If V is obtained by pullback as in (ii), then it must have a least element, say it is v ∈ V_{k+1} where k is least with this property. Then, for ℓ ≤ k we have V_{ℓ} = ∅, and for ℓ > k we have V_{ℓ} = v^{↑} ^{≅}→ Σ_{ℓ−k} × \overline{ω}^{n}. Hence the claim follows. □

Cpos revisited Let C be the full subcategory of H consisting of the complete, path-transitive, ¬¬-separated sheaves.

Corollary 3.6 The embedding Y: ω-Cpo^{⊂} → H factors through C ^{⊂} → H.

Proof. To get completeness, note that the colimit of the cone (4) in ω-Cpo is \overline{ω}, and, for path-transitivity, check that the diagram

\begin{matrix}1 & \overline{⊥→} & Σ \\ Σ & \begin{matrix}⊤ \\ ↓ \end{matrix} & \overline{_{L⊥ →}} & Σ_{2} & ^{↓η_{Σ}} \end{matrix}

is a pushout in ω-Cpo.

For ¬¬-separation, for an ω-complete poset D, note that γY(D) is the set underlying D and the associated sheaf of Y(D) is Set(γY , D). Then, as Y(D)(C) consists of functions from C to D it is clear that the reflector (2) is monic. The conclusion follows by Proposition 1.3(i). □

4 Internal characterisation of ω-Cpo

We will show that the full embedding Y: ω-Cpo^{⊂} → C is an equivalence of categories.

Consider a sheaf A in C. Since it is separated, the reflector (2)

A(C) ≅ H(C, A) ^{γ}→ Set(γC, γA),

is injective. We characterize the images of those monos for the cases A(\overline{ω}×Σ_{n}).

As d: Σ → 2 is ¬¬-dense, the map A^{d}: A^{Σ} → A^{2} is monic, hence A^{Σ} is the path relation on A. Let P_{A} =^{def} (γ(A), γ(A^{Σ})). Write ⊑_{A} for the relation γ(A^{Σ}) on γ(A), and simply ⊑ if the subindex is clear. The path relation is always reflexive, and it is transitive because A is path-transitive.

So, by definition, we have a bijective correspondence

A(Σ) ≅ H(Σ, A) ≅ H(1, A^{Σ}) ≅ ⊑_{A} ≅ Preo(Σ, P_{A}).

The preorder P_{A} exhibits an intrinsic notion of approximation on the sheaf A.

We shall consider A as a sheaf defined on the splitting S(F) because it will be useful to compute its values at objects of the form Σ_{n} × Σ_{m}.

Consider the full subcategory S of S(F) determined by the objects 1 and Σ. Given C = Σ_{n} × Σ_{m}, let G: S/C → H be the first projection from the comma category: it is the diagram of all global elements and paths of C. It is clear that C ≅ colim G in H, because all maps in S(F) from Σ into a finite object C form a cover in the canonical topology. It follows that an element of A(C) is an element of Set(γC, γA) which maps paths to paths, in other words an element of Preo(C, P_{A}).

Since A is complete it follows that, for n ∈ ℕ, the following is a limiting cone in Set (cf. [8])

A(1 × Σ_{n}) \underline{←} A(Σ × Σ_{n}) \underline{←}  ⋯ \underline{←} A(Σ_{m+1} × Σ_{n}) ⋯
⋯
A(\overline{ω} × Σ_{n})^{↑ ⋯}  \overline{→} \underline{←}

Hence, A(\overline{ω} × Σ_{n}) ≅ Preo(ω × Σ_{n}, P_{A}). It is possible to prove that A(\overline{ω}^{n}) ≅ Preo(ω^{n}, P_{A}), but we will get that for free from Theorem 4.4. From now on, we identify A(C) with its image under the reflector (2)

{A(C) ≅ Preo(C, P_{A}) ⊆ Set(γC, γA), \atop (6)}

when C is one of the cases discussed above (a binary product of Σ_{n} or \overline{ω}). For instance, to describe a map \overline{ω} → A in H, or equivalently, by Yoneda, an element of A(\overline{ω}), we give a chain ⟨x_{i}⟩ in P_{A}.

We claim that A(∞): A(\overline{ω}) → A(1) yields a lub operator for ω-chains in P_{A}. Note that with the identifications just introduced,

⨆_{A}⟨x_{i}⟩ =^{def} A(∞)⟨x_{i}⟩ = ⟨x_{i}⟩ ∘ ∞. ; (7)

Proposition 4.1 ⨆_{A}⟨x_{i}⟩ is an upper bound.

Proof. For i ∈ ω, consider the path ⟨i, ∞⟩: Σ → \overline{ω}. Then,

x_{i} = ⟨x_{i}⟩ ∘ i = ⟨x_{i}⟩ ∘ ⟨i, ∞⟩ ∘ ⊥ ⊑ ⟨x_{i}⟩ ∘ ⟨i, ∞⟩ ∘ ⊤ = ⟨x_{i}⟩ ∘ ∞ = ⨆_{A}⟨x_{i}⟩.□

The operator ⨆_{A} satisfies the following properties, cf. [6].

Proposition 4.2 (Constant) For x ∈ γ(A), we have that

⨆_{A}⟨x ⊑ … ⊑ x ⊑ …⟩ = x.

(Monotonicity) If ⟨x_{i}⟩ and ⟨y_{j}⟩ are ω-chains such that x_{k} ⊑_{A} y_{k} for k ∈ ℕ,

then ⨆_{A}⟨x_{i}⟩ ⊑ ⨆_{A}⟨y_{j}⟩. (Finality) If ⟨x_{i}⟩ is an ω-chain in P_{A} and f: ω → ω is monotone and un-

bounded, then ⨆_{A}⟨x_{i}⟩ = ⨆_{A}⟨x_{f(i)}⟩.

Proof. (Constant) By (7), one has ⨆_{A}⟨x ⊑ … ⊑ x ⊑ …⟩ = ⨆_{A}x∘! = x∘! ∘ ∞ = x.

(Monotonicity) Let α be the map \overline{ω} × Σ → A defined as

⟨i, k⟩ ↦ \{ \begin{matrix}x_{i}, & if k = 0 \\ y_{i}, & if k = 1. \end{matrix}

Then

⨆_{A}⟨x_{i}⟩ = α ∘ ⟨id\overline{ω}, ⊥∘!⟩ ∘ ∞ = α ∘ ⟨∞∘!, id_{Σ}⟩ ∘ ⊥
⊑ α ∘ ⟨∞∘!, id_{Σ}⟩ ∘ ⊤ = α ∘ ⟨id\overline{ω}, ⊤∘!⟩ ∘ ∞ = ⨆_{A}⟨y_{j}⟩.

(Finality) Let \overline{f}: \overline{ω} → \overline{ω} be f extended continuously by \overline{f}(∞) = ∞. Then

⨆_{A}⟨x_{i}⟩ = ⟨x_{i}⟩ ∘ ∞ = ⟨x_{i}⟩ ∘ \overline{f} ∘ ∞ = ⨆_{A}⟨x_{f(i)}⟩. □

Proposition 4.3 ⨆_{A}⟨x_{i}⟩ is least among upper bounds.

Proof. Given an ω-chain ⟨x_{i}⟩ in P_{A} and x in γ(A) such that x_{i} ⊑ x, for all i ∈ ℕ, by (Monotonicity) and (Constant) we have that

⨆_{A}⟨x_{i}⟩ ⊑ ⨆_{A}⟨x ⊑ … ⊑ x ⊑ …⟩ = x. □

Theorem 4.4 The full embedding Y: ω-Cpo^{⊂} → C is an equivalence of categories.

Proof. As a consequence of (Finality), the relation ⊑_{A} is antisymmetric because, for x ⊑ y ⊑ x in P_{A},

\begin{aligned}x & = & ⨆_{A}⟨x ⊑ … ⊑ x ⊑ …⟩ & = & ⨆_{A}⟨x ⊑ y ⊑ … ⊑ x ⊑ y ⊑ …⟩ \\ & = & ⨆_{A}⟨y ⊑ … ⊑ y ⊑ …⟩ & = & y \end{aligned}

using (Constant) twice. Thus, P_{A} is an ω-cpo. And, by the natural isomorphism (6),

A(\overline{ω}) ≅ Preo(ω, P_{A}) ≅ ω-Cpo(\overline{ω}, P_{A}).

Hence A ≅ Y(P_{A}).

5 Logical characterization of ω-Cpo

The logical interpretation of Theorem 4.4 gives the following logical description of the objects of ω-Cpo.

Theorem 5.1 The full subcategory ω-Cpo^{⊂} → H consists of those sheaves A such that

(A is complete)  ^{∥−} ∀σ ∈ A^{I}. ∃!τ ∈ A\overline{ω}. σ = τ ∘ c
(A is path-transitive) ^{∥−} ∀δ ∈ A^{Σ∨Σ}. ∃!γ ∈ A^{Σ_{2}}. δ = γ ∘ t
(A is ¬¬-separated) ^{∥−} ∀x, y ∈ A. ¬¬(x = y) ⇒ x = y.

We show that every ω-cpo D = (|D|, ⊑_{D}) comes with an intrinsic notion of approximation ≤_{D} and passage to the limit ⋁_{D}, making (D, ≤_{D}, ⋁_{D}) an internal ω-cpo in H, with respect to which all maps are continuous.

Let ≤_{D} ⊆ D × D be the ω-cpo with underlying set ⊑_{D} ordered pointwise. As an object in H, ≤_{D} has two internal descriptions; namely, as the specialization order

∥− ∀x, y ∈ D. x ≤_{D} y ⟺ ∀τ ∈ Σ^{D}. τ(x) ⇒ τ(y)

which is the intrinsic order defined by the admissible subsets of D, and as the path relation

∥− ∀x, y ∈ D. x ≤_{D} y ⟺ ∃α ∈ D^{Σ}. α(⊥) = x ∧ α(⊤) = y.

Thus, (D, ≤_{D}) is an internal poset in H.

Let

Chain(D, ≤_{D}) =^{def} {σ ∈ D^{N} | ∀n ∈ N. σ_{n} ≤_{D} σ_{n+1}}

be the object of countable ascending chains in (D, ≤_{D}). We have that

Chain(D, ≤_{D}) ≅ D^{I}

and so the lub-operator ⋁_{D}: Chain(D, ≤_{D}) → D may be obtained as the composite

Chain(D, ≤_{D}) ≅ D^{I} ^{D^{c}}→ D\overline{ω} ^{D^{∞}} → D.

One can show that (D, ≤_{D}, ⋁_{D}) is an internal ω-cpo in H.

Furthermore, for ω-cpos P and Q we have that

∥− ∀φ ∈ Q^{P} . ∀σ ∈ Chain(P, ≤_{P}). φ(⋁_{P} σ) = ⋁_{Q}(φ ∘ σ).

Thus, every map f: P → Q in H is ω-continuous with respect to the intrinsic order.

6 Conclusions

We have obtained full embeddings

Rep(H)^{⊂} → ω-Cpo^{⊂} → WC(H) = C(H),

where Rep(H), WC(H), and C(H) respectively denote the full subcategories of H consisting of the replete, the well-complete, and the complete objects.

Thanks to the universal characterization of the category of replete objects as the smallest full reflective exponential ideal contaning Σ (see [12,13]), we know that Rep(H) = Rep(ω-Cpo). Thus, for the topos H the internal notion of repleteness determines a good class of “standard” domains. All constructions on ω-cpos used in denotational semantics actually take place within the replete objects, see [25]. It is not clear if the notion of repleteness in H (or in ω-Cpo for that matter) coincides with some existent notion of domain: we only know that the inclusion is strict because of a counterexample worked out by Michael Makkai and the second author [19].

It is clear that the other inclusion ω-Cpo^{⊂} → WC(H) is strict by Theorem 4.4 as it is easy to imagine examples of complete objects which are not path-transitive or ¬¬-separated. In other words, one can appreciate the subtle differences between notions of domains purely in logical terms: replete and well-complete mark somehow the two extremes. The latter is just the bare essential in order to get the internal logic working to yield the basic results about fixpoints; the former further requires of an object all properties of Σ, true in the universe, to hold for the object. Our characterization shows that, in the logic of H, the requirements for ω-cpos are ad hoc: an unavoidable algebraic condition (completeness) together with two useful logical properties. Separation allows to perform certain arguments in a classical way; path-transitivity makes ω-chains definable by their finite prefixes.

Our result establishes a direct link between traditional methods in denotational semantics and the synthetic approach. It is important to note that the synthetic approach suggests different kinds of categories of domains. In the case of repleteness, it suggest a different (probably new), intrinsic notion of a good category of ω-cpos; in the case of well-completeness, it presents a natural extension of the traditional interpretation of fixed-point operators by lubs of ω-chains.

References

[1] A. Bucalo and G. Rosolini. Repleteness and the associated sheaf. To appear in the J. Pure Appl. Alg., 1997.

[2] A. Carboni, M.C. Pedicchio, and G. Rosolini, editors. Category Theory ’90, volume 1488 of Lectures Notes in Mathematics, Como, 1991. Springer-Verlag.

[3] E.J. Dubuc. Concrete quasitopoi. In Fourman et al. [11], pages 239–279.

[4] M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Cambridge University Press Distinguished Dissertations in Computer Science, 1996.

[5] M.P. Fiore. Enrichment and representation theorems for categories of domains and continuous functions. Manuscript available as rep.dvi from

http://www.dcs.ed.ac.uk/home/mf/ADT, 1996.

[6] M. P. Fiore. An enrichment theorem for an axiomatisation of categories of domains and continuous functions. To appear in Mathematical Structures in Computer Science —Proceedings of the Workshop LDPL’95, 1997.

[7] M.P. Fiore and G.D. Plotkin. An extension of models of axiomatic domain theory to models of synthetic domain theory. To appear in Proceedings of the CSL’96 Conf., 1997.

[8] M. Fiore and G. Rosolini. Two models of Synthetic Domain Theory. J. Pure Appl. Alg., 116:151–162, 1997.

[9] P.J. Freyd and G.M. Kelly. Categories of continuous functors I. J. Pure Appl. Alg., 2:169–191, 1972.

[10] P.J. Freyd, P. Mulry, G. Rosolini, and D.S. Scott. Extensional PERs. Inform. and Comput., 98:211–227, 1992.

[11] M. Fourman, C. Mulvey, and D.S. Scott, editors. Application of Sheaves, volume 753 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

[12] J.M.E. Hyland. First steps in Synthetic Domain Theory. In Carboni et al. [2], pages 95–104.

[13] J.M.E. Hyland and E. Moggi. The S-replete construction. In Pitt et al. [20], pages 96–116.

[14] M. Jibladze. A presentation of the initial lift-algebra. J. Pure Appl. Alg., 116:185–198, 1997.

[15] P.T. Johnstone. Topos Theory. Academic Press, 1977.

[16] J.R. Longley. Realizability Toposes and Language Semantics. PhD thesis, Department of Computer Science, University of Edinburgh, 1995.

[17] J. Longley and A. Simpson. A uniform approach to domain theory in realizability models. To appear in Mathematical Structures in Computer Science —Proceedings of the Workshop LDPL’95, 1997.

[18] S. Mac Lane and I. Moerdijk. Sheaves in geometry and logic. Springer-Verlag, 1992.

[19] M. Makkai and G. Rosolini. Studying repleteness in the category of cpos. This volume, 1997.

[20] D.H. Pitt, P.T. Johnstone, and A.M. Pitts, editors. Category theory and Computer Science, Lectures Notes in Computer Science, Cambridge, 1995. Springer-Verlag.

[21] B. Reus. Program Verification in Synthetic Domain Theory. Dokt.Diss., Lüdwig-Maximilians-Universität München, 1995. Shaker Verlag, Aachen.

[22] G. Rosolini. Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986.

[23] G. Rosolini. Categories and effective computations. In D.H. Pitt, A. Poigné, and D.E. Rydeheard, editors, Category theory and Computer Science, volume 283 of Lectures Notes in Computer Science, pages 1–11, Edinburgh, 1987. Springer-Verlag.

[24] G. Rosolini. An ExPER model for QUEST. In S. Brookes, editor, Mathematical Foundations of Programming Semantics, volume 598 of Lectures Notes in Computer Science, Pittsburgh, 1992. Springer-Verlag.

[25] G. Rosolini. Notes on Synthetic Domain Theory, 1996. Available from

ftp://ftp.disi.unige.it.

[26] P. Taylor. The fixed point property in synthetic domain theory. In G. Kahn, editor, Logic in Computer Science 6, pages 152–160, Amsterdam, 1991. IEEE.