Math. Struct. in Comp. Science (1997), vol. ?, pp. ??–?? Copyright \begin{matrix}c \\ ◯ \end{matrix} Cambridge University Press

An Enrichment Theorem for an Axiomatisation of Categories of Domains and Continuous Functions

M a r c e l o P. F i o r e^{†}

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

Email: mf@dcs.ed.ac.uk

Received 25 October 1996

Domain-theoretic categories are axiomatised by means of categorical non-order-theoretic requirements on a cartesian closed category equipped with a commutative monad. An enrichment theorem showing that every axiomatic domain-theoretic category can be endowed with an intensional notion of approximation, the path relation, with respect to which the category Cpo-enriches is proved. Our analysis suggests more liberal notions of domains. In particular, a category where the path order is not ω-complete, but in which the constructions of domain theory (as, for example, the existence of uniform fixed-point operators and the solution of domain equations) are available is presented.

Introduction

Domain theory (Sco70) is a mathematical theory of computation that provides models for spaces over which to define computable functions. The theory is based on the notion of approximation (or information order) between partial objects, which is formalised by means of order-theoretic structures. More precisely, domains are partially ordered sets equipped with a notion of passage to the limit (for appropriate subsets of partial objects) given by least upper bounds, and computable functions are taken to be continuous (i.e. to preserve the notions of approximation and passage to the limit). The simplest of these structures is Cpo, the category of small cpos (posets, possibly without bottom element, closed under lubs of ω-chains) and continuous functions (monotone functions that preserve lubs of ω-chains).

This paper studies the notions of approximation and passage to the limit in an axiomatic setting. Our axiomatisation is subject to the following criteria: the axioms should be natural (so that they are available in as many contexts as possible) and non-order-theoretic (so that they explain the order-theoretic structure). Our aim is

† Research supported by SERC grant RR30735, EC grant SC1000 795, and EPSRC grant GR/J84205.

1 to provide a justification of Scott’s original consideration of ordered structures, and 2 to deepen our understanding of the notion of passage to the limit. From a wider perspective, these investigations form part of a programme to formulate an axiomatic theory of domains —see (FJM^{+}96, § Axiomatic Domain Theory).

Concerning (1), in accordance with traditional views of domains, we set up a categorical axiomatic framework in which an intensional notion of approximation, the so-called path relation, can be defined and shown to be ω-complete.

Concerning (2), in order to broaden the concept of domain, we present a category in which the notion of approximation is not ω-complete, but that allows the constructions of domain theory.

In our exposition, we have decided to intertwine the introduction of assumptions and axioms with the development of the theory so that the contribution of each axiom is always clear. The assumptions are the means for introducing the categorical structure over which the axioms impose the extra requirements asked for in the models. Our axiomatisation can be classified as follows: I. Axioms 1 and 2 introduce the infinitary structure allowing the definition of a uniform

fixed-point operator for endomorphisms on pointed objects. II. Axiom 3 forces the notion of approximation to be transitive and, together with Ax-

ioms 1 and 2, permits the definition of a notion of passage to the limit for ω-chains of approximations.

III. Axioms 4 and 5 force the passage-to-the-limit operator to be computed by lubs.

In Section 1 we introduce our basic assumption; viz. we assume a cartesian category of discourse equipped with a commutative monad 𝕃 = (L, η, μ, t′). This data captures the basic structure present in the leading example given by Cpo with the lifting monad on it. Other examples of categories with a lifting monad are introduced to aid the reader in understanding the axioms. (The status of these examples with respect to our axiomatisation is discussed in Section 9.) In Section 2 we axiomatise lifting. First, as in synthetic domain theory, we consider dominances; then, we introduce the notion of lifting structure, characterise it in terms of dominances, and show that they induce a commutative monad (henceforth called lifting). In Section 3 we consider the category of Eilenberg-Moore algebras for the monad 𝕃 as a category of pointed objects and strict maps. In this view, every pointed object is equipped with a bottom element preserved by strict maps. In Section 4 we introduce the first two axioms and exemplify their use by defining a uniform fixed-point operator, fix, for endomorphisms on pointed objects. Axiom 1 postulates the existence of a fixed-point object consisting of an algebra σ : L\overline{ω} → \overline{ω}, and Axiom 2 equips \overline{ω} with a global element ∞ invariant under iteration. The essential difference between our fixed-point object and the one previously considered in (CP92) is its inductive nature, in that we require it to arise as the colimit for the standard ω-chain generated by iterating L. An intensional notion of approximation, the path relation (⊑), is introduced in Section 5 and characterised for the examples of Section 1. (In the context of synthetic domain theory the path relation has been considered briefly in (Pho90) (where it is called the link relation); it is also implicit in (Hyl91) and (Tay91), where it is required to coincide with the intrinsic (or specialisation) order.) The path relation interacts as expected with composition, L, pairing, and currying; but it need not be transitive. By introducing Axiom 3, transitivity is achieved and the path relation is shown to provide a Preo-enrichment for our category of discourse. Section 6 proposes axioms that provide a passage-to-the-limit operator V for countably infinite sequences of approximations. With this structure we establish the first algebraic properties of the operator V. Surprisingly, we are far from having an ω-complete notion of approximation. Sections 7 and 8 introduce the last two axioms, Axioms 4 and 5, which make Σ ( =^{def} L1) behave externally as the Sierpinsky space 2; as a consequence \overline{ω} can be regarded externally as the first infinite ordinal ω. We are then in a position to prove the internal completeness of the objects in our category of discourse and as a corollary, externalising via the Yoneda embedding, obtain the enrichment theorem: i.e. that every domain-theoretic category (viz. one that is a model of our axioms) Cpo-enriches with respect to the path relation. The leading example of a domain-theoretic category is —naturally— Cpo with the lifting monad.

The fact that categories of domains and stable functions fail to satisfy our last axiom suggests more liberal notions of domains. In particular, in Section 10, we present a category which contains the category Cpo_{∧} of cpos with continuous pullbacks and stable functions as a full subcategory, satisfies all but the last axiom, and does not Cpo-enrich with respect to the path order. Nevertheless, in this new category the constructions of domain theory (as, for example, the existence of uniform fixed-point operators and the solution of domain equations) are available.

In a companion paper we will exploit our axiomatisation and the enrichment theorem to get a representation theorem of domain-theoretic categories equipped with a lifting monad into categories of cpos and continuous functions (in a suitable intuitionistic set theory).

1. Basic assumptions

Our basic data is: Assumption 1. We assume a cartesian category of discourse C and a commutative monad 𝕃 = (L, η, μ, t′) on it.

To keep the paper reasonably self contained the above structure is defined; for details consult (Koc70; Koc71; Mog91). Definition 1.1. 1 Let C be a category. A monad 𝕃 = (L, η, μ) on C consists of a functor L : C → C,

and natural transformations η_{C} : C → LC (the unit) and μ_{C} : L^{2}C → LC (the multiplication) such that

— μ_{C} ∘ μ_{LC} = μ_{C} ∘ Lμ_{C} : L^{3}C → LC;

— μ_{C} ∘ η_{LC} = id_{LC} and μ_{C} ∘ Lη_{C} = id_{LC}. 2 Let C be a cartesian category. A commutative monad 𝕃 = (L, η, μ, t′) on C consists of

a monad 𝕃 = (L, η, μ) on C and a natural transformation t′_{A,B} : A × LB → L(A × B) (the tensorial strength) such that — L(r_{C})∘t′_{1,C} = r_{LC} : 1×LC → LC and L(a_{A,B,C})∘t′_{A×B,C} = t′_{A,B×C} ∘(id_{A}×t_{B,C})∘

a_{A,B,LC} : (A × B) × LC → L((A × B) × C), where r_{C} and a_{A,B,C} are respectively the canonical natural isomorphisms 1 × C ≅ C and (A × B) × C ≅ A × (B × C);

— t′_{A,B} ∘ (id_{A} × η_{B}) = η_{A×B} : A × B → L(A × B) and t′_{A,B} ∘ (id_{A} × μ_{B}) = μ_{A×B} ∘ (Lt_{A,B}) ∘ t_{A,LB} : A × L^{2}B → L(A × B);

— μ_{A×B} ∘(Lt′′_{A,B})∘t′_{LA,B} = μ_{A×B} ∘(Lt′_{A,B})∘t′′_{A,LB} : L(A)×L(B) → L(A×B), where

t′′_{A,B} =^{def} L(c_{B,A}) ∘ t′_{B,A} ∘ c_{LA,B} : L(A) × B → L(A × B) with c_{A,B} the canonical

natural isomorphism A × B ≅ B × A.

Examples of the categorical structure of Assumption 1 are lifting monads (see Example 1.2 and Section 2) and powerdomain monads (see (HP79; AJ96)).

Example 1.2. (Lifting monads)

1 Let Set be the category of small sets and functions.

The lifting monad on Set can be described as follows: it has underlying functor ( )+1 associating to a set A the set A + 1 = {∗} ∪ {[a] | a ∈ A} with unit the inclusion A ↪ A + 1 : a ↦ [a], multiplication (A + 1) + 1 → A + 1 sending ∗ ↦ ∗, [∗] ↦ ∗, [[a]] ↦ [a], and tensorial strength A × (B + 1) → (A × B) + 1 sending ⟨a, ∗⟩ ↦ ∗ and ⟨a, [b]⟩ ↦ [⟨a, b⟩].

2 Let (Preo) Poset be the category of small (preorders) posets and monotone functions. The lifting monad on (Preo) Poset can be described as follows: it has underlying functor ( )_{⊥} associating to a (preorder) poset P the (preorder) poset P_{⊥} = {⊥} ∪ {[x] | x ∈ P } where ⊥ ≤_{P_{⊥}} [x] and [x] ≤_{P_{⊥}} [y] ⟺ x ≤_{P} y with unit the inclusion P ↪ P_{⊥} : x ↦ [x], multiplication (P_{⊥})_{⊥} → P_{⊥} sending ⊥ ↦ ⊥, [⊥] ↦ ⊥, [[x]] ↦ [x], and tensorial strength P ×Q_{⊥} → (P ×Q)_{⊥} sending ⟨x, ⊥⟩ ↦ ⊥ and ⟨x, [y]⟩ ↦ [⟨x, y⟩].

3 Let Cpo be the category of small cpos and continuous functions.

The lifting monad on Poset restricts to a lifting monad on Cpo. 4 Convention. To emphasise the distinction between ordinary and order-enriched cat-

egories the latter are subscripted with the order providing the enrichment. (Thus, for example, for a category K, K_{=} denotes the order-enriched category induced by K by discretely ordering each hom-set.) The ordinary underlying category of an orderenriched category W_{≤} is denoted W.

Let Cpo_{⊑} be the Cpo-category of small cpos and continuous functions ordered pointwise (i.e. f ⊑ g : P → Q ⟺ ∀ x ∈ P. fx ≤_{Q} gx). For W_{≤} a small Cpo-category, let [W_{≤}^{op}, Cpo_{⊑}] be the functor category of Cpofunctors and natural transformations. The pointwise lifting monad on [W_{≤}^{op}, Cpo_{⊑}] has underlying functor [W_{≤}^{op}, ( )_{⊥}] : F ↦ ( )_{⊥} ∘ F, with unit, multiplication, and tensorial strengths given pointwise.

5 Let (Poset∧) Cpo_{∧} be the category of small (posets) cpos with (monotone) continuous pullbacks and stable (i.e. (monotone) continuous pullback preserving) functions. The lifting monad on Poset restricts to a lifting monad on (Poset_{∧}) Cpo_{∧}.

The reader should keep in mind that Cpo equipped with the lifting monad is considered the leading example of a domain-theoretic category; and hence it will guide our axiomatisation.

2. Lifting

In this section we review a, by now standard, axiomatisation of lifting monads in terms of dominances. (For the connection between this axiomatisation and partiality consult (Fio96).) Lifting monads are a fundamental example of Assumption 1, and hence important for understanding it. However, since the constructions of this section are only needed for treating Examples 5.2 (5), 5.8, and 5.9, on a first reading, it may be skipped. Convention. Subobjects obtained as pullbacks of a monomorphism m are called msubobjects.

In the vein of synthetic domain theory (Ros86; Hyl91; Tay91), we consider a generic observable property, ⊤ : 1 ↪ Σ, whose role is to internalise the notion of termination and hence determine the observable properties (⊤-subobjects) of all objects. Definition 2.1. (Dominance (Ros86)) Let K be a category with a terminal object 1. An object Σ equipped with a subobject ⊤ : 1 ↪ Σ such that pullbacks of ⊤ always exist is called a ⊤-suboject classifier if every ⊤-subobject D ↪ A appears in a pullback

D A  1 Σ⊤

for a unique characteristic map A → Σ. A ⊤-subobject classifier is called a dominance if

— ⊤^{∗} : K/Σ → K has right adjoint, and

— ⊤-subobjects are closed under composition. Remark. In the context of SDT, dominances are only defined by the second requirement, as the first requirement generally holds in the universes of sets considered (e.g. locally cartesian closed categories with finite limits, as toposes and quasitoposes). Remark. 1 Pullbacks of ⊤-subobjects always exist. 2 In a cartesian category, if m : D ↪ A is a ⊤-subobject then so is m × B : D × B ↣

A × B because if m has characteristic map f : A → Σ then m × B has characteristic map f ∘ π_{1} : A × B → Σ. Hence, if m and n are ⊤-subobjects then so is m × n.

Examples of dominances: Example 2.2. (Dominances) 1 In Set, let 1 = {0} and 2 = {0, 1}. Then, 1 ↪ 2 : 0 ↦ 1 classifies all subsets. 2 In (Preo) Poset, let 1 = {0} and 2 = {0 ≤ 1}. Then, 1 ↪ 2 : 0 ↦ 1 classifies

upper-closed subsets.

3 In Cpo, 1 ↪ 2 : 0 ↦ 1 classifies Scott-open subsets. 4 For W_{≤} a small Cpo-category, let 1 : W_{≤}^{op} → Cpo_{⊑} : w ↦ 1.

(a) Let 2 : W_{≤}^{op} → Cpo_{⊑} : w ↦ 2.

Then, ⊤ : 1 ↪ 2 defined by ⊤_{W} (0) = 1 classifies the pointwise-Scott-open cartesian natural (i.e. natural transformations in which the squares required to commute by naturality are pullbacks) monos.

(b) Let 𝔖 : W_{≤}^{op} → Cpo_{⊑} be the Cpo-functor defined

— on objects: as 𝔖(W) = (Scott-sieves(W), ⊆) where a sieve R on W (i.e. a subset of ∐_{V ∈|W|} W(V, W) satisfying the closure property: for every f : V → W in R and g : V′ → V in W, f ∘ g is in R) is said to be Scott if for every V ∈ | W |, R ∩ W(V, W) is Scott-open in W_{≤}(V, W); and

— on morphisms: as 𝔖(f : W′ → W)(R) = {h : V → W′ | f ∘ h ∈ R}.

Then, ⊤ : 1 ↪ 𝔖 defined by ⊤_{W} (0) = ∐_{V ∈|W|} W_{≤}(V, W) classifies the pointwise-Scott-open natural monos.

5 In (Poset_{∧}) Cpo_{∧}, 1 ↪ 2 : 0 ↦ 1 classifies (upper-closed) Scott-open subsets closed

under pullbacks. 6 In a topos, true : 1 → Ω classifies subobjects.

The above dominances satisfy the extra requirement of classifying the unique map 0 → 1; thus allowing the notion of non-termination to be internalised as a map 1 → Σ. Now we introduce an alternative description of these dominances in terms of so-called lifting structures (see Theorem 2.4). Definition 2.3. (Lifting structure) Let K be a category with an initial object 0 and a terminal object 1. A lifting structure (( )_{⊥}, [ ]) on K consists of a pointed endofunctor [ ] : Id \underrightarrow{.} ( )_{⊥} : K → K such that

— pullbacks of [ ]_{1} always exist,

— [ ] is cartesian (that is, for every f : A → B,

\begin{matrix}A & \overline{f →} & B \\ A_{⊥} & ^{[ ]_{A}↓ ∩} & \overline{_{f_{⊥}→}} & B_{⊥} & \begin{matrix}↓ & ∩ \\ [ ]_{B} \end{matrix} \end{matrix}

is a pullback square),

— for every B ∈ | K |, [ ]_{B} classifies [ ]_{1}-partial maps with target B (that is, every span A ↩ D → B with D ↪ A an [ ]_{1}-subobject appears in a pullback

\begin{aligned}D & \overline{→} & B \\ A & ^{↓ ∩} & \overline{→} & B_{⊥} & \begin{matrix}↓ & ∩ \\ [ ]_{B} \end{matrix} \end{aligned}

for a unique characteristic map A → B_{⊥}), and — the composite 1 ^{⊂} \underrightarrow{[ ]_{1}} 1_{⊥} ^{⊂} \underrightarrow{[ ]_{1_{⊥}}} (1_{⊥})_{⊥} and the unique map 0 → 1 are [ ]_{1}-subobjects.

Theorem 2.4. Lifting structures and dominances that classify 0 → 1 are in bijective correspondence.

Proof. See (Fio96, Chapter 3).

Lifting structures are easily seen to provide the structure of a commutative monad: Definition 2.5. (Lifting) Every lifting structure (( )_{⊥}, [ ]) on K induces a lifting monad (( )_{⊥}, [ ], μ) on K with multiplication defined as:

A \overline{A→} A

A_{⊥}^{[ ]_{A}↓ ∩}

(A_{⊥})_{⊥}^{[ ]_{A_{⊥}}↓ ∩}  \overline{_{μ_{A}→}} A_{⊥} \begin{matrix}↓ & ∩ \\ [ ]_{A} \end{matrix}.

Moreover, for cartesian K, the lifting monad is commutative with tensorial strength defined as:

\begin{matrix}A × B & \overline{A × B→} & A × B \\ A × B_{⊥} & ^{A × [ ]_{B}↓ ∩} & \overline{_{_{t′_{A,B}}→}} & (A × B)_{⊥} & \begin{matrix}↓ & ∩ \\ [ ]_{A×B} \end{matrix} & . \end{matrix}

Example 2.6. The lifting monads induced by the dominances of Example 2.2 are:

— for Example 2.2 (1), that of Example 1.2 (1);

— for Example 2.2 (2), that of Example 1.2 (2);

— for Example 2.2 (3), that of Example 1.2 (3);

— for Example 2.2 (4a), that of Example 1.2 (4);

— for Example 2.2 (5), that of Example 1.2 (5);

— for Example 2.2 (6), the partial map classifier monad (see (Joh77)). Proposition 2.7. The category of Eilenberg-Moore algebras for a lifting monad on a category with a strict initial object has a zero object.

3. Pointed objects and strict maps

We write C^{𝕃} for the category of Eilenberg-Moore algebras for the monad 𝕃. In the leading example, Cpo with the lifting monad, we have that Cpo^{𝕃} is the category of small cpos with a least element and strict continuous functions. Thus the following:

Convention. An algebra for the monad 𝕃 is called a pointed object. The algebra structure on a pointed object X is denoted by ρ_{X} but generally left implicit; moreover ρ_{LA} is taken to be μ_{A} unless specified otherwise. Algebra homomorphisms are called strict and are denoted with ∘→. When we write X ∘→ Y, X and Y are assumed to be pointed. Remark. If C^{𝕃} has a zero object 1 then C has a terminal object 1 (as the forgetful functor C^{𝕃} → C has a left adjoint and therefore preserves limits); moreover if C has an initial object 0 then L0 ≅ 1, and η_{0}, μ_{0}, t′_{A,0}, t′_{0,B} have target 1 and hence are uniquely determined by their source. Assumption 2. We assume C^{𝕃} has a zero object 1. Definition 3.1. (Bottom) For a pointed object X we define ⊥_{X} to be the unique strict map 1 ∘→ X. Remark. For every f : X ∘→ Y, f ∘ ⊥_{X} = ⊥_{Y} and hence ⊥_{X} = ρ_{X} ∘ ⊥_{LX}.

4. Inductive fixed-point object

The axioms of this section introduce the infinitary structure allowing the definition of a uniform fixed-point operator, fix, for endomorphisms on pointed objects. Convention. We set: Σ = L1, Σ_{n} = L^{n}1, ⊥ = (1 ∘→ Σ), ⊤ = η_{1} : 1 → Σ.

To motivate the first axiom it is convenient to regard Σ_{n} as a canonical chain of n + 1 elements. In fact, as we show below, for n ≥ 0, every Σ_{n} comes equipped with global elements \underline{k}_{Σ_{n}} : 1 → Σ_{n} (0 ≤ k ≤ n) such that, for 0 ≤ i ≤ j ≤ n, we have \underline{i}_{Σ_{n}} ⊑ \underline{j}_{Σ_{n}} for a suitable notion of approximation ⊑ (defined in Section 5). Definition 4.1. (\underline{i}_{Σ_{n}}) For 0 ≤ i ≤ n, we inductively define \underline{i}_{Σ_{n}} : 1 → Σ_{n} as follows:

\underline{0}_{Σ_{n}} =^{def} (1∘→Σ_{n}) and \underline{i + 1}_{Σ_{n+1}} =^{def} (1 \overline{⊤→} Σ \overline{\underrightarrow{L(\underline{i}_{Σ_{n}})}} Σ_{n+1}) = (1 \overline{\underrightarrow{\underline{i}_{Σ_{n}}}} Σ_{n} \overline{\underrightarrow{η_{Σ_{n}}}} Σ_{n+1}).

In view of the above intuition, Axiom 1 postulates the existence of a countably infinite chain, \overline{ω}, obtained by pasting the Σ_{n}’s so that they become the finite prefixes of \overline{ω}. Formally: Axiom 1. (\overline{ω}) The functor L : C → C has an algebra σ : L\overline{ω} → \overline{ω} such that the cone ⟨s_{n}⟩ : ⟨L^{n}⊥ : Σ_{n} → Σ_{n+1}⟩ \underrightarrow{.} \overline{ω}, inductively defined as: s_{0} = σ∘⊥_{L\overline{ω}} and s_{n+1} = σ∘L(s_{n}), is colimiting. (That is, the following

1 \overline{ω} σ ∘ ⊥_{L\overline{ω}}  ⊥_{L\overline{ω}} σ  Σ L\overline{ω}L(σ ∘ ⊥_{L\overline{ω}}) Lσ  L^{2}\overline{ω}L^{2}(σ ∘ ⊥_{L\overline{ω}})  · · · · · · L^{2}σ ⊥  L⊥  L^{2}⊥ Σ_{2}

is a colimit diagram.)

In the leading example, Cpo with the lifting monad, we take \overline{ω} to be ω + 1 (the successor ordinal of ω) and σ to be the successor map sending ⊥ ↦ 0, n ↦ n+1 (n ≥ 0), and ω ↦ ω.

Also in the axiomatic framework the successor operation can be defined: Definition 4.2. 1 (\underline{n}\overline{ω}) For every n ≥ 0, we define \underline{n}\overline{ω} =^{def} s_{n} ∘ \underline{n}_{Σ_{n}} : 1 → \overline{ω}. 2 (succ) We define succ : \overline{ω} → \overline{ω} as the composite σ ∘ η\overline{ω}. Proposition 4.3. For n ≥ 0, succ ∘ \underline{n}\overline{ω} = \underline{n + 1}\overline{ω}.

Axiom 2 equips \overline{ω} with a point at infinity, ∞, characterised by its invariance under iteration: Axiom 2. (∞) \overline{ω} has a global element ∞ which is a fixed-point of succ. Convention. For n ≥ 0, we inductively define η_{A}^{(n)} : A → L^{n}A as η_{A}^{(0)} = A and η_{A}^{(n+1)} = η_{L^{n}A} ∘ η_{A}^{(n)} = η_{LA}^{(n)} ∘ η_{A}.

Proposition 4.4. (The invariance of ∞) For n ≥ 0, σ ∘…∘(L^{n}σ)∘η(n+1) ; \overline{ω} ∘∞ = ∞.

The rest of the section is devoted to exemplifying the use of the axioms by showing how one can define a uniform fixed-point operator fix. To this purpose, given an endomorphism f on a pointed object X we first internalise the sequence ⟨⊥_{X}, f ∘ ⊥_{X}, …, f^{n} ∘ ⊥_{X}, …⟩ of iterations of f at ⊥_{X} and then extract its value at infinity. Precisely: Definition 4.5. 1 (it) For every endomorphism f on a pointed object X, we define it(f) : \overline{ω} → X as

the unique mediating morphism from the colimiting cone ⟨s_{n}⟩ to the cone ⟨it_{n}(f)⟩ inductively defined as: it_{0}(f) = ⊥_{X} and it_{n+1}(f) = ρ_{X} ∘ L(f ∘ it_{n}(f)).

2 (fix) For every endomorphism f on a pointed object X, we define fix(f) : 1 → X as

the composite it(f) ∘ ∞. Proposition 4.6. For every endomorphism f on a pointed object X, 1 f ∘ it(f) = it(f) ∘ succ, and 2 (fix is a fixed-point operator) f ∘ fix(f) = fix(f).

Proof.

(1) Because for n ≥ 0,

it(f) ∘ σ ∘ η\overline{ω} ∘ s_{n} = it(f) ∘ σ ∘ L(s_{n}) ∘ η_{Σ_{n}} = it(f) ∘ s_{n+1} ∘ η_{Σ_{n}}
= it_{n+1}(f) ∘ η_{Σ_{n}}  = ρ_{X} ∘ L(f ∘ it_{n}(f)) ∘ η_{Σ_{n}}
= ρ_{X} ∘ η_{X} ∘ f ∘ it_{n}(f) = f ∘ it(f) ∘ s_{n}.

(2) We calculate: f ∘ fix(f) = f ∘ it(f) ∘ ∞ = it(f) ∘ succ ∘ ∞ = it(f) ∘ ∞ = fix(f). Proposition 4.7. (Uniformity) The fixed-point operator fix is uniform. That is, if

(X ⟶^{f} X ∘⟶^{h} Y) = (X ∘⟶^{h} Y ⟶^{g} Y) then h ∘ fix(f) = fix(g).

Proof. Because h ∘ it(f) = it(g).

For our subsequent development σ need not be an isomorphism; when it is (as happens in the leading example and in domain-theoretic categories —see Section 9) we have: Proposition 4.8. Assume σ is an isomorphism. Then, 1 (\overline{ω}, σ ∘ μ\overline{ω} ∘ Lσ^{−1}) is a pointed object and σ is strict; 2 if ∞ is the unique fixed-point of succ then the uniformity property characterises fix; 3 σ : L\overline{ω} → \overline{ω} is an initial L-algebra and, for every endomorphism f on a pointed

object X, it(f) is characterised as the unique L-algebra homomorphism (\overline{ω}, σ) → (X, ρ_{X} ∘ Lf). Proof.

(2) Let Y be a uniform fixed-point operator. Since it(f)∘σ = ρ_{X} ∘L(f ∘it(f)), it follows that it(f) is a strict morphism \overline{ω} ∘→X because

L\overline{ω}  \overline{L(it(f))  →} LX

L^{2}\overline{ω}^{Lσ^{−1}↓} \overline{\underrightarrow{L^{2}(f ∘ it(f))}} L^{2}X Lρ_{X}→

L\overline{ω}^{μ\overline{ω}↓} \overline{_{L(f ∘ it(f))→}} LX^{μ_{X}↓}

\overline{ω}^{σ↓}  \overline{_{it(f)  →}} X^{↓ρ_{X}}^{ρ_{X} →} .

Then, as it(f) ∘ succ = f ∘ it(f) we have that Y(f) = it(f) ∘ Y(succ) = it(f) ∘ ∞ = fix(f).

(3) Given α : LA → A define the cone ⟨a_{n}⟩ : ⟨Σ_{n}⟩ \underrightarrow{.} A inductively as follows: a_{0} = α ∘ ⊥_{LA} and a_{n+1} = α ∘ L(a_{n}). Then, for h : \overline{ω} → A it follows by induction that, for n ≥ 0, α∘(Lh)∘σ^{−1} ∘s_{n} = a_{n} and hence h : (\overline{ω}, σ) → (A, α) if and only if h : ⟨s_{n}⟩ → ⟨a_{n}⟩. The second part follows because it(f) = ρ_{X} ∘ L(f ∘ it(f)) ∘ σ^{−1}.

5. Path order

The notion of approximation, viz. the path relation, is introduced; for further analysis consult (Fio95). After studying examples (both for concrete models and in the axiomatic setting) the properties of the path relation and its interaction with relevant categorical structure are considered. In particular, we show that the path relation need not be transitive. By introducing Axiom 3, transitivity is achieved and the path relation is shown to provide a Preo-enrichment for our category of discourse.

We have equipped Σ with two global elements ⊥ and ⊤ intuitively corresponding to non-termination and termination. Thus, ⊥ approximates ⊤. Informally, let us visualise this fact as the existence of a directed path ⊥ ⊤ from ⊥ to ⊤ in Σ, and say that such a path is a proof that ⊥ approximates ⊤. With this viewpoint, it is natural to say, for two global elements x and y of an object C, that x approximates y if the canonical path ⊥ ⊤ can be transformed, via a map Σ → C, into a path x y from x to y in C. In symbols, x ⊑ y : 1 → C if there exists (a proof ) α : Σ → C such that α ∘ ⊥ = x and α ∘ ⊤ = y. A formalisation of these intuitions leads to the following: Definition 5.1. For f, g : A → B and α : Σ × A → B, we set α : f g : A → B if and only if

Σ × A  α  B ⊤ × A 1 × A ≅ A ⊥ × A 1 × A ≅ A  fg  .

Moreover, we define the path relation f ⊑ g : A → B if and only if there exists α : Σ × A → B such that α : f g.

We characterise the path relation for some of our examples: Example 5.2. 1 For the lifting monad on Set (see Example 1.2 (1)), the path relation is indiscrete

(i.e. f ⊑ g for all f and g). 2 For the lifting monad on (Preo) Poset and Cpo (see Examples 1.2 (2)–(3)), the

path relation is the pointwise (pre)order (i.e. f ⊑ g : P → Q ⟺ ∀ x ∈ P. fx ≤_{Q} gx). 3 Let W_{≤} be a small Cpo-category. For the pointwise lifting monad on [W_{≤}^{op}, Cpo_{⊑}]

(see Example 1.2 (4)), the path relation is the pointwise pointwise order; that is,

f ⊑ g : P → Q ⟺ ∀ W ∈ | W_{≤} |. ∀ x ∈ P W. f_{W} x ≤_{QW} g_{W} x.

4 For the lifting monad on Poset_{∧} and Cpo_{∧} (see Example 1.2 (5)), the path relation

is the stable order; that is, f ⊑ g : P → Q ⟺ ∀ x, y ∈ P. x ≤_{P} y ⇒ fx = gx ⊓_{Q} fy. 5 For the monad induced by the dominance 1 ↪ 𝔖 on [2_{=}, Cpo_{⊑}] (see Example 2.2 (4b)),

the path relation is the pointwise pointwise order. Example 5.3. 1 For 0 ≤ i ≤ j ≤ n, \underline{i}_{Σ_{n}} ⊑ \underline{j}_{Σ_{n}} : 1 → Σ_{n}. 2 For 0 ≤ i ≤ j, \underline{i}\overline{ω} ⊑ \underline{j}\overline{ω} : 1 → \overline{ω}. 3 Definition 5.4. (∞_{n}) For n ≥ 0, we define ∞_{n} : Σ → \overline{ω} as the composite

σ ∘ … ∘ (L^{n}σ) ∘ (L^{n+1}∞) ∘ η_{Σ}^{(n)}.

For n ≥ 0, ∞_{n} : \underline{n} ∞ : 1 → \overline{ω}. Example 5.5. Given an endomorphism f on a pointed object X, the sequence ⟨⊥_{X}, f ∘ ⊥_{X}, …, f^{n} ∘ ⊥_{X}, …⟩ of iterations of f at ⊥_{X} becomes a chain with respect to the path relation as f^{n} ∘ ρ_{X} ∘ L(f^{i} ∘ ⊥_{X}) : f^{n} ∘ ⊥_{X} f^{n+i} ∘ ⊥_{X} : 1 → X.

We now incorporate exponentials into our discussion: Assumption 3. We assume C cartesian closed.

Convention. In a cartesian closed category K we write e : A^{B} ×B → A for the evaluation map and λ : K(C × A, B) ≅ K(C, B^{A}) for the currying operator.

Proposition 5.6. (The calculus of proofs (Fio95)) 1 id_{f} : f f : A → B where id_{f} = f ∘ π_{2}. 2 If α : f f′ : A → B and β : g g′ : B → C then β ⋆ α : g ∘ f g′ ∘ f′ : A → C

where β ⋆ α = β ∘ ⟨π_{1}, α⟩. 3 For every pointed object X and every x : 1 → X, ρ_{X} ∘ (Lx) : ⊥_{X} x. 4 If α : f g : A → B then (Lα) ∘ t′ : Lf Lg : LA → LB. 5 α : f f′ : C → A and β : g g′ : C → B if and only if ⟨α, β⟩ : ⟨f, g⟩ ⟨f′, g′⟩ :

C → A × B. 6 α : f g : A × B → C if and only if λ(α ∘ a) : λ(f) λ(g) : A → C^{B} where a is

the canonical isomorphism (Σ × A) × B ≅ Σ × (A × B). Corollary 5.7.

1 For every f : A → X with X pointed, (A → 1 ⟶^{⊥_{X}} X) f : A → X. 2 α : f g : A → B if and only if λ(α) : ⌜f⌝ ⌜g⌝ : 1 → B^{A}.

Proof. (1) By Proposition 5.6 (3), because X^{A} is pointed (with ρ_{X^{A}} = λ(ρ_{X} ∘(Le)∘t′′)) and ⊥_{X^{A}} = ⌜A → 1 ⟶^{⊥_{X}} X⌝ (using Definition 3.1).

Contrary to what Example 5.2 might suggest, the path relation need not be transitive:

Example 5.8. In [↙↘, Cpo], the category of spans over Cpo, with the dominance 1 ↪ 𝔖 (see Section 2, in particular Example 2.2 (4b)) the path relation is not transitive. To see this observe that

(∗, ∗)
1 =
∗ ←  ∗→

and

𝔖 = \begin{aligned}& & & (⊤, ⊤) \\ & & (⊤, ⊥) & & (⊥, ⊤) \\ ⊤ & ← & (⊥, ⊥) & ⊤ & → \\ ⊥ & ← & ⊥ & → \end{aligned}

with the images of ⊥ : 1 → 𝔖 and ⊤ : 1 ↪ 𝔖 respectively corresponding to

(⊥, ⊥)  (⊤, ⊤)

and

⊥ ←  ⊥ →  ⊤ ←  ⊤ → .

Thus, the pushout of 𝔖 ⟵^{⊤} 1 ⟶^{⊥} 𝔖 can be described as

(⊤, ⊤)

(⊤, +)  (+, ⊤)

(+, +)

⊤ ←  (+, ⊥)  (⊥, +)  ⊤ →

+ ←  (⊥, ⊥)  + →

⊥ ←  ⊥ →

and in its hom of global elements we have that

\begin{aligned}& & (⊥, ⊥) \\ ⊥ & ← & ⊥ & → \end{aligned}  \begin{aligned}& & (+, +) \\ + & ← & + & → \end{aligned}  \begin{aligned}& & (⊤, ⊤) \\ ⊤ & ← & ⊤ & → \end{aligned}

but

(⊥, ⊥)  (⊤, ⊤)

⊥ ←  ⊥ →  ⊤ ←  ⊤ → .

The following axiom forces the transitivity of the path relation. Intuitively, thinking of Σ_{n} (n ≥ 0) as a chain of n + 1 elements, the axiom and the fact that pushouts compose imply that Σ_{i+k+j} (i, j, k ≥ 0) results from gluing the upper k + 1 elements of Σ_{i+k} with the lower k + 1 elements of Σ_{k+j}.

Axiom 3. For n ≥ 0, the commuting square

\begin{matrix}Σ_{n} & ∘ L^{n}⊥→ & Σ_{n+1} \\ Σ_{n+1} & ^{η_{Σ_{n}}↓ ∩} & ∘L^{n+1}⊥ → & Σ_{n+2} & \begin{matrix}↓ & ∩ \\ η_{Σ_{n+1}} \end{matrix} \end{matrix}

is a pushout.

Remark. Since pushouts compose, for i, j, k ≥ 0, the commuting square

\begin{matrix}Σ_{k} & ∘ L^{k}⊥→ & Σ_{k+j} \\ Σ_{k+i} & ^{η_{Σ_{k}}^{(i)}↓ ∩} & ∘L^{k+i}⊥ → & Σ_{k+i+j} & \begin{matrix}↓ & ∩ \\ η_{Σ_{k+j}}^{(i)} \end{matrix} \end{matrix}

is a pushout.

Example 5.9. As the path relation in [↙↘, Cpo] with the dominance 1 ↪ 𝔖 is not transitive, Axiom 3 cannot hold there. Indeed, we have

𝔖_{2} = \begin{aligned}& & & & (⊤, ⊤) \\ & & & (⊤, +) & & (+, ⊤) \\ & & (⊤, ⊥) & & (+, +) & & (⊥, ⊤) \\ ⊤ & ← & (+, ⊥) & (⊥, +) & ⊤ & → \\ + & ← & (⊥, ⊥) & + & → \\ ⊥ & ← & ⊥ & → & . \end{aligned}

In the rest of the section we will only be concerned with the instance of Axiom 3 for n = 0; the case for general n will play a crucial rôle in the following section when internalising finite chains. Note that, as × A preserves colimits (by Assumption 3), it follows that the commuting square

1 × A  ⊥ × A  Σ × A ⊤ × A  η_{Σ} × A Σ × A L⊥ × A  Σ_{2} × A  (1)

is a pushout.

Convention. For a pushout

· A  B C

and a cone A ⟶^{f} D ⟵^{g} B for it, we write [f, g] for the unique mediating morphism C → D given by the universal property.

Remark. For a cone Σ × A ⟶^{α} B ⟵^{β} Σ × A for (1), we have λ([α, β]) = [λ(α), λ(β)].

Proposition 5.10. (Transitivity) If α : f g : A → B and β : g h : A → B then [α, β] ∘ (L⊤ × A) : f h : A → B.

Proof. As [α, β]∘(L⊤×A)∘(⊤×A) = [α, β] ∘ (η_{Σ} × A) ∘ (⊤ × A) = β∘(⊤×A) = h∘π_{2} and [α, β] ∘ (L⊤ × A) ∘ (⊥ × A) = [α, β] ∘ (L⊥ × A) ∘ (⊥ × A) = α ∘ (⊥ × A) = f ∘ π_{2}.

As a corollary we have:

Theorem 5.11. The category C equipped with ⊑ (henceforth denoted C_{⊑}) is a Preocartesian-closed-category and L determines a Preo-endofunctor on it.

Proof. By Propositions 5.6 (1) and 5.10, the path relation gives a preorder on each homset. And, by Proposition 5.6 (2), the composition of morphisms is a monotone operation with respect to the path preorder. Finally, by Proposition 5.6 (5–6), the cartesian closed structure Preo-enriches. L determines a Preo-endofunctor by Proposition 5.6 (4).

It follows that 𝕃 is a Preo-monad and hence:

Corollary 5.12. C^{𝕃} and C_{𝕃} Preo-enrich with respect to ⊑.

6. Canonical upper bounds of ω-chains

First, using Axiom 3, to every ω-chain \overline{f} = ⟨f_{n} f_{n+1}⟩ in C_{⊑}(A, B) we associate maps Σ_{n} × A → B (n ≥ 0) internalising the finite chains ⟨f_{0} … f_{n}⟩ (see Definition 6.1); then, using Axiom 1, we internalise the whole ω-chain \overline{f} (see Definition 6.2); and finally, using Axiom 2, we extract its value at infinity. This process defines a passage-to-the-limit operator V yielding canonical upper bounds for ω-chains of approximations. Various algebraic properties of V are established.

Definition 6.1. For an ω-chain \overline{f} = ⟨α_{n} : f_{n} f_{n+1}⟩ in C_{⊑}(A, B) we inductively define, for n ≥ 0, [\overline{f}]_{n} : Σ_{n} ×A → B satisfying [\overline{f}]_{n} ∘(η_{1}^{(n)} ×A) = α_{n} ∘(⊥×A) as follows:

— [\overline{f}]_{0} = (1 × A ≅ A ⟶^{f_{0}} B) and [\overline{f}]_{0} ∘ (η_{1}^{(0)} × A) = (1 × A ≅ A ⟶^{f_{0}} B) = α_{0} ∘ (⊥ × A).

— [\overline{f}]_{n+1} = [[\overline{f}]_{n}, α_{n}] : (Σ_{n+1} × A) → B (that is,

α_{n}) Σ × A B Σ_{n+1} × A [\overline{f}]_{n+1} η_{Σ}^{(n)} × A L^{n}⊥ × A 1 × A η_{1}^{(n)} × A Σ_{n} × A  ⊥ × A [\overline{f}]_{n}

and [\overline{f}]_{n+1} ∘ (η_{1}^{(n+1)} × A) = [\overline{f}]_{n+1} ∘ (η_{Σ}^{(n)} × A) ∘ (⊤ × A) = α_{n} ∘ (⊤ × A) =

(1 × A ≅ A ⟶^{f_{n+1}} B) = α_{n+1} ∘ (⊥ × A).

We have constructed ⟨[\overline{f}]_{n}⟩ so that it is a cone for ⟨L^{n}(⊥) × A : Σ_{n} × A → Σ_{n+1} × A⟩. This together with the requirement that \overline{ω} be constructed as a colimit allows us to internalise \overline{f}:

Definition 6.2. For every ω-chain \overline{f} in C_{⊑}(A, B) we define, [\overline{f}] : \overline{ω} × A → B as the unique mediating morphism from ⟨s_{n} × A⟩ to ⟨[\overline{f}]_{n}⟩.

Example 6.3. Let f : A → B. Writing ⟨f⟩ for the constantly f ω-chain ⟨f ^{id_{f}}

f ^{id_{f}} …⟩ in C_{⊑}(A, B), for n ≥ 0, [⟨f⟩]_{n} = (Σ_{n} × A ⟶^{π_{2}} A ⟶^{f} B) and hence

[⟨f⟩] = (\overline{ω} × A ⟶^{π_{2}} A ⟶^{f} B).

Example 6.4. Let \overline{c} be the ω-chain ⟨s_{n+1} ∘ η_{Σ}^{(n)} : \underline{n} \underline{n + 1}⟩ in C_{⊑}(1, \overline{ω}). Then, for every n ≥ 0, [\overline{c}]_{n} = s_{n} (because, by induction, the case n = 0 reduces to the equality [\overline{c}]_{0} = s_{0} ∘ η_{1}^{(0)} = s_{0}; and for the case n = m + 1 (m ≥ 0) we have that

[\overline{c}]_{m+1} = [[\overline{c}]_{m}, s_{m+1} ∘ η_{Σ}^{(m)}]
= [s_{m}, s_{m+1} ∘ η_{Σ}^{(m)}]  , by induction
= [s_{m+1} ∘ L^{m}⊥, s_{m+1} ∘ η_{Σ}^{(m)}]
= s_{m+1} ∘ [L^{m}⊥, η_{Σ}^{(m)}]
= s_{m+1}  , by Axiom 3)

and hence [\overline{c}] = id\overline{ω}.

Example 6.5. For every endomorphism f on a pointed object X,

it(f) = [⟨f^{n} ∘ ρ_{X} ∘ L(f ∘ ⊥_{X}) : f^{n} ∘ ⊥_{X} f^{n+1} ∘ ⊥_{X}⟩].

Because

it(f) = [⟨it_{n+1}(f) ∘ η_{Σ}^{(n)} : it_{n}(f) ∘ \underline{n}_{Σ_{n}} it_{n+1}(f) ∘ \underline{n + 1}_{Σ_{n+1}}⟩],
it_{n+1}(f) ∘ η_{Σ}^{(n)} = f^{n} ∘ ρ_{X} ∘ L(f ∘ ⊥_{X}),
it_{n}(f) ∘ \underline{n}_{Σ_{n}} = f^{n} ∘ ⊥_{X}.

We introduce the passage-to-the-limit operator: Definition 6.6. (V) For an ω-chain \overline{f} in C_{⊑}(A, B), define V\overline{f} : A → B as the composite

A ≅ 1 × A ⟶^{∞×A} \overline{ω} × A ⟶^{[\overline{f}]} B.

Example 6.7. (Constant) Let f : A → B. Writing ⟨f⟩ for the constantly f ω-chain ⟨f ^{id_{f}} f ^{id_{f}} …⟩ in C_{⊑}(A, B), it follows that V⟨f⟩ = f (see Example 6.3). Example 6.8. For every endomorphism f on a pointed object X,

fix(f) = V⟨f^{n} ∘ ρ_{X} ∘ L(f ∘ ⊥_{X}) : f^{n} ∘ ⊥_{X} f^{n+1} ∘ ⊥_{X}⟩.

We have internalised arbitrary ω-chains; however, as we show below, it is enough to consider ω-chains of global elements. Definition 6.9. For an ω-chain \overline{f} = ⟨α_{n} : f_{n} f_{n+1}⟩ in C_{⊑}(A, B), let ⌜\overline{f}⌝ be the ω-chain ⟨λ(α_{n}) : ⌜f_{n}⌝ ⌜f_{n+1}⌝⟩ in C_{⊑}(1, B^{A}). Proposition 6.10. Let \overline{f} = ⟨α_{n} : f_{n} f_{n+1}⟩ be an ω-chain in C_{⊑}(A, B). For n ≥ 0, λ([\overline{f}]_{n}) = [⌜\overline{f}⌝]_{n} : Σ_{n} → B^{A} and hence λ[\overline{f}] = [⌜\overline{f}⌝] : \overline{ω} → B^{A}.

Again, in order to discuss the properties of the V operator it is enough to restrict attention to ω-chains of global elements: Proposition 6.11. For every ω-chain \overline{f} in C_{⊑}(A, B), ⌜V\overline{f}⌝ = V⌜\overline{f}⌝ : 1 → B^{A}.

The operator V provides canonical upper-bounds for ω-chains: Proposition 6.12. (Canonical Upper Bounds) Let \overline{c} = ⟨c_{n}⟩ be an ω-chain in C_{⊑}(1, C). Then, [\overline{c}] ∘ ∞_{n} : c_{n} V\overline{c} : 1 → C.

Proof. Note that ∞_{n} has been defined in Example 5.3 (3). We have that [\overline{c}] ∘ ∞_{n} ∘ ⊥ = c_{n} because

⊥ 1  Σ_{n} Σ_{n+1} η_{Σ}^{(n)}  L^{n}(L\overline{ω}) L^{n}(⊥_{L\overline{ω}})  L^{n}\overline{ω} ⋯ L\overline{ω}  \overline{ω} C[\overline{c}] σ L^{n}σ [\overline{c}]_{n} c_{n} L^{n}⊥ Σ  L^{n}(L∞)  . η_{1}^{(n)}

Moreover,

[\overline{c}] ∘ ∞_{n} ∘ ⊤ = [\overline{c}] ∘ σ ∘ … ∘ (L^{n}σ) ∘ (L^{n+1}∞) ∘ η_{Σ}^{(n)} ∘ ⊤
= [\overline{c}] ∘ σ ∘ … ∘ (L^{n}σ) ∘ (L^{n+1}∞) ∘ η_{1}^{(n+1)}
= [\overline{c}] ∘ σ ∘ … ∘ (L^{n}σ) ∘ η(n+1) ; \overline{ω} ∘ ∞
= [\overline{c}] ∘ ∞  , by the invariance of ∞.

Canonical upper bounds are preserved by composition: Lemma 6.13. 1 Let \overline{a} = ⟨α_{n} : a_{n} a_{n+1}⟩ be an ω-chain in C_{⊑}(1, A) and let \overline{b} = ⟨β_{n} : b_{n} b_{n+1}⟩ be

an ω-chain in C_{⊑}(1, B).

Given m : B × A → C, let \overline{c} be the ω-chain

⟨m ∘ ⟨β_{n}, α_{n}⟩ : m ∘ ⟨b_{n}, a_{n}⟩ m ∘ ⟨b_{n+1}, a_{n+1}⟩⟩

in C_{⊑}(1, C).

Then, [\overline{c}] = m ∘ ⟨[\overline{b}], [\overline{a}]⟩. 2 (Continuity of composition) Let \overline{f} = ⟨α_{n} : f_{n} f_{n+1}⟩ and \overline{g} = ⟨β_{n} : g_{n} g_{n+1}⟩

be ω-chains in C_{⊑}(A, B) and C_{⊑}(B, C) respectively.

For \overline{h} = ⟨β_{n} ⋆ α_{n} : g_{n} ∘ f_{n} g_{n+1} ∘ f_{n+1}⟩, (V\overline{g}) ∘ (V\overline{f}) = V\overline{h}.

Proof.

(1) It is enough to show that [\overline{c}]_{i} = m ∘ ⟨[\overline{b}]_{i}, [\overline{a}]_{i}⟩ for every i ≥ 0. We proceed by induction on i. The case i = 0 reduces to \overline{c}_{0} = m ∘ ⟨b_{0}, a_{0}⟩. For the case i = j + 1 (j ≥ 0) we calculate:

[\overline{c}]_{j+1} = [[\overline{c}]_{j}, m ∘ ⟨β_{j}, α_{j}⟩]  , by Definition 6.1
= [m ∘ ⟨[\overline{b}]_{j}, [\overline{a}]_{j}⟩, m ∘ ⟨β_{j}, α_{j}⟩] , by induction
= m ∘ [⟨[\overline{b}]_{j}, [\overline{a}]_{j}⟩, ⟨β_{j}, α_{j}⟩]
= m ∘ ⟨[[\overline{b}]_{j}, β_{j}], [[\overline{a}]_{j}, α_{j}]⟩
= m ∘ ⟨[\overline{b}]_{j+1}, [\overline{a}]_{j+1}⟩.

(2) Let M : C^{B} × B^{A} → C^{A} be the exponential transpose of

(C^{B} × B^{A}) × A ≅ C^{B} × (B^{A} × A) ⟶^{C^{B} × e} C^{B} × B ⟶^{e} C.

Then,

⌜(V\overline{g}) ∘ (V\overline{f})⌝ = M ∘ ⟨⌜V\overline{g}⌝, ⌜V\overline{f}⌝⟩
= M ∘ ⟨[⌜\overline{g}⌝] ∘ ∞, [⌜\overline{f}⌝] ∘ ∞⟩
= M ∘ ⟨[⌜\overline{g}⌝], [⌜\overline{f}⌝]⟩ ∘ ∞
= [⌜\overline{h}⌝] ∘ ∞  , by Lemma 6.13 (1)
= ⌜V\overline{h}⌝.

The operator V is invariant under shifting ω-chains: Convention. For an ω-chain \overline{f} = ⟨α_{n} : f_{n} f_{n+1}⟩ in C_{⊑}(A, B) we write \overline{f}^{+} for the ω-chain ⟨α_{n+1} : f_{n+1} f_{n+2}⟩ in C_{⊑}(A, B). Proposition 6.14. For an ω-chain \overline{c} in C_{⊑}(1, X), 1 [\overline{c}^{+}] = [\overline{c}] ∘ succ, and 2 (Shift) V\overline{c}^{+} = V\overline{c}.

Proof.

(1) First we show by induction that for n ≥ 0, [\overline{c}^{+}]_{n} = [\overline{c}]_{n+1} ∘ η_{Σ_{n}}. Let \overline{c} = ⟨α_{n} : x_{n} x_{n+1}⟩. The case n = 0 reduces to the equality [\overline{c}^{+}]_{0} = x_{1} = [\overline{c}]_{1} ∘ ⊤. For the case n = m + 1 (m ≥ 0), by Definition 6.1, we have that [\overline{c}^{+}]_{m+1} = [\overline{c}]_{m+2} ∘ η_{Σ_{m+1}} if and only if

[\overline{c}^{+}]_{m} = [\overline{c}]_{m+2} ∘ η_{Σ_{m+1}} ∘ L^{m}⊥  (2)

and

α_{m+1} = [\overline{c}]_{m+2} ∘ η_{Σ_{m+1}} ∘ η_{Σ}^{(m)}.  (3)

And (2) holds because

[\overline{c}^{+}]_{m} = [\overline{c}]_{m+1} ∘ η_{Σ_{m}} = [\overline{c}]_{m+2} ∘ L^{m+1}⊥ ∘ η_{Σ_{m}} = [\overline{c}]_{m+2} ∘ η_{Σ_{m+1}} ∘ L^{m}⊥

whilst (3) holds because

α_{m+1} = [\overline{c}]_{m+2} ∘ η_{Σ}^{(m+1)} = [\overline{c}]_{m+2} ∘ η_{Σ_{m+1}} ∘ η_{Σ}^{(m)}.

The result follows as, for n ≥ 0, [\overline{c}^{+}]_{n} = [\overline{c}]∘s_{n+1}∘η_{Σ_{n}} = [\overline{c}]∘σ∘L(s_{n})∘η_{Σ_{n}} = [\overline{c}]∘succ∘s_{n}.

(2) V\overline{c}^{+} = [\overline{c}^{+}] ∘ ∞ = [\overline{c}] ∘ succ ∘ ∞ = [\overline{c}] ∘ ∞ = V\overline{c}.

Remark. It is interesting to note that from the characterisation of fix in Example 6.8, using (Constant), (Shift) and the fact that canonical upper bounds are preserved by composition, the usual algebraic argument for showing that fix is a fixed-point operator can be reproduced. That is, for every endomorphism f on a pointed object X,

f ∘ fix(f) = V⟨id_{f} : f f⟩_{n} ∘ V⟨f^{n} ∘ ρ_{X} ∘ L(f ∘ ⊥_{X}) : f^{n} ∘ ⊥_{X} f^{n+1} ∘ ⊥_{X}⟩_{n}

, by (Constant) and Example 6.8

= V⟨f^{n+1} ∘ ρ_{X} ∘ L(f ∘ ⊥_{X}) : f^{n+1} ∘ ⊥_{X} f^{n+2} ∘ ⊥_{X}⟩_{n}

, by continuity of composition

= fix(f)

, by (Shift) and Example 6.8.

Canonical upper bounds are preserved by L: Lemma 6.15. Let \overline{f} = ⟨α_{n} : f_{n} f_{n+1}⟩ be an ω-chain in C_{⊑}(A, B), and write L\overline{f} for the ω-chain ⟨L(α_{n}) ∘ t′ : Lf_{n} Lf_{n+1}⟩ in C_{⊑}(LA, LB). We have that 1 [L\overline{f}] = (L[\overline{f}]) ∘ t′, and 2 (Continuity of L) L(V\overline{f}) = V(L\overline{f}).

Proof.

(1) Observe that [L\overline{f}] = (L[\overline{f}]) ∘ t′ if and only if, for n ≥ 0,

[L\overline{f}]_{n} = (L[\overline{f}]) ∘ t′ ∘ (s_{n} × LA)
= (L[\overline{f}]) ∘ L(s_{n} × A) ∘ t′
= L([\overline{f}]_{n}) ∘ t′.  (4)

We show (4) by induction on n. The case n = 0 reduces to the equality [L\overline{f}]_{0} = L(α_{0}) ∘ t′ = L([\overline{f}]_{0}) ∘ t′. For the case n = m + 1 (m ≥ 0), by Definition 6.1, we have that [L\overline{f}]_{m+1} = L([\overline{f}]_{m+1}) ∘ t′ if and only if

L([\overline{f}]_{m+1}) ∘ t′ ∘ (η_{Σ}^{(m)} × LA) = L(α_{m}) ∘ t′  (5)

and

L([\overline{f}]_{m+1}) ∘ t′ ∘ (L^{m}⊥ × LA) = [L\overline{f}]_{m}.  (6)

And (5) holds because

L([\overline{f}]_{m+1}) ∘ t′ ∘ (η_{Σ}^{(m)} × LA) = L([\overline{f}]_{m+1}) ∘ L(η_{Σ}^{(m)} × A) ∘ t′
= L(α_{m}) ∘ t′  , by Definition 6.1

whilst (6) holds because

L([\overline{f}]_{m+1}) ∘ t′ ∘ (L^{m}⊥ × LA) = L([\overline{f}]_{m+1}) ∘ L(L^{m}⊥ × A) ∘ t′
= L([\overline{f}]_{m}) ∘ t′  , by Definition 6.1
= [L\overline{f}]_{m}  , by induction.

(2) Follows from Lemma 6.15 (1).

7. Unique proofs

We take a first step towards externalising Σ by identifying proofs of approximation between maps. As a consequence we are able to: show that colimits order-enrich (Proposition 7.3), and explore further algebraic properties of V and fix. Surprisingly, it follows that the path preorder is antisymmetric. Proposition 7.1. The following are equivalent: 1 (Unique proofs) If α, β : f g : 1 → C then α = β. 2 1 ∘⟶^{⊥} Σ ⟵^{⊤} 1 are jointly epi. 3 The map

C(A, B^{Σ}) → Preo(2, C_{⊑}(A, B))
α ↦ e ∘ ⟨α, ⊥ ∘ (A → 1)⟩ ⊑ e ∘ ⟨α, ⊤ ∘ (A → 1)⟩

is a bijection.

Axiom 4. (Unique proofs) 1 ∘⟶^{⊥} Σ ⟵^{⊤} 1 are jointly epi. Convention. For f ⊑ g : A → B, we set [f ⊑ g] : f g.

Corollary 7.2. The map

C(A, B\overline{ω}) → Preo(ω, C_{⊑}(A, B)) : α ↦ ⟨e ∘ ⟨α, \underline{n}\overline{ω} ∘ (A → 1)⟩⟩_{n∈|ω|}

is a bijection.

Axiom 4 forces and ⊑ to coincide. More importantly, it allows us to conclude: Proposition 7.3. Colimits in C Preo-enrich.

Proof. Let Δ : G → C and let ⨿ : Δ \underrightarrow{.} C be colimiting in C. For f, g : C → D, we show that if f ∘ ⨿ ⊑ g ∘ ⨿ : Δ \underrightarrow{.} D then f ⊑ g : C → D. Assume f ∘ ⨿ ⊑ g ∘ ⨿ : Δ \underrightarrow{.} D. For every e : M → N in G, we have that

[f ∘ ⨿_{N} ⊑ g ∘ ⨿_{N}] ∘ (Σ × Δe) ∘ (⊥ × ΔM) = f ∘ ⨿_{N} ∘ π_{2} ∘ (1 × Δe)
= f ∘ ⨿_{N} ∘ Δe ∘ π_{2}
= f ∘ ⨿_{M} ∘ π_{2}

and

[f ∘ ⨿_{N} ⊑ g ∘ ⨿_{N}] ∘ (Σ × Δe) ∘ (⊤ × ΔM) = g ∘ ⨿_{N} ∘ π_{2} ∘ (1 × Δe)
= g ∘ ⨿_{N} ∘ Δe ∘ π_{2}
= g ∘ ⨿_{M} ∘ π_{2}.

Thus, by the unique-proofs axiom, [f ∘ ⨿_{N} ⊑ g ∘ ⨿_{N}] ∘ (Σ × Δe) = [f ∘ ⨿_{M} ⊑ g ∘ ⨿_{M}] and so Γ =^{def} ⟨[f ∘ ⨿_{M} ⊑ g ∘ ⨿_{M}]⟩_{M} is a cone Σ × Δ \underrightarrow{.} D. As Σ × preserves colimits, it follows that Σ × ⨿ : Σ × Δ \underrightarrow{.} Σ × C is colimiting. Then, for α : Σ × C → D the unique mediating morphism between Σ × ⨿ and Γ we have that α : f g as 1 × ⨿ is colimiting, and α ∘ (⊥ × C) ∘ (1 × ⨿) = f ∘ π_{2} ∘ (1 × ⨿) and α ∘ (⊤ × C) ∘ (1 × ⨿) = g ∘ π_{2} ∘ (1 × ⨿).

Typical applications of the above proposition (see Corollary 8.3) are given in the corollary below. Convention. For f ⊑ g ⊑ h : A → B we write [f ⊑ g ⊑ h] for the unique mediating

morphism [[f ⊑ g], [g ⊑ h]] : Σ_{2}×A → X from (1) to the cone Σ×A ⟶^{[f⊑g]} X ⟵^{[g⊑h]} Σ×A. Corollary 7.4. 1 For x ⊑ y ⊑ z and x′ ⊑ y′ ⊑ z′ in C_{⊑}(1, C), if [x ⊑ y] ⊑ [x′ ⊑ y′] and [y ⊑ z] ⊑ [y′ ⊑

z′] in C_{⊑}(Σ, C) then [x ⊑ y ⊑ z] ⊑ [x′ ⊑ y′ ⊑ z′] : Σ_{2} → C. 2 For ω-chains \overline{f} and \overline{g} in C_{⊑}(A, B), if [\overline{f}]_{n} ⊑ [\overline{g}]_{n} : Σ_{n} × A → B (n ≥ 0) then

[\overline{f}] ⊑ [\overline{g}] : \overline{ω} × A → B.

In addition to (Constant) and (Shift), further algebraic properties of V, needed to establish the antisymmetry of the path preorder, are studied below. Proposition 7.5. Let ⟨f_{n}⟩ be an ω-chain in C_{⊑}(\overline{ω}, C). Then,

[⟨f_{n}⟩] ∘ ⟨∞, ∞⟩ = [⟨f_{n} ∘ ∞⟩] ∘ ∞.

Proof.

[⟨f_{n}⟩] ∘ ⟨∞, ∞⟩ = (1 ⟶^{∞} \overline{ω} ≅ 1 × \overline{ω} ⟶^{∞×\overline{ω}} \overline{ω} × \overline{ω} ⟶^{[⟨f_{n}⟩]} C) = (V⟨f_{n}⟩) ∘ ∞
= (V⟨f_{n}⟩) ∘ (V⟨∞⟩)  = V⟨f_{n} ∘ ∞⟩
= [⟨f_{n} ∘ ∞⟩] ∘ ∞.

Corollary 7.6. For n, m ≥ 0 let c_{n,m} : 1 → C be such that ⟨c_{n,m}⟩_{m} is an ω-chain in C_{⊑}(1, C) and [c_{n,m} ⊑ c_{n,m+1}] ⊑ [c_{n+1,m} ⊑ c_{n+1,m+1}] : Σ → C. Then, 1 (Interchange) ⟨c_{n,m}⟩_{n}, ⟨V⟨c_{n,m}⟩_{m}⟩_{n} and ⟨V⟨c_{n,m}⟩_{n}⟩_{m} are ω-chains in C_{⊑}(1, C),

and V⟨V⟨c_{n,m}⟩_{m}⟩_{n} = V⟨V⟨c_{n,m}⟩_{n}⟩_{m}. 2 (Diagonal) ⟨c_{m,m}⟩_{m} is an ω-chain in C_{⊑}(1, C), and V⟨V⟨c_{n,m}⟩_{m}⟩_{n} = V⟨c_{m,m}⟩_{m}.

Proof.

(1) Observe that

[⟨[⟨c_{n,m}⟩_{m}]⟩_{n}] = [⟨[⟨c_{n,m}⟩_{n}]⟩_{m}] ∘ ⟨π_{2}, π_{1}⟩  (7)

because for i, j ≥ 0,

[⟨[⟨c_{n,m}⟩_{m}]⟩_{n}] ∘ ⟨\underline{i}, \underline{j}⟩ = [⟨[⟨c_{n,m}⟩_{m}]⟩_{n}] ∘ (\underline{i} × \overline{ω}) ∘ ⟨1, \underline{j}⟩ = [⟨c_{i,m}⟩_{m}] ∘ \underline{j}
= c_{i,j}  = [⟨c_{n,j}⟩_{n}] ∘ \underline{i}
= [⟨[⟨c_{n,m}⟩_{n}]⟩_{m}] ∘ (\underline{j} × \overline{ω}) ∘ ⟨1, \underline{i}⟩ = [⟨[⟨c_{n,m}⟩_{n}]⟩_{m}] ∘ ⟨\underline{j}, \underline{i}⟩.
= [⟨[⟨c_{n,m}⟩_{n}]⟩_{m}] ∘ ⟨π_{2}, π_{1}⟩ ∘ ⟨\underline{i}, \underline{j}⟩.

Then,

V⟨V⟨c_{n,m}⟩_{m}⟩_{n} = [⟨[⟨c_{n,m}⟩_{m}] ∘ ∞⟩_{n}] ∘ ∞
= [⟨[⟨c_{n,m}⟩_{m}]⟩_{n}] ∘ ⟨∞, ∞⟩  , by Proposition 7.5
= [⟨[⟨c_{n,m}⟩_{n}]⟩_{m}] ∘ ⟨π_{2}, π_{1}⟩ ∘ ⟨∞, ∞⟩ , by (7)
= [⟨[⟨c_{n,m}⟩_{n}]⟩_{m}] ∘ ⟨∞, ∞⟩
= [⟨[⟨c_{n,m}⟩_{n}] ∘ ∞⟩_{m}] ∘ ∞  , by Proposition 7.5
= V⟨V⟨c_{n,m}⟩_{n}⟩_{m}.

(2) Let

c′_{n,m} = \{ \begin{matrix}c_{m,m} & , if 0 ≤ m ≤ n \\ c_{n,m} & , if m > n ≥ 0 \end{matrix}

Then,

V⟨V⟨c_{n,m}⟩_{m}⟩_{n} = V⟨V⟨c′_{n,m}⟩_{m}⟩_{n} , by (Shift)
= V⟨V⟨c′_{n,m}⟩_{n}⟩_{m} , by (Interchange)
= V⟨c_{m,m}⟩_{m}  , by (Shift) and (Constant).

Corollary 7.7. 1 (Finality) Let \overline{a} = ⟨a_{n}⟩ and \overline{b} = ⟨b_{n}⟩ be ω-chains in C_{⊑}(1, C) such that ∀ n.∃ m.a_{n} ⊑

b_{m} and ∀ m. ∃ n. b_{m} ⊑ a_{n}. Then, V\overline{a} = V\overline{b}.

2 (Dinaturality) Let X and Y be pointed objects. For f : X → Y and g : Y → X, fix(f ∘ g) = f ∘ fix(g ∘ f). Proof.

(1) It suffices to show that for every ω-chain ⟨c_{n}⟩ in C_{⊑}(1, C) and every unbounded monotone endofunction f on ω, V⟨c_{n}⟩ = V⟨c_{f(n)}⟩. Let c′_{n,m} = c_{min(f(n),m)}. Then, for n ≥ 0,

⟨c′_{n,m}⟩ = ⟨c_{0}, …, c_{f(n)−1}, c_{f(n)}, …, c_{f(n)}, …⟩

and

V⟨c′_{n,m}⟩_{m} = V⟨c_{f(n)}⟩_{m} , by (Shift)
= c_{f(n)}  , by (Constant).

Finally, since [c′_{n,m} ⊑ c′_{n,m+1}] ⊑ [c′_{n+1,m} ⊑ c′_{n+1,m+1}] (by construction, using Proposition 5.6 (1) and the fact that x ⊑ y ⊑ z implies [x ⊑ x] ⊑ [y ⊑ z]) it follows that

V⟨c_{m}⟩_{m} = V⟨c′_{m,m}⟩_{m}
= V⟨V⟨c′_{n,m}⟩_{m}⟩_{n} , by (Diagonal)
= V⟨c_{f(n)}⟩_{n}.

(2) By (Finality) using the characterisation of fix in Example 6.8.

As a surprising consequence we have: Theorem 7.8. C_{⊑} is Poset-cartesian-closed.

Proof. By Theorem 5.11 we need only show that the path preorder is antisymmetric. Assuming f ⊑ g ⊑ f : A → B, by (Finality) we have that V⟨f⟩ = V⟨g⟩ and, by (Constant), we are done.

8. Least upper bounds of ω-chains

We introduce Axiom 5 which together with Axiom 4 make Σ and \overline{ω} behave externally as 2 and ω respectively (see Proposition 8.1 (3) and Corollary 8.3). We are thus in position to establish the enrichment theorem. Proposition 8.1. The following are equivalent: 1 (Interpolation Property) The commuting square

⟨μ_{1}, L(Σ → 1)⟩ Σ_{2}  Σ × Σ Σ_{2} L⊤ Σ L⊤  ⟨L(Σ → 1), μ^{1}⟩  (8)

is a pushout.

Remark. The maps in the above diagram can be better understood as the proofs L⊤ = [\underline{0} ⊑ \underline{2}], ⟨μ_{1}, L(Σ → 1)⟩ = [⟨⊥, ⊥⟩ ⊑ ⟨⊥, ⊤⟩ ⊑ ⟨⊤, ⊤⟩], and ⟨L(Σ → 1), μ_{1}⟩ = [⟨⊥, ⊥⟩ ⊑ ⟨⊤, ⊥⟩ ⊑ ⟨⊤, ⊤⟩].

2 (Diamond property) If

x′  y x y′  (9)

in C_{⊑}(1, C) then [x ⊑ x′] ⊑ [y ⊑ y′] : Σ → C. 3 (C_{⊑} has Poset-cotensors with 2) The monotone map

C_{⊑}(A, B^{Σ}) → Poset_{⊑}(2, C_{⊑}(A, B))
α ↦ e ∘ ⟨α, ⊥ ∘ (A → 1)⟩ ⊑ e ∘ ⟨α, ⊤ ∘ (A → 1)⟩

is an isomorphism of preorders. 4 (Tay94) (Σ, ⊑_{Σ}) where ⊑_{Σ} =^{def} ⟨Σ^{⊥}, Σ^{⊤}⟩ : Σ^{Σ} ↣ Σ × Σ is a distributive lattice for

which ⊥ and ⊤ are respectively the least and greatest elements. Axiom 5. The commuting square (8) is a pushout. Lemma 8.2. For ω-chains \overline{f} = ⟨f_{n}⟩ and \overline{g} = ⟨g_{n}⟩ in C_{⊑}(A, B),

∀ n ≥ 0. f_{n} ⊑ g_{n} : A → B implies [\overline{f}] ⊑ [\overline{g}] : \overline{ω} × A → B.  (10)

Proof. Assuming the antecedent of (10), it follows by induction on n (using Axiom 5 and Proposition 7.3 —see Corollary 7.4 (1)) that [\overline{f}]_{n} ⊑ [\overline{g}]_{n} (n ≥ 0), and hence [\overline{f}] ⊑ [\overline{g}] (by Corollary 7.4 (2)). Corollary 8.3. 1 (C_{⊑} has Poset-cotensors with ω) The monotone map

ext : C_{⊑}(A, B\overline{ω}) → Poset_{⊑}(ω, C_{⊑}(A, B)) : α ↦ ⟨e ∘ ⟨α, \underline{n}\overline{ω} ∘ (A → 1)⟩⟩_{n∈|ω|}

is an isomorphism of preorders. 2 (Monotonicity of V) The passage-to-the-limit operator V is monotone.

Proof.

(1) By Corollary 7.2 and Lemma 8.2.

(2) By Lemma 8.2 because composition is monotone.

At this stage, it is possible to give a direct proof that the passage-to-the-limit operator computes lubs: let ⟨f_{n}⟩ be an ω-chain, then

— for i ≥ 0,

f_{i} = V⟨f_{i}⟩_{n}  , by (Constant)
⊑ V⟨f_{i+n}⟩_{n} , by monotonicity of V
= V⟨f_{n}⟩_{n} , by (Shift);

— for f_{n} ⊑ f (n ≥ 0),

V⟨f_{n}⟩ ⊑ V⟨f⟩ , by monotonicity of V
= f  , by (Constant).

However, our axiomatisation yields a stronger result, viz. that the objects of C_{⊑} are internally complete (in the sense of Lemma 8.4); and from this, externalising via the Yoneda embedding, we will give another proof of the enrichment theorem. We have decided to proceed in this way to explore the consequences of the axioms and to show that they provide insight in understanding domains. Indeed, the internal-completeness property, which holds in Cpo but fails in Cpo_{∧}, exhibits a crucial difference between continuity and stability. Lemma 8.4. (Internal completeness) For every C ∈ | C_{⊑} |, we have the following adjoint situation C^{∞} ⊣ λ(C × \overline{ω} ⟶^{π_{1}} C) : C → C\overline{ω} in C_{⊑}.

Proof. The diagram

λ(π_{1}) × 1 C × \overline{ω}  C π_{1}  C\overline{ω} × \overline{ω}C\overline{ω} × 1 C × ∞  C\overline{ω} × ∞ C\overline{ω} C × 1 π_{1}C  λ(π_{1})  ≅ ≅  λ(π_{1}) × \overline{ω} e  C^{∞}

shows that C^{∞} ∘ λ(π_{1}) = C. Finally we need show that C\overline{ω} ⊑ λ(π_{1}) ∘ C^{∞}; or equivalently that

(C\overline{ω} × \overline{ω} ⟶^{e} C) ⊑ (C\overline{ω} × \overline{ω} ⟶^{π_{1}} C\overline{ω} ⟶^{C^{∞}} C);

or equivalently, as C\overline{ω} × preserves Poset-colimits, that for n ≥ 0,

(C\overline{ω} × Σ_{n} ⟶^{C\overline{ω}×s_{n}} C\overline{ω} × \overline{ω} ⟶^{e} C)

⊑ (C\overline{ω} × Σ_{n} ⟶^{C\overline{ω}×s_{n}} C\overline{ω} × \overline{ω} ⟶^{π_{1}} C\overline{ω} ⟶^{C^{∞}} C)
= (C\overline{ω} × Σ_{n} ⟶^{C\overline{ω}×(∞∘(Σ_{n}→1))} C\overline{ω} × \overline{ω} ⟶^{e} C).

Since

s_{n} = [⟨\underline{i}⟩_{i}]_{n}  , by Example 6.4
⊑ [⟨∞⟩]_{n}  , by Corollary 8.3 (1) and Example 5.3 (3)
= ∞ ∘ (Σ_{n} → 1) , by Example 6.3

we are done.

Theorem 8.5. (Enrichment theorem) The Poset-category C_{⊑} is Cpo-cartesian-closed, and L determines a Cpo-endofunctor on it.

Proof. As for every A ∈ | C |, C_{⊑}(A, ) : C_{⊑} → Poset_{⊑} preserves adjunctions (as it is a Poset-functor) we have, by Lemma 8.4 and Corollary 8.3 (1), the following adjoint situation:

B^{∞} ∘ λ(π^{1}) ∘ C_{⊑}(A, B)  C_{⊑}(A, B\overline{ω}) ≅ Poset_{⊑}(ω, C_{⊑}(A, B)) ; ext

and since ext(λ(π_{1}) ∘ ) : f ↦ ⟨f⟩, it follows that every hom-poset is ω-complete. Composition is continuous by Proposition 5.6 (2) and Lemma 6.13. L determines a Cpo-functor by Theorem 5.11 and Lemma 6.15 (2).

It follows that 𝕃 is a Cpo-monad and hence: Corollary 8.6. C^{𝕃} and C_{𝕃} Cpo-enrich with respect to ⊑.

9. Domain-theoretic categories

A category satisfying Assumptions 1–3 in which Axioms 1–5 hold is said to be domain theoretic.

In domain-theoretic categories, \overline{ω} complies Freyd’s axiomatisation (Fre91): Lemma 9.1. In a domain-theoretic category, σ : L\overline{ω} → \overline{ω} is a free L-algebra (i.e. an initial L-algebra whose inverse is a final L-coalgebra —see (Fre91)), and hence ∞ : 1 → \overline{ω} is the unique coalgebra homomorphism (1, ⊤) → (\overline{ω}, σ^{−1}).

Proof. Since ⟨L^{n}⊥ : Σ_{n} → Σ_{n+1}⟩ is an ω-chain of embeddings (because ⊥ : 1 → Σ is an embedding and L is a Cpo-functor) with colimiting cone ⟨s_{n}⟩ : ⟨L^{n}⊥ : Σ_{n} → Σ_{n+1}⟩ \underrightarrow{.} \overline{ω}, by the limit/colimit-coincidence theorem (SP82), it follows that the cone ⟨Ls_{n}⟩ : ⟨L^{n+1}⊥ : Σ_{n+1} → Σ_{n+2}⟩ \underrightarrow{.} L\overline{ω} is colimiting because L is a Cpo-functor. As σ : L\overline{ω} → \overline{ω} is the unique mediating morphism ⟨Ls_{n}⟩ → ⟨s_{n+1}⟩, it is an isomorphism and hence and initial L-algebra by Proposition 4.8 (3). Again by the limit/colimit-coincidence theorem (SP82), the cone ⟨s_{n}^{R}⟩ : \overline{ω} \underrightarrow{.} ⟨L^{n}(1 ← Σ) : Σ_{n} ← Σ_{n+1}⟩, where s_{0}^{R} = (\overline{ω} → 1) and s_{n+1}^{R} = L(s_{n}^{R}) ∘ σ^{−1} (n ≥ 0), is limiting as so is ⟨Ls_{n}^{R}⟩ : L\overline{ω} \underrightarrow{.} ⟨L^{n+1}(1 ← Σ) : Σ_{n+1} ← Σ_{n+2}⟩ because L is a Cpo-functor. Then, by (the dual of) the basic lemma (SP82), the coalgebra σ^{−1} : \overline{ω} → L\overline{ω} is final because it is the unique mediating morphism ⟨s_{n+1}^{R}⟩ → ⟨Ls_{n}^{R}⟩.

Examples of domain-theoretic categories are: [W_{≤}^{op}, Cpo_{⊑}], for W_{≤} a small Cpocategory, with the pointwise lifting monad.

The rest of the categories in Example 1.2 are not examples:

— Set, Preo and Poset fail Axiom 2.

— Poset_{∧} fails Axioms 2 and 5.

— Cpo_{∧} fails Axiom 5. (Though, in the light of the following section, this is not unsatisfactory.)

10. Stability

Though indirectly, it is possible to incorporate stability into our axiomatic framework. However, as we argue below, it is best to abandon Cpo-enrichment.

The analysis of Sections 6 and 7 suggested considering the following: Definition 10.1. Let VPoset_{∧} be the category with:

— objects: (P, V) with P ∈ | Poset_{∧} | and V : P ω → P in Poset_{∧} satisfying

(Constant) V⟨x⟩_{n} = x  (x ∈ | P |);
(Diagonal) V⟨V⟨x_{n,m}⟩_{m}⟩_{n} = V⟨x_{m,m}⟩_{m} (x : ω × ω → P in Poset_{∧});
(Shift) V⟨x_{n+1}⟩ = V⟨x_{n}⟩ (x : ω → P in Poset_{∧});

and

— morphisms: f : (P, V_{P}) → (Q, V_{Q}) with f : P → Q in Poset_{∧} satisfying

(Continuity) f(V_{P} ⟨x_{n}⟩) = V_{Q}⟨f(x_{n})⟩ (x : ω → P in Poset_{∧}).

By construction, Cpo_{∧} is a full subcategory of VPoset_{∧}. Moreover, VPoset_{∧} satisfies Axioms 1–4 but not Axiom 5, does not Cpo-enrich with respect to the path order, and further: Proposition 10.2. There is no Cpo-enrichment on VPoset_{∧} in which ⊥ approximates ⊤ in the hom of global elements of Σ.

Outstandingly, (VPoset_{∧})^{𝕃} together with the lifting comonad is a model of intuitionistic linear type theory (in the sense of (BBHdP93)) with sums and products in which the solution of domain equations is possible. Moreover, notice that in VPoset_{∧} we have broaden the notion of domain by allowing, for example, the posets

0 → 1 → ⋯ → i → ⋯ → ∗ → ∞

∞ ↗ 0 → 1 → ⋯ → i → ⋯ ↘ ∗

equipped with a passage-to-the-limit operator V given by

V⟨x_{n}⟩ = \{ \begin{matrix}x & , if x_{n} = x for all n greater than some n_{0} \\ ∞ & , otherwise \end{matrix}

We conclude that Cpo-enrichment is not the natural setting for stability. Remark. An abstract approach to “formal cpos” generalising the construction of Definition 10.1 has been considered by the author and Gordon Plotkin —see (FJM^{+}96, § Axiomatic Domain Theory). For example, this construction applied to Poset (instead of Poset_{∧}) yields VPoset ≅ Cpo.

Marcelo P. Fiore 28

Acknowledgements. Conversations with Gordon Plotkin, John Power and Pino Rosolini on axiomatic domain theory, category theory and synthetic domain theory are gratefully acknowledged. The detailed comments of the anonymous referees helped to improve the presentation. Finally, I am most grateful to Achim Jung and Klaus Keimel for their patience in waiting for this paper.

References

S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, 1996.

P.N. Benton, G.M. Bierman, J.M.E. Hyland, and V.C.V. de Paiva. Linear lambda calculus and categorical models revisited. In E. Börger et al., editor, Selected Papers from Computer Science Logic ’92, volume 702 of Lecture Notes in Computer Science, 1993.

R.L. Crole and A.M. Pitts. New foundations for fixpoint computations: FIX-hyperdoctrines and

the FIX-logic. Information and Computation, 98:171–210, 1992. A. Carboni, M.C. Pedicchio, and G. Rosolini, editors. Category Theory, volume 1488 of Lecture

Notes in Mathematics. Springer-Verlag, 1991. Proceedings of the International Conference held in Como, Italy, July 22-28.

M.P. Fiore. Lifting as a KZ-doctrine. In D. Pitt, D. Rydeheard, and P. Johnstone, editors, Proceedings of the 6^{th} International Conference, CTCS’95, volume 953 of Lecture Notes in Computer Science, pages 146–158. Springer-Verlag, August 1995.

M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Cambridge University

Press Distinguished Dissertations in Computer Science, 1996. M.P. Fiore, A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini, and I. Stark. Domains

and denotational semantics: History, accomplishments and open problems. In number 59 of Bulletin of the European Association for Theoretical Computer Science, pages 227–256, June 1996.

P.J. Freyd. Algebraically complete categories. In (CPR91), pages 131–156, 1991. M. Henessy and G. Plotkin. Full abstraction for a simple parallel programming language. Lecture

Notes in Computer Science, 74, 1979. J.M.E. Hyland. First steps in synthetic domain theory. In (CPR91), pages 95–104, 1991. P.T. Johnstone. Topos Theory. Academic Press, 1977. A. Kock. Monads on symmetric monoidal closed categories. Arch. Math. (Basel), 21:1–10, 1970. A. Kock. Closed categories generated by commutative monads. J. Austr. Math. Soc., XII:405–

424, 1971. E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92,

July 1991. W. Phoa. Domain Theory in Realizability Toposes. PhD thesis, Trinity College, Cambridge,

1990. (Also CST-82-91, University of Edinburgh). G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986. D.S. Scott. Outline of a mathematical theory of computation. Technical Report PRG-2, Oxford

Univ. Computing Lab., 1970. M.B. Smyth and G.D. Plotkin. The category-theoretic solution of recursive domain equations.

SIAM Journal of Computing, 11(4):761–783, November 1982. P. Taylor. The fixed point property in synthetic domain theory. In 6^{th} LICS Conference, pages

152–160. IEEE, 1991.

An Enrichment Theorem for an Axiomatisation of Categories of Domains 29

P. Taylor. Synthetic domain theory notes. Manuscript, 1994.

Some diagrams have been drawn with Paul Taylor’s commutative-diagrams package.