Enrichment and Representation Theorems for Categories of Domains and Continuous Functions

Marcelo P. Fiore^{∗} Department of Computer Science Laboratory for Foundations of Computer Science University of Edinburgh, The King’s Buildings Edinburgh EH8 3JZ, Scotland

                            <mf@dcs.ed.ac.uk>

March 1996

Synopsis

Domain-theoretic categories are axiomatised by means of categorical non-order-theoretic requirements on a cartesian closed category equipped with a commutative monad. We prove 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. Subsequently, we provide a representation theorem of the form: every small domain-theoretic category (with a lifting monad) has a full and faithful representation in a domain-theoretic category of cpos and continuous functions (with a lifting monad) in a suitable intuitionistic set theory.

Our analysis suggests more liberal notions of domains. In particular, we present 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 possible.

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 and EC project Programming Language Semantics and Program Logics grant SC1000 795

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 Axioms 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 (see Example 1.2). 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). Examples of categories with a dominance are introduced to aid the reader in understanding the axioms. (The status of these examples with respect to our axiomatisation is discussed in Section 10.) 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. (A possible definition of ∞ from a universal property for \overline{ω}, taken from [Fre91], is given in Section 5.) The essential difference between our fixed-point object and the one previously considered in [CP92] is its constructive 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 6 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, case analysis, 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 7 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 8 and 9 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 domaintheoretic category is —naturally— Cpo with the lifting monad. Subsequently, in Section 11 we show that every small domain-theoretic category (with a lifting monad) has a full and faithful representation in a domain-theoretic category of cpos and continuous functions (with a lifting monad) in a suitable intuitionistic set theory. Thus to each small domain-theoretic category we associate a universe in which the domain-theoretic category can be studied as a category of cpos and continuous functions by means of intuitionistic logic.

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 12, we present (without further exploration) a category which contains the category of cpos with continuous bounded binary infs 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 possible.

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 see [Koc70].

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 and μ_{C} : L^{2}C → LC 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) 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 the lifting monad and powerdomain monads (see [HP79, AJ96]) on Cpo:

Example 1.2 The lifting monad on Cpo can be described as follows: it has underlying functor ( )_{⊥} associating to a cpo P the cpo P_{⊥} = {⊥} ∪ {[x] | x ∈ P } where ⊥ ≤_{P_{⊥}} [x] and [x] ≤_{P_{⊥}} [y] ⟺ x ≤_{P} y with unit the inclusion η_{P} : P ↪ P_{⊥} : x ↦ [x], multiplication μ_{P} : (P_{⊥})_{⊥} → P_{⊥} sending ⊥ ↦ ⊥, [⊥] ↦ ⊥, [[x]] ↦ [x], and tensorial strength t′_{P,Q} : P × Q_{⊥} → (P × Q)_{⊥} sending ⟨x, ⊥⟩ ↦ ⊥ and ⟨x, [y]⟩ ↦ [⟨x, y⟩]. □

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

Remark. When C is cartesian closed L can be internalised; as writing \underline{L}_{A,B} : B^{A} → LB^{LA} for the exponential transpose of L(e) ∘ t′′ : B^{A} × LA → LB we have

C(A, B) C(1, B^{A})  C(1, LB^{LA}) \underline{L}^{A,B} ∘  . C(LA, LB) L_{A,B}

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

We present an axiomatisation of lifting in terms of dominances which is by now a traditional way to generate examples of Assumption 1. (For the connection between this axiomatisation and partiality consult [Fio96].)

Convention. Subobjects obtained as pullbacks of a monomorphism m are called m-subobjects.

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) 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.

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 1. Let Set be the category of small sets and functions, and let 1 = {0} and 2 = {0, 1}.

Then, 1 ↪ 2 : 0 ↦ 1 classifies all subsets.

2. Let Poset (Preo) be the category of small posets (preordered sets) and monotone functions, and let 1 = {0} and 2 = {0 ≤ 1}.

Then, 1 ↪ 2 : 0 ↦ 1 classifies upper-closed subsets.

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

Then, 1 ↪ 2 : 0 ↦ 1 classifies Scott-open subsets.

4. Convention. To emphasise the distinction between ordinary and order-enriched categories the latter are subscripted with the order providing the enrichment. (Thus, for example, Set denotes the ordinary category of small sets and functions whilst Set_{=} denotes the order-enriched category of small sets and functions ordered discretely.) The ordinary underlying category of an order-enriched 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 Cpo-functors and natural transformations, and 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. Definition 2.3 Let K_{≤} be a Poset- (Cpo-) cartesian-closed-category and let Λ ∈ | K |. The category K_{Λ} has objects (P, ⊓ : P^{Λ} → P) where P ∈ | K | and λ(P × Λ ⟶^{π_{1}} P) ⊣ ⊓ : P^{Λ} → P in K_{≤}; and morphisms f : (P, ⊓_{P}) → (Q, ⊓_{Q}) where f : P → Q in K is such that f ∘ ⊓_{P} = ⊓_{Q} ∘ f^{Λ}. Composition and identities are as in K. □

In Poset_{∧} (Cpo_{∧}), 1 ↪ 2 : 0 ↦ 1 classifies upper-closed (Scott-open) subsets closed under bounded binary infs.

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 term of so-called lifting structures (see Theorem 2.5).

Definition 2.4 (Lifting structure) Let K be a category with an initial object 0 and a terminal object 1.

A lifting structure (L, η) on K consists of a pointed endofunctor η : Id \underrightarrow{.} L : K → K such that

• pullbacks of η_{1} always exist,

• η is cartesian (that is, for every f : A → B,

A LA  B LBη_{B} η_{A}  f Lf

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

D A  Bη_{B} LB

for a unique characteristic map A → LB), and

• the composite 1 ↪^{η_{1}} L1 ↪^{η_{L1}} L^{2}1 and the unique map 0 → 1 are η_{1}-subobjects. □

Theorem 2.5 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.6 (Lifting) Let K be a cartesian category with an initial object.

Every lifting structure (L, η) on K induces a lifting monad 𝕃 = (L, η, μ, t′) on K with multiplication and tensorial strength defined as follows:

[figure: A; A; A; LA; η_{A}; ∩; L^{2}A; η_{LA}; ∩; μ_{A}; LA; ∩; η_{A}; A × B; A × B; A × B; L(A) × B; η_{A} × B; ∩; t′_{A,B}; L(A × B); ∩; η_{A×B}]

□

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 zero object 1 then C has terminal object 1 (as the forgetful functor C^{𝕃} → C has a left adjoint and therefore preserves limits); moreover if C has 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.

Proposition 3.1 If C has a strict initial object 0 then, for a lifting monad 𝕃, C^{𝕃} has a zero object 1 if and only if the dominance classifies 0 → 1. □ Assumption 2 We assume C^{𝕃} has a zero object 1. □ Definition 3.2 (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 Constructive 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.

To motivate the first axiom it is convenient to regard L^{n}1 as a canonical chain of n + 1 elements. In fact, as we show below, for n ≥ 0, every L^{n}1 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 6). Convention. We set: Σ = L1, Σ_{n} = L^{n}1, ⊥ = (1 ∘→ Σ), ⊤ = η_{1} : 1 → Σ. 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} ([figure: 1; ⊤; Σ; L(\underline{i}_{Σ_{n}}); Σ_{n+1}]) = ([figure: 1; \underline{i}_{Σ_{n}}; Σ_{n}; η_{Σ_{n}}; Σ_{n+1}]). □

In view of the above informal argument, Axiom 1 postulates de 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

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}  (1)

henceforth denoted ⟨s_{n}⟩, is colimiting. □ Remark. Note that s_{0} = σ ∘ ⊥_{L\overline{ω}} and, for n ≥ 0, s_{n+1} = σ ∘ L(s_{n}).

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 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) f ∘ fix(f) = f ∘ it(f) ∘ ∞ = it(f) ∘ succ ∘ ∞ = it(f) ∘ ∞ = fix(f). □ Proposition 4.7 1. (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).

2. Assuming σ is an isomorphism, if ∞ is the unique fixed-point of succ then the uniformity property characterises fix.

Proof:

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

(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
[figure: Lρ_{X}]
[figure: L^{2}\overline{ω}; Lσ^{−1}; L^{2}(f ∘ it(f)); L^{2}X]

[figure: L\overline{ω}; μ\overline{ω}; L(f ∘ it(f)); LX; μ_{X}]
[figure: ρ_{X}]
[figure: \overline{ω}; σ; it(f); X; ρ_{X}; .]

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

For our subsequent development σ need not be an isomorphism; when it is (as happens in the leading example) we have:

Proposition 4.8 Assume σ is an isomorphism. Then,

1. (\overline{ω}, σ ∘ μ\overline{ω} ∘ Lσ^{−1}) is a pointed object and σ is strict.

2. σ : 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) 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 Infinity

A definition of ∞ from a universal property of \overline{ω} is possible. Following [Fre91] one could proceed as follows:

Axiom 2^{+} (Final coalgebra) σ is an isomorphism and σ^{−1} : \overline{ω} → L\overline{ω} is a final L-coalgebra.□

Remark. By Proposition 4.8 (2), it follows that σ is a free L-algebra (i.e. an initial L-algebra whose inverse is a final L-coalgebra —see [Fre91]).

Definition 5.1 ([Fre91]) Let ∞′ : 1 → \overline{ω} be the unique L-coalgebra morphism (1, ⊤) → (\overline{ω}, σ^{−1}). □

Proposition 5.2 ([Fre91]) ∞′ is the unique fixed-point of σ ∘ η\overline{ω}. □

6 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 6.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 6.2 1. In Set with the dominance 1 ↪ 2, the path relation is indiscrete (i.e. f ⊑ g for all f and g).

2. In (Preo) Poset and Cpo with the dominance 1 ↪ 2 the path relation is the pointwise (pre)order (i.e. f ⊑ g : P → Q ⟺ ∀ x ∈ P. fx ≤_{Q} gx).

3. For a small Cpo-category W_{≤}, in [W_{≤}^{op}, Cpo_{⊑}] with the dominance 1 ↪ 2 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. In [2_{=}, Cpo_{⊑}] with the dominance 1 ↪ 𝔖 the path relation is the pointwise pointwise order.

5. In Poset_{∧} and Cpo_{∧} with the dominance 1 ↪ 2 the path relation is the stable order; that is, f ⊑ g : P → Q ⟺ ∀ x, y ∈ P. x ≤_{P} y ⇒ fx = gx ⊓_{Q} fy. □

Example 6.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 6.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 6.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. □

Assumption 3 We assume C cartesian closed. □

The calculus of proofs (see [Fio95]):

Proposition 6.6 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).

7. Let A ⟶^{⨿_{1}} A + B ⟵^{⨿_{2}} B be a coproduct diagram with associated natural isomorphism [ , ] : C(A, –) × C(B, –) ≅ C(A + B, –).

Then, α : f f′ : A → C and β : g g′ : B → C if and only if

γ : [f, g] [f′, g′] : A + B → C where γ is the unique mediating morphism between

Σ_{m} × A ⟶^{Σ_{m}×⨿_{1}} Σ_{m} × (A + B) ⟵^{Σ_{m}×⨿_{2}} Σ_{m} × B and Σ_{m} × A ⟶^{α} C ⟵^{β} Σ_{m} × B. □

Corollary 6.7 α : f g : A → B if and only if λ(α) : ⌜f⌝ ⌜g⌝ : 1 → B^{A}. □

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

Example 6.8 In [↙↘, Cpo], the category of spans over Cpo, with the dominance 1 ↪ 𝔖 (see Example 2.2 (4b)) the path relation is not transitive.

To see this observe that

(∗, ∗)
[figure: 1; =; L0; =; .......; .......]
∗  ∗

and

𝔖 = L1 = [figure: (⊤, ⊤); (⊤, ⊥)  (⊥, ⊤); .......; .......; ⊤  (⊥, ⊥)  ⊤; .......; .......; ⊥  ⊥]

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

(⊥, ⊥)  (⊤, ⊤)
[figure: .......; .......; and; .......; .......]
⊥  ⊥  ⊤  ⊤ .

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

(⊤, ⊤)
[figure]
(⊤, +)  (+, ⊤)
[figure: ....................; ....................]
(+, +)
[figure]
⊤  (+, ⊥)  (⊥, +)  ⊤
[figure: .......; .......]
+  (⊥, ⊥)  +
[figure: .......; .......]
⊥  ⊥

and in its hom of global elements we have that

[figure: (⊥, ⊥); .......; .......; ⊥  ⊥; (+, +); .......; .......; +  +; (⊤, ⊤); .......; .......; ⊤  ⊤]

but

(⊥, ⊥)  (⊤, ⊤)
[figure: .......; .......; ; .......; .......]
⊥  ⊥  ⊤  ⊤ .
□

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

Σ_{n} η_{Σ_{n}} Σ_{n+1}  L^{n+1}⊥ L^{n}⊥  Σ_{n+1} η_{Σ_{n+1}} Σ_{n+2}  (n ≥ 0)

is a pushout. □

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

L𝔖 = [figure: (⊤, ⊤); (⊤, +)  (+, ⊤); (⊤, ⊥)  (+, +)  (⊥, ⊤); .......; .......; ⊤  (+, ⊥)  (⊥, +)  ⊤; .......; .......; +  (⊥, ⊥)  +; .......; .......; ⊥  ⊥  .]

□

In the rest of the section we will only be concerned with the instance of Axiom 3 for n = 0. Note that, as × A preserves colimits, it follows that the commuting square

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

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 (2), we have λ([α, β]) = [λ(α), λ(β)].

Proposition 6.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 6.11 The category C equipped with ⊑ (henceforth denoted C_{⊑}) is a Preo-cartesian-closed-category and L determines a Preo-endofunctor on it.

Proof: By Propositions 6.6 (1) and 6.10, the path relation gives a preorder on each hom-set. And, by Proposition 6.6 (2), the composition of morphisms is a monotone operation with respect to the path preorder. Finally, by Proposition 6.6 (5–6), the cartesian closed structure Preo-enriches.

L determines a Preo-endofunctor by Proposition 6.6 (4). □

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

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

7 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 7.1); then, using Axiom 1, we internalise the whole ω-chain \overline{f} (see Definition 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.3). □ Example 7.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 7.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 7.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 7.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 7.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: First, [\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 7.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 7.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 7.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 7.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 7.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}⊥  (3)

and

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

And (3) 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 (4) 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. Note that from the characterisation of fix in Example 7.8, using (Constant), (Shift) and the fact that canonical upper bounds are preserved by composition, the usual argument for showing that fix is a fixed-point operator can be reproduced.

8 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; establish the continuity of L (with respect to V); and explore further algebraic properties of V and fix. Surprisingly, it follows that the path preorder is antisymmetric. Proposition 8.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. □ Corollary 8.2 The map

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

is a bijection. □

Canonical upper bounds are preserved by L: Corollary 8.3 (Continuity of L) Let ⟨f_{n}⟩ be an ω-chain in C_{⊑}(A, B). Then,

L(V⟨f_{n}⟩) = V⟨L(f_{n})⟩.

Proof: Because the commutativity of

[figure: (B^{A})\overline{ω}; (B^{A})^{∞}; B^{A}; (LB^{LA})\overline{ω}; (\underline{L}_{A,B})\overline{ω}; (LB^{LA})^{∞}; LB^{LA}; ^{\underline{L}^{A,B}}]

implies the commutativity of

C(1, LB^{LA}) C(1, B^{A}) C(1, (LB^{LA})\overline{ω}) Preo(ω, C_{⊑}(LA, LB))  C(A, B) C(LA, LB) C(1, (B^{A})\overline{ω}) Preo(ω, C_{⊑}(A, B))  V V L_{A,B} ∘  L_{A,B}  □

Axiom 4 forces and ⊑ to coincide. More importantly, it allows us to conclude:

Proposition 8.4 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) ∘ (⊥ × 1) = 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, Γ =^{def} ⟨[f ∘ ⨿_{M} ⊑ g ∘ ⨿_{M}]⟩_{M} : Σ × Δ \underrightarrow{.} D.

As Σ × preserves colimits, it follows that Σ × ⨿ : Σ × Δ \underrightarrow{.} Σ × C is colimiting.

Finally, 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 × ⨿). □

Further algebraic properties of V and fix are:

Proposition 8.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} ∘ ∞⟩] ∘ ∞.  □

Convention. For f ⊑ g : A → B, we set [f ⊑ g] : f g. Corollary 8.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}⟩  (5)

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 8.5
= [⟨[⟨c_{n,m}⟩_{n}]⟩_{m}] ∘ ⟨π_{2}, π_{1}⟩ ∘ ⟨∞, ∞⟩ , by (5)
= [⟨[⟨c_{n,m}⟩_{n}]⟩_{m}] ∘ ⟨∞, ∞⟩
= [⟨[⟨c_{n,m}⟩_{n}] ∘ ∞⟩_{m}] ∘ ∞  , by Proposition 8.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 8.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 6.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 7.8. □

As a surprising consequence we have:

Theorem 8.8 C_{⊑} is Poset-cartesian-closed.

Proof: By Theorem 6.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. □

9 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 9.1 (3) and Corollary 9.2). We are thus in position to establish the enrichment theorem.

Proposition 9.1 The following are equivalent:

1. (Interpolation Property) The commuting square

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

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}⟩ = [⟨⊥, ⊥⟩ ⊑ ⟨⊤, ⊥⟩ ⊑ ⟨⊤, ⊤⟩], where for f ⊑ g ⊑ h : A → B we write [f ⊑ g ⊑ h] for the unique mediating morphism [[f ⊑ g], [g ⊑ h]] : LΣ × A → X from (2) to the cone

Σ × A ⟶^{[f⊑g]} X ⟵^{[g⊑h]} Σ × A.

2. (Diamond property) If

x′  y x y′  (7)

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 the least and greatest elements. □ Axiom 5 The commuting square (6) is a pushout. □ Corollary 9.2 (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. □

The objects of C_{⊑} are internally complete in the following sense: Lemma 9.3 For every C ∈ | C_{⊑} |, we have 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 7.4
⊑ [⟨∞⟩]_{n}  , by Corollary 9.2 and Example 6.3 (3)
= ∞ ∘ (Σ_{n} → 1) , by Example 7.3

we are done. □

Such a strong form of completeness which holds in Cpo but does not hold in Cpo_{∧} exhibits a crucial difference between continuity and stability.

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

Proof: From the fact that for every A ∈ | C |, C_{⊑}(A, ) : C_{⊑} → Poset_{⊑} preserves adjunctions (as it is a Poset-functor) we have, by Lemma 9.3 and Corollary 9.2, 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 Lemma 7.13. L determines a Cpo-functor by Theorem 6.11 and Corollary 8.3. □

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

Corollary 9.5 C^{𝕃} and C_{𝕃} Cpo-enrich with respect to ⊑. □

Corollary 9.6 \overline{ω} is a free L-algebra. □

10 Domain-theoretic categories

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

Examples of domain-theoretic categories are: [W_{≤}^{op}, Cpo_{⊑}], for W_{≤} a small Cpo-category, with the dominance 1 ↪ 2.

The rest of the categories in Example 2.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 Section 12, this is not unsatisfactory.)

11 Representation theory

From the enrichment theorem it follows that every domain-theoretic category comes equipped with a natural Cpo-enrichment. Moreover, from the representation theorem below, every small domain-theoretic category (with a lifting monad) has a full and faithful representation in a domain-theoretic category of cpos and continuous functions (with a lifting monad) in a suitable intuitionistic set theory.

More precisely, the intuitionistic universes of sets we will be dealing with are presheaf topoi (see [LM92]). Thus, in Subsection 11.1, we define the category Cpo(E) of cpos and continuous functions in a topos E with natural numbers object and characterise Cpo(E) for E a presheaf topos. By enriched Yoneda, it follows that every small domain-theoretic category C has a full and faithful representation in Cpo(PC). However, since the domain-theoretic structure need not be preserved by the embedding we go further and use a notion of orthogonality (Subsection 11.2) to strengthen the result. In fact, in Subsection 11.3, we identify a domain-theoretic full subcategory of Cpo(PC) which is also a full reflective subcategory of the topos PC and in which C has a full and faithful representation (via an embedding that preserves the domain-theoretic structure). Furthermore, via the representations the path order becomes the pointwise order.

Convention.

1. For a small category A we write PA for [A^{op}, Set].

2. For a small Cpo-category W_{≤}, we write [W^{op}, Cpo] ([W_{⊑}^{op}, Cpo_{⊑}]_{⊑}) for the functor category (Cpo-functor-category) of functors (Cpo-functors) and natural transformations (ordered pointwise). Moreover, we write CAT (Cpo-CAT) for the large 2-category of locally small categories (Cpo-categories), functors (Cpo-functors) and natural transformations.

11.1 Cpos in a topos with natural numbers object

In a topos E with natural numbers object ℕ, one can define a “cpo” to be an object P of E equipped with a subobject ≤ ↣ P × P and a map ⋁ : Chains(P, ≤) → P where Chains(P, ≤) is the set of countable chains in (P, ≤) defined as {c ∈ P^{ℕ} | ∀ n ∈ ℕ. c(n) ≤ c(n + 1)}, such that the sentence stating that (P, ≤) is a partial order with lub operator ⋁ is valid in E. Explicitly, (P, ≤, ⋁) is a cpo in E, when the following sentences are valid in E:

(Reflexivity) ∀ x ∈ P. x ≤ x,

(Transitivity) ∀ x, y, z ∈ P. x ≤ y ∧ y ≤ z ⇒ x ≤ z,

(Antisymmetry) ∀ x, y ∈ P. x ≤ y ∧ y ≤ x ⇒ x = y,

(Lub) ∀ c ∈ Chains(P, ≤). ∀ u ∈ P. (∀ n ∈ ℕ. c(n) ≤ u) ⟺ ⋁(c) ≤ u. For cpos (P, ≤_{P} , ⋁_{P}) and (Q, ≤_{Q}, ⋁_{Q}) a map f : P → Q in E is said to be continuous if the following sentences are valid in E:

(Monotonicity) ∀ x, y ∈ P. x ≤_{P} y ⇒ f(x) ≤_{Q} f(y),

(Continuity) ∀ c ∈ Chains(P, ≤). f(⋁_{P} c) = ⋁_{Q}(f ∘ c). We write Cpo(E) for the category of cpos and continuous maps in E.

Moreover, for f, g : (P, ≤_{P} , ⋁_{P}) → (Q, ≤_{Q}, ⋁_{Q}) we set f ≤ g if and only if the following sentence is valid in E:

(Pointwise order) ∀ x ∈ P. f(x) ≤_{Q} g(x).

We have that Cpo(Set) ≅ Cpo and Cpo(Set)_{≤} ≅ Cpo_{⊑}, more generally: Proposition 11.1 For every small category A,

Cpo(PA) ≅ [A^{op}, Cpo] and Cpo(PA)_{≤} ≅ [A_{=}^{op}, Cpo_{⊑}]_{⊑}.

Proof: Implicit in [Ros80, Chapter III]. □

11.2 Orthogonality

A crucial rôle in the representation theorem below is played by a notion of orthogonality with respect to cones, generalising that of orthogonality with respect to maps (see [Bor94a]) and the sheaf condition for a cover in a Grothendieck topology (see [Bor94b, LM92]). Convention. In the sequel all cones range over small diagrams.

An object is said to be orthogonal to a cone whenever it believes (or, as Lawvere will put it, perceives) that the cone is colimiting. Formally: Definition 11.2 1. We say that an object K is orthogonal to a cone Δ \underrightarrow{.} C whenever for

every cone Δ \underrightarrow{.} K there exists a unique C → K such that

C . Δ .K .

2. (O(K, J)) For a category K and a class J of cones in K we define O(K, J) as the full

subcategory of K consisting of all those objects orthogonal to every cone in J. □ Proposition 11.3 Let J be a class of cones in a cocomplete category K. Then,

O(K, J) = O(K, J′) where J′ = {colim(Δ) → C |  ↙ ↘C colim(Δ)Δ→  for Δ → C in J}.  □

Proposition 11.4 For a class J of cones in a small category A, O(PA, J) is the full subcategory of PA consisting of all those presheaves P such that for every γ : Δ \underrightarrow{.} C in J the cone P γ : P C \underrightarrow{.} P Δ is limiting in Set. □

Orthogonality and free cocompletions

Convention. For a class J of colimiting cones in a category X, a functor X → Y is said to be J-cocontinuous if it preserves all the colimits in the class J.

Theorem 11.5 ([Kel82]) For a class J of colimiting cones in a small category A, O(PA, J) is the free cocompletion of A that respects the colimits in J.

Precisely,

• O(PA, J) is cocomplete and the Yoneda embedding A ↪ PA restricts to a J-cocontinuous embedding A ↪ O(PA, J), and

• for every cocomplete category K and J-cocontinuous functor A → K we have a commuting

triangle

A ^{⊂} O(PA, J)

[figure]

K

for a unique cocontinuous functor O(PA, J) → K.

Moreover, the functors O(PA, J) → K arising as above are precisely those which have a right adjoint. □

Corollary 11.6 For a class J of colimiting cones in a small category A,

A  PA . O(PA, J)  □

Orthogonality and limits

Proposition 11.7 The embedding O(K, J) ↪ K creates limits. That is, for Γ : G → O(K, J), L \underrightarrow{.} Γ : G → K limiting implies L ∈ | O(K, J) |.

Proof: For Γ : G → O(K, J), assume L \underrightarrow{.} Γ : G → K limiting.

Let Δ \underrightarrow{.} C : D → K be a cone in J and consider a cone Δ \underrightarrow{.} L.

By orthogonality, for every k ∈ | G |, we have unique maps C → Γ_{k} such that

(Δ \underrightarrow{.} C → Γ_{k}) = (Δ \underrightarrow{.} L → Γ_{k}).  (8)

Moreover, for every i → j in G,

(Δ \underrightarrow{.} C → Γ_{i} → Γ_{j}) = (Δ \underrightarrow{.} L → Γ_{i} → Γ_{j})
= (Δ \underrightarrow{.} L → Γ_{j})
= (Δ \underrightarrow{.} C → Γ_{j})

so that (C → Γ_{i} → Γ_{j}) = (C → Γ_{j}) and thus we have a cocone C \underrightarrow{.} Γ.

Finally, we show that

↙ Δ C  L ↘ ⟶  ⟺  C  L ⟶↖ ↗ Γ  .

(⇒) Because, for every k ∈ | G |,

(Δ \underrightarrow{.} C → L → Γ_{k}) = (Δ \underrightarrow{.} L → Γ_{k})
= (Δ \underrightarrow{.} C → Γ_{k}) , by (8)

and, by orthogonality, (C → L → Γ_{k}) = (C → Γ_{k}).

(⇐) Because, for D ∈ | D |,

(Δ_{D} → C → L \underrightarrow{.} Γ) = (Δ_{D} → C \underrightarrow{.} Γ)
= (Δ_{D} → L \underrightarrow{.} Γ) , by (8)

and, as L \underrightarrow{.} Γ is limiting, (Δ_{D} → C → L) = (Δ_{D} → L). □

Corollary 11.8 If K is complete then so is O(K, J). □

Orthogonality and cartesian closure

Definition 11.9 For a class J of cones in a category K and a class O of objects in K, we set

⌊J⌋_{O} =^{def} {γ × X | γ ∈ J, X ∈ O}. □

Proposition 11.10 For a class J of cones in a cartesian closed category K, O(K, ⌊J⌋_{| K |}) is a full sub-cartesian-closed-category of K. □

Proposition 11.11 Let K and K^{G} be cartesian closed, and let Δ : G → K be a diagram with colimit.

For a cone γ : Δ \underrightarrow{.} C and an object K ∈ | K |, the following are equivalent:

• For every X ∈ | K |, K is orthogonal to γ × X : Δ × X \underrightarrow{.} C × X.

• For every X ∈ | K |, K^{X} is orthogonal to γ : Δ \underrightarrow{.} C.

• K^{γ} : K^{C} \underrightarrow{.} K^{Δ} is limiting.

• For u the unique mediating morphism colim(Δ) → C, K^{u} : K^{C} → K^{colim Δ} is an isomorphism. □

Theorem 11.12 For a class J of cones in a small cartesian closed category A,

O(PA, ⌊J⌋_{| A |}) = O(PA, ⌊J⌋_{| PA |})

Proof:

(⊆) For P ∈ | PA | and γ : Δ \underrightarrow{.} C in J assume that P is orthogonal to γ×A : Δ×A \underrightarrow{.} C×A for all A ∈ | A |. Then, for F ∈ | PA |, the following bijective correspondence

C × F → P C × colim⟨F_{k}⟩_{k} → P colim⟨C × F_{k}⟩_{k} → P ⟨C × F_{k}⟩_{k} \underrightarrow{.} P ⟨Δ × F_{k}⟩_{k} \underrightarrow{.} P Δ × colim⟨F_{k}⟩_{k} → P Δ × F → P  A × preserves colimits for all A ∈ | A | since Δ is a diagram in A and using the assumption F ≅ colim_{k∈∫_{A}F} ⟨F_{k}⟩ with F_{k} ∈ | A |

shows that P is orthogonal to γ × F : Δ × F \underrightarrow{.} C × F.

(⊇) Vacuous. □

11.3 Representation theorem

Let (C, 𝕃) be a small domain-theoretic category such that C has an initial object (and binary coproducts) and 𝕃 is a lifting monad (i.e. induced by a lifting structure —see Section 2).

Via the Yoneda embedding, C embeds in PC as a category of sets and functions. Now we identify a full (reflective) subcategory of PC in which C embeds as a category of cpos and continuous functions.

Noticing that except for Axiom 2 (which is equational) the rest of the axioms state that certain cones are colimiting, our idea is to use the notion of orthogonality to consider all those sets that believe the axioms while preserving the domain-theoretic structure. Technically, this is achieved by restricting to the full subcategory of all those sets which are orthogonal to a suitably closed class of cones containing the cones in the axioms.

Definition 11.13 1. (J_{(C,𝕃)}) We define J_{(C,𝕃)} as the smallest family of cones in C containing the following class of basic cones:

\begin{aligned}& 0 \\ ∅ \end{aligned}

1  Σ ⊥  L⊥ \overline{ω}^{s_{0}}  ^{s_{1}}  Σ_{2}^{s_{2}}  · · · · · ·

Σ_{n} η_{Σ_{n}} Σ_{n+1}  L^{n+1}⊥ L^{n}⊥  Σ_{n+1} η_{Σ_{n+1}} Σ_{n+2}  (n ≥ 0)

Σ Σ Σ  1 1 ⊥ ⊥ ⊥  ⊤ ⊤ Σ Σ ⊤

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

(  A  A + B  B  )

and satisfying the following closure properties:

(Parameterisation) For γ ∈ J_{(C,𝕃)} and X ∈ | C |, γ × X ∈ J_{(C,𝕃)}.

(Stability) For Δ \underrightarrow{.} C in J_{(C,𝕃)} and D ↪ C a ⊤-subobject in C,

Γ Δ  D C ⇒ Γ \underrightarrow{.} D in J_{(C,𝕃)}.

2. (R(C, 𝕃)) We write R(C, 𝕃), or simply RC when 𝕃 is clear from the context, for O(PC, J_{(C,𝕃)}). □ Proposition 11.14 Every cone in J_{(C,𝕃)} is colimiting.

Proof: Because the class of colimiting cones contains the class of basic cones, and it is both closed under parameterisation (by cartesian closure) and under stability (see [Fio96, Lemma 5.3.6]). □

Theorem 11.15 (Representation theorem)

1. The Yoneda embedding C ↪ RC preserves the initial object, finite products, exponentials, the lifting structure, the free lift-algebra (and binary coproducts).

2. RC equipped with the lifting monad induced by the lifting structure is a domain-theoretic category.

3. In Cpo-CAT,

C_{⊑} ↪ R(C)_{⊑} ↪ [C_{⊑}^{op}, Cpo_{⊑}]_{⊑} ↪ Cpo(PC)_{≤}

where R(C)_{⊑} ↪ [C_{⊑}^{op}, Cpo_{⊑}]_{⊑} : P ↦ R(C)_{⊑}( , P).

4. In CAT,

Cpo(PC) . PC C  RC

Proof:

(1) The embedding C ↪ RC preserves the initial object, the free lift algebra (and binary coproducts) by construction of J using Theorem 11.5; it preserves the cartesian closed structure by Proposition 11.10 and because so does the Yoneda embedding C ↪ PC; furthermore it preserves the lifting structure by the following lemmas:

(1a) The Yoneda embedding C ↪ PC preserves the dominance. (See [Ros86, Chapter 3].)

(1b) For

in PC, 1

Σ Q

P

⊤

P ∈ | RC | implies Q ∈ | RC |. (See Proposition 11.7.)

(1c) Lemma 11.16 For

η_{P}LP P  1⊤ Σ Π^{⊤}P  in PC,

P ∈ | RC | implies LP ∈ | RC |.

Proof: The argument we give has been adapted from a corresponding result of Pino Rosolini for sheaf topoi.

Assume P ∈ | RC |. Let Δ \underrightarrow{.} C be a cone in J (and hence orthogonal to Σ) and consider a cone Δ \underrightarrow{.} LP.

We have the following cube

D C  Σ1 Γ  P LP Δ

where C → Σ is the unique mediating morphism between Δ \underrightarrow{.} C and Δ \underrightarrow{.} LP → Σ.

We show that C → LP mediates between Δ \underrightarrow{.} C and Δ \underrightarrow{.} LP if and only if, for D → P the unique mediating morphism between Γ \underrightarrow{.} D (which, by stability, is in J and hence orthogonal to P) and Γ \underrightarrow{.} P, we have

D  P LP C  .

(⇒) Assume C → LP mediates between Δ \underrightarrow{.} C and Δ \underrightarrow{.} LP . Then, C → LP → Σ mediates between Δ \underrightarrow{.} C and Δ \underrightarrow{.} LP → Σ and hence (C → LP → Σ) = (C → Σ).

Thus we have

D C  Σ1 P LP

for a unique D → P. Moreover, (Γ \underrightarrow{.} D → P ↪ LP) = (Γ \underrightarrow{.} P ↪ LP) and hence D → P mediates between Γ \underrightarrow{.} D and Γ \underrightarrow{.} P. (⇐) Assuming

D  P LP C

for D → P the unique mediating morphism between Γ \underrightarrow{.} D and Γ \underrightarrow{.} P, we have

Γ  P Δ  LP D C

and since P ↪ LP classifies ⊤-partial maps (see [Hyl91]), C → LP mediates between Δ \underrightarrow{.} C and Δ \underrightarrow{.} LP. □

(1d) The embedding C ↪ RC preserves the initial object and the pullback

1 Σ⊤ 0 1 ⊥  .

(2) Because:

• RC is cartesian closed, by Theorem 11.12 and Proposition 11.10 (which applies as, by construction, J is closed under parameterisation).

• Every lifting monad on a category with a strict initial object satisfies Assumption 2 (see Proposition 3.1).

• Axioms 1, 3, 4, 5 state that the basic cones, except for the first one, are colimiting and, by Theorem 11.5, this requirement is preserved by C ↪ RC.

• Axiom 2 is equational and hence preserved by C ↪ RC.

(3) The main difficulty is verifying that the embedding RC ↪ [C_{⊑}^{op}, Cpo_{⊑}] lifts to a Cpo-embedding R(C)_{⊑} ↪ [C_{⊑}^{op}, Cpo_{⊑}]_{⊑}; i.e. that the path order in RC coincides with the pointwise pointwise order. Precisely, we show that, α ⊑ β : P → Q in R(C)_{⊑} if and only if, for all C ∈ | C | and all h : C → P in R(C)_{⊑}, α ∘ h ⊑ β ∘ h : C → Q in R(C)_{⊑}.

(⇒) By the monotonicity of composition with respect to the path relation.

(⇐) By assumption, for every C ∈ | C | and every h : C → P in R(C)_{⊑} there exists (a unique) p_{h} : Σ×C → Q in R(C)_{⊑} such that p_{h}∘⟨⊥∘(C → 1), C⟩ = α∘h and p_{h}∘⟨⊤∘(C → 1), C⟩ = β ∘h.

As every presheaf is (canonically) a colimit of representables, we have a colimiting cone ⨿ : Δ \underrightarrow{.} P with Δ : ∫_{C} P → C. Thus, for each k ∈ | ∫_{C} P |, there exists p_{⨿_{k}} : Σ × Δ_{k} → Q such that p_{⨿_{k}} ∘ ⟨⊥ ∘ (Δ_{k} → 1), Δ_{k}⟩ = α ∘ ⨿_{k} and p_{⨿_{k}} ∘ ⟨⊤ ∘ (Δ_{k} → 1), Δ_{k}⟩ = β ∘ ⨿_{k}. Moreover, for each e : i → j in ∫_{C} P, we have that p_{⨿_{j}} ∘ (Σ × Δe) ∘ (⊥ × Δ_{i}) = α ∘ (1 × ⨿_{i}) and p_{⨿_{j}} ∘(Σ×Δe)∘(⊤×Δ_{i}) = β ∘(1×⨿_{i}) so that, by the unique proofs axiom, p_{⨿_{j}} ∘(Σ×Δe) = p_{⨿_{i}} and hence we have a cone p_{⨿} : Σ × Δ \underrightarrow{.} Q with Σ × Δ : ∫_{C} P → C.

Finally, letting p : Σ × P → Q be the unique mediating morphism in

Σ × Δ Q Σ × P Σ × ⨿  p_{⨿} p

we are done, because

Δ ≅ 1 × Δ P ≅ 1 × P ⨿  1 × Δ⊥ × Δ ⊥ × PΣ × ⨿  Q p_{⨿} p Σ × Δ Σ × P α ∘ ⨿

so that p ∘ ⟨⊥ ∘ (P → 1), P ⟩ = α, and similarly p ∘ ⟨⊤ ∘ (P → 1), P ⟩ = β.

(4) By Corollary 11.6. □

The representation theorem incorporates the axiomatic approach into the scenario of synthetic domain theory in that RC (and hence C) may be regarded as a category of sets with and intrinsic cpo structure with respect to which all functions are continuous. The intrinsic cpo structure of a variable set [Law75, Sco80] P in RC manifests as follows: P Σ_{n} (n ≥ 0) is a set of chains with n + 1 elements (so that, in particular, P 1 is an underlying set of elements partially ordered by ⟨P ⊥, P ⊤⟩ : P Σ ↣ P 1×P 1); and P \overline{ω} is a set of ω-chains with lub operator P ∞ : P \overline{ω} → P 1.

Remark. Implicit in our development there is a family of representation theorems with respect to O(PC, J) with J a class of colimiting cones in C containing the basic cones and closed under parameterisation and stability. For example, C is also represented in R_{c}C (a full reflective subcategory of RC) defined by orthogonality with respect to the class of all colimiting cones in C. However, the variable sets in R_{c}C are more difficult to grasp than those in RC.

Example 11.17 Two categories to which our representation theorem applies are SFP (the category of bifinite domains and continuous functions) and Split(Cpo(Pℕ, Pℕ))_{∗} (the idempotent splitting of the monoid of continuous endomorphisms on Pℕ with an initial object added freely). □

12 Stability

Though indirectly, it is possible to incorporate stability in our axiomatic framework (details will be reported elsewhere). However, as we argue below, it is best to abandon Cpo-enrichment.

The analysis of Sections 7 and 8 suggests considering the following:

Definition 12.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 12.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. We conclude that Cpo-enrichment is not the natural setting for stability.

Remark. An abstract approach to “formal cpos” generalising the construction of Definition 12.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.

Acknowledgements

Conversations with Gordon Plotkin, John Power and Pino Rosolini on axiomatic domain theory, category theory and synthetic domain theory are gratefully acknowledged.

References

[AJ96] 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.

[BBHdP93] 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.

[Bor94a] F. Borceux. Handbook of Categorical Algebra I: Basic Category Theory. Cambridge University Press, 1994.

[Bor94b] F. Borceux. Handbook of Categorical Algebra III: Categories of Sheaves. Cambridge University Press, 1994.

[CP92] R.L. Crole and A.M. Pitts. New foundations for fixpoint computations: FIXhyperdoctrines and the FIX-logic. Information and Computation, 98:171–210, 1992.

[CPR91] 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.

[Fio95] 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.

[Fio96] M.P. Fiore. Axiomatic domain theory in categories of partial maps. To be published by Cambridge University Press in the Distinguished Dissertations Series. (Ph.D. thesis, Department of Computer Science, University of Edinburgh, 1994.), 1996.

[FJM^{+}96] 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. To appear in the Bulletin of the European Association for Theoretical Computer Science. (Technical Report CSR-96-2, The University of Birmingham, School of Computer Science —available from ftp://ftp.cs.bham.ac.uk/pub/techreports/1996/CSR-96-02.ps.gz), 1996.

[Fre91] P.J. Freyd. Algebraically complete categories. In [CPR91], pages 131–156, 1991.

[HP79] M. Henessy and G. Plotkin. Full abstraction for a simple parallel programming language. Lecture Notes in Computer Science, 74, 1979.

[Hyl91] J.M.E. Hyland. First steps in synthetic domain theory. In [CPR91], pages 95–104, 1991.

[Kel82] G.M. Kelly. Basic Concepts of Enriched Category Theory. Cambridge University Press, 1982.

[Koc70] A. Kock. Monads on symmetric monoidal closed categories. Arch. Math. (Basel), 21:1–10, 1970.

[Law75] F.W Lawvere. Continuously variable sets: algebraic geometry = geometric logic. In H.E. Rose and Shepherdson J.C., editors, Logic Colloquium ’73. North-Holland, 1975.

[LM92] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992.

[Pho90] W. Phoa. Domain Theory in Realizability Toposes. PhD thesis, Trinity College, Cambridge, 1990. (Also CST-82-91, University of Edinburgh).

[Ros80] G. Rosolini. Internal properties of structures in topoi. Dissertation presented for the D. Phil qualifying examination, Mathematical Institute, University of Oxford, September 1980.

[Ros86] G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986.

[Sco70] D.S. Scott. Outline of a mathematical theory of computation. Technical Report PRG-2, Oxford Univ. Computing Lab., 1970.

[Sco80] D.S. Scott. Relating theories of the λ-calculus. In R. Hindley and J. Seldin, editors, To H.B. Curry: essays in Combinatory Logic, lambda calculus and Formalisms. Academic Press, 1980.

[Tay91] P. Taylor. The fixed point property in synthetic domain theory. In 6^{th} LICS Conference, pages 152–160. IEEE, 1991.

[Tay94] P. Taylor. Synthetic domain theory notes. Manuscript, 1994.