Liminf convergence in Ω-Categories

Kim Ritter Wagner University of Cambridge, Computer Laboratory New Museums Site, Pembroke Street Cambridge CB2 3QG, UK e-mail: Kim.Wagner@cl.cam.ac.uk

June 9, 1995

The aim of this article is twofold. From a mathematical perspective we present a notion of convergence which is suitably general such as to include the convergence of chains to their least upper bounds in preordered sets, and the convergence of Cauchy sequences to their metric limits in metric spaces. Rather than presenting this theory from a purely mathematical perspective however, we will use it to introduce a simple-minded domain theory based on a generic notion of approximation. We might hope that this is not the only use of the concepts we present, although it is the one that motivated us in the first place.

One possible kind of approximation one uses in domain theory as it is used in the study of denotational semantics of programming languages is the binary one that we have in preorders: either an element is below another in the preordering, or it is not. Another kind of approximation is the metric one, where we do not just say whether one element approximates another, but to which degree it does so, with a non-negative real number.

It turns out that we can separate out from a large part of domain theory considerations about a particular notion of approximation, and just state a few axioms that should hold about a notion of approximation. In this general theory, which encompasses preorders and metric spaces among many other kinds of structures, we can then do general domain theory. The requirements for our notion of approximation turns out to be that of a quite well-known mathematical structure, viz. that of a commutative, unital quantale. One such quantale is the two point lattice, which gives rise to the theory of preorders, and another is that of the non-negative real numbers, turned up-side down, giving rise to generalized metric spaces. The advantage of this separation of concerns is obvious: we can see more easily what is common in different brands of domain theory, and what is specifically dependent on the kind of approximation one uses.

The initial part of the machinery that we just sketched is well-known as the (even more general) theory of enriched categories ([Eilenberg & Kelly 66]). At the core of our contribution is the concept of convergence (liminf) which unifies least upper bound of chains in preorders with metric limit of Cauchy sequences in metric spaces. This enables us to carry through a straightforward unification of the partial order and the metric approaches to domain theory, employing only basic lattice theory. We show the scope of the unification by providing one general proof for Scott’s inverse limit theorem, which subsumes both Scott’s original proof in the partial order setting (see e.g. [Lambek & Scott 86] Chapter 18) and America and Rutten’s proof in the metric setting ([America & Rutten 87]). Much of the background to this note is elaborated in the authors PhD thesis, [Wagner 94], although the formulation of convergence has been streamlined in this document.

The first step in establishing the theory is to use Lawvere’s insight ([Lawvere 73]) that the notion of an enriched category is a unifying concept for among many other structures, (generalized) metric spaces and preorders. The difference is in which structure one enriches over. If the structure one enriches over (the base category), Ω, is the two-point lattice, then the category of Ω-enriched categories and Ω-functors is precisely the category of preorders and monotone maps, and if Ω is the extended non-negative reals, [0, ∞], with the opposite ordering than the real numbers, and equipped with + as tensor, one obtains the category of generalized metric spaces and conservative (non-expansive) maps.

The second step is to unify the notion of least upper bound of chains with metric limit of Cauchy sequences. This is where the notion of liminf of sequences in enriched categories comes in. It is clear that one can not just take the categorical notion of Cauchy completeness ([Lawvere 73]) as the unifying concept for metric completeness and chain completeness. The reason is that this notion renders all preorders complete. It only works in the symmetric case. It turns out however, that it is possible to define a unifying notion of convergence. Using this we define completeness and continuity and prove a general version of Scott’s inverse limit theorem.

In Section 1 we give an outline of the basic theory of Ω-categories, which is a special case of enriched categories. In Section 2 we present our notion of convergence in Ω-categories, and state some basic properties of this kind of convergence. Section 3 is devoted to a Fubini-like theorem concerning our notion of convergence and is in a sense the conclusion of the presentation of the theory proper. The three following sections are further considerations and an application. They are reasonably independent, and any can be skipped by the reader. Section 4 shows how the notion of Scott open subsets and Scott continuous functions can be refound in our more general setting, and Section 5 gives a categorical account of our notion of convergence. Finally Section 6 contains our general version of Scott’s inverse limit theorem.

It is far from obvious what the right way of presenting this theory is. The main question is how much category theoretical language to use. On the one hand, readers with a strong background in category theory are bound to be impatient with a more pedestrian approach, but on the other hand many readers without such a strong background will necessarily be prohibited from understanding the material if it relies heavily on categorical notions. I have therefore chosen to use a certain minimum of category theory, where it has an immediate benefit towards brevity of reasoning, not just brevity of expression. Another issue is how much detail to include. Many of the calculations do not require much more than mindless rewriting following a few rules given by a few basic properties of the structures in question, and are really rather trivial. Here I have chosen to err on the side of giving too much detail, since the impatient reader always has the option of skipping the more tedious parts of the proofs.

I wish to extend my thanks to Valeria de Paiva and Andrew Pitts for a thorough reading of a draft of this paper.

1 Ω-categories

We aim initially at unifying partial orders with metric spaces, and by accepting generalizations of both notions we have a unifying concept ready at hand: enriched categories ([Lawvere 73]). The following two definitions lead up to the general concept.

Definition 1.1 A preorder is a pair (A_{0}, [ ≤ ]) where A_{0} is a set and [ ≤ ] : A_{0} × A_{0} → 2, where 2 stands for the two point lattice {t, f} with f ≤_{2} t, and where [ ≤ ] is reflexive: [a ≤ a] = t for all a, and transitive: [a ≤ b] ∧ [b ≤ c] ≤_{2} [a ≤ c].

For morphisms between preorders (A_{0}, [ ≤_{A} ]) and (B_{0}, [ ≤_{B} ]) we consider the monotone functions on the underlying sets, i.e. the mappings f : A_{0} → B_{0} such that [a ≤_{A} a′] ≤_{2} [f(a) ≤_{B} f(a′)]. We will denote the category of preorders and monotone maps PreOrd. □

We should remark that we have identified in the above, the underlying set of 2 with the lattice. Normally, when we wish to emphasize that we are talking about the underlying set of some structure, we use subscript 0, as in A_{0}.

Lawvere coined in [Lawvere 73] the name for the following structures.

Definition 1.2 A generalized metric space is a pair (A_{0}, d) where A_{0} is a set and d : A_{0}×A_{0} → [0, ∞], where [0, ∞] is the interval of non-negative real numbers, extended with infinity and with the opposite ordering as the usual real numbers, and where d is reflexive: d(a, a) = 0 and transitive: d(a, b) + d(b, c) ≤_{[0,∞]} d(a, c).

For morphisms between generalized metric spaces (A_{0}, d_{A}) and (B_{0}, d_{B}) we consider the conservative functions on the underlying sets, i.e. the mappings f : A_{0} → B_{0} such that d_{A}(a, a′) ≤_{[0,∞]} d_{B}(f(a), f(a′)). We will denote the category of generalized metric spaces and monotone maps GMet. □

Reflexivity and transitivity for the distance function in generalized metric spaces are two of the well-known axioms for metric spaces, viz. identity and the triangular inequality. Compared with the usual axioms for metric spaces we miss symmetry and separation (d(a, b) = 0 implies a = b), but one can do a lot with the weaker generalized structures. In particular, as we show in this article, one can do domain theory.

It should be evident from the above that the class of preorders and generalized metric spaces are generated following the same pattern, only using a different ‘basis’: In the one case one uses (2, ≤, ∧) and in the other ([0, ∞], ≥, +). It should come as no surprise that these are not the only ‘bases’ (henceforth to be called base categories) that can be used. In fact the general theory of enriched categories permits the base category to be a proper (monoidal closed) category, not just a lattice. In order to make the exposition more accessible we refrain from this generality here, thus working with lattice theoretic meets and joins instead of categorical limits and colimits. We believe that by doing so we exclude many interesting examples and an extension to the more general case is an obvious future task. Sticking with particular lattices, systematically named Ω in the following, as base categories, we call our enriched categories Ω-categories.

We give the basic definitions limiting the class of allowable Ω and of Ω-categories.

Definition 1.3 A complete lattice Ω is called a commutative quantale when it has a commutative and associative monotone operation, tensor, ⊗ : Ω × Ω → Ω such that p ⊗ has a right adjoint for every p ^{∈} Ω. We will call this right adjoint p ⊸ . A commutative quantale is called unital if the tensor has a unit 1, that is, p ⊗ 1 = p for all p. □

Henceforward, Ω will denote a commutative, unital quantale.

Remark 1.4 Since we will use it so often, it is worth spelling out that the adjunction requirement above, p ⊗ ⊣ p ⊸ for every p, is to say (using commutativity) that p ⊗ q ≤ r if and only if p ≤ q ⊸ r. Also, remember that left-adjoints preserve colimits and right-adjoints limits, in other words p ⊗ ⋁_{i} q_{i} = ⋁_{i} p ⊗ q_{i} and p ⊸⋀_{i} q_{i} = ⋀_{i} p ⊸ q_{i}.

It is also worth remarking that very often in the examples we will consider, the unit, 1, of the tensor will be the top element, ⊤, of Ω, but that this need not be the case.

Also, remember that every complete lattice is a partial order, not just a preorder, so equality in Ω is really equality, not just isomorphism. □

Definition 1.5 A category enriched over Ω (or Ω-category) is a pair, (A_{0}, [ , ]) where A_{0} is a set and where the second component (usually called the hom functor) to every two elements a, a′ ^{∈} A_{0}, yields an element [a, a′] ^{∈} Ω, such that 1 ≤ [a, a] for every a ^{∈} A_{0} (reflexivity) and [a, b] ⊗ [b, c] ≤ [a, c] for all a, b, c ^{∈} A_{0} (transitivity). □

Obviously we can generalize Definition 1.5 to large enriched categories, in that we allow the first component to be a proper class. This will enable us to consider for instance the collection of retracts of a domain as an Ω-category. However, not all the constructions in the sequel are applicable to large Ω-categories, and unless otherwise stated, the Ω-categories in the sequel will be small, that is, their underlying class A_{0} will be a set, and we will explicitly emphasize if an Ω-category A is large. When we wish to emphasize the name of the Ω-category, A say, we write A[ , ] for the hom functor. As usual, we denote by A^{op} the Ω-category with the same underlying class, but with A^{op}[a, a′] = A[a′, a].

Definition 1.6 An Ω-functor between Ω-categories A and B is a function f : A_{0} → B_{0} where A[a, a′] ≤ B[f(a), f(a′)] for all a, a′ ^{∈} A_{0}. □

Ω-functors are composed by composing the underlying functions on sets, and it is clear that the class of small Ω-categories and Ω-functors form a category. We denote it Ω-CAT. Whenever we in the sequel form categories of Ω-categories, it will be understood that we only consider the small Ω-categories.

Example 1.7 Let Ω = 2, the two point lattice, with ⊗ = ∧. The category of 2-enriched categories and 2-functors is the category PreOrd of preorders and monotone maps from Definition 1.1. □

Example 1.8 Let Ω = [0, ∞] with the opposite ordering as the reals (so 0 is the greatest element) and + as tensor. We find that the adjoint to p + is . −p, where . − is truncated subtraction, and where the operations are extended to cope with infinity such that ∞ . −∞ = 0 and everything else is as expected. In this case the category of Ω-categories is the category GMet of generalized metric spaces and conservative maps from Definition 1.2. □

Example 1.9 The non-negative real numbers can be equipped with other tensors than +. Take for example ⊗ as max. Transitivity now reads max{d(a, b), d(b, c)} ≥_{[0,∞]} d(a, c). The Ω-categories for this Ω are precisely the (generalized) ultra-metric spaces. □

Thus we see that Ω-categories will take the place of domains in our discussion, though we will have to impose restrictions on them, corresponding to the completeness requirements one imposes on pre-orders or metric spaces (chain and Cauchy completeness, respectively) in order to obtain feasible domains for recursive domain equations.

Observation 1.10 It is easy to see that (Ω, ⊸) is itself an Ω-category, which justifies that we sometime write [p, q] for p ⊸ q. It is an easy exercise to see that [ , p] is a Ω-functor from (Ω, ⊸)^{op} to (Ω, ⊸), and that [p, ] and p ⊗ are endo-functors on (Ω, ⊸). We will often confuse Ω as a quantale with (Ω, ⊸) as an Ω-category, writing Ω for both. □

The tensor from Ω lifts to Ω-categories thus.

Definition 1.11 Given Ω-categories, (A_{0}, A[ , ]) and (B_{0}, B[ , ]) we can form the Ω-category called their tensor product, A ⊗ B, with set part A_{0} × B_{0}, the Cartesian product of their underlying sets, and hom functor part (A ⊗ B)[(a, b), (a′, b′)] = A[a, a′] ⊗ B[b, b′]. □

The linear implication (⊸) from Ω lifts as follows.

Definition 1.12 We write f : X ⊸ Y when f is an Ω-functor from X to Y. Given Ω-categories X and Y we can form the Ω-category [X, Y], the Ω-category with set part all the Ω-functors from X to Y and with hom functor part

[X, Y][f, g] = ⋀_{x^{∈}X_{0}} Y [f(x), g(x)].

□

Proposition 1.13 Given an Ω-category A, the hom functor A[ , ] is an Ω-functor from A^{op} ⊗ A to Ω.

Proof : Easy. □ The adjunction a ⊗ ⊣ a ⊸ in Ω lifts as well, implying that Ω-CAT is a monoidal closed category.

Proposition 1.14 For every Ω-category A it holds that A ⊗ ⊣ [A, ] (see e.g. [Eilenberg & Kelly 66]). □

We remarked in [Wagner 94] that Ω-CAT is Cartesian closed if and only if Ω is a complete Heyting algebra with ⊗ as meet. (This is by no means a new observation.)

Interestingly for domain theory, the category Ω-CAT also has finite coproducts.

Proposition 1.15 The coproduct X + Y for two Ω-categories X and Y is (({0}×X_{0}) ∪ ({1}×Y_{0}), [ , ]), where [(0, x), (0, x′)] = X[x, x′], [(1, y), (1, y′)] = Y [y, y′], and [(i, z), (j, v)] = ⊥ for i ≠ j, together with the injections inX : X ⊸ (X + Y) and inY : Y ⊸ (X + Y) defined by inX(x) = (0, x) and inY (y) = (1, y).

Proof : Let X, Y and Z be Ω-categories with f : X ⊸ Z and g : Y ⊸ Z. We define (f, g) : (X +Y) ⊸ Z by (f, g)(0, x) = f(x) and (f, g)(1, y) = g(y). It is obviously the unique morphism that will make f = (f, g) ∘ inX and g = (f, g) ∘ inY, so existence and uniqueness in no problem, as long as we can show that (f, g) is a morphism. To see this we have to check that [(f, g)(i, z), (f, g)(j, v)] ≥ [(i, z), (j, v)], which is obvious for i = j, so assume without loss of generality that i = 0 and j = 1. Then we need to show [f(z), g(v)] ≥ ⊥, which is trivially the case. □

Observation 1.16 Ω-CAT has a terminal object, the Ω-category with one element, ∗, and [∗, ∗] = ⊤_{Ω}. We denote this Ω-category by 1l. The morphism from X into 1l is denoted by ·_{X}. When ⊤ = 1 there is a one-to-one correspondence between Ω-functors from 1l to A and elements of A_{0}; a confusion we will use for notational convenience whenever appropriate. □

There is an object in the category Ω-CAT which plays the role of the natural numbers. There are several ways of defining it. Probably the simplest, though not the one starting from elementary categorical concepts is the following.

Definition 1.17 By ℕ we denote the Ω-category ({0, 1, 2, … }, [ , ]), where ℕ[n, m] is ⊤ if n = m, and ⊥ (the least element of Ω) otherwise. We also define \underline{0} : 1l ⊸ ℕ as \underline{0}(∗) = 0, and succ : ℕ ⊸ ℕ in the obvious way (which we could make precise if we were precise about the component {0, 1, 2, … }.) □

We could also have defined the natural numbers in a categorical style, using coproducts ([Freyd 90]). Consider the endo-functor + 1l in Ω-CAT which sends an Ω-category A into A + 1l and an Ω-functor f : A ⊸ B into f + id1l = ((inB ∘ f), in1l) : (A + 1l) ⊸ (B + 1l) according to the following diagram

[figure: B; A; B + 1l; A + 1l; 1l; 1l; f; inA; inB; ^{in1l}; _{in1l}; ^{id1l}; f + id1l]

Proposition 1.18 (ℕ, (succ, \underline{0})) is uniquely characterized as the initial algebra for the functor + 1l.

Proof : Easy. □ Spelled out Proposition 1.18 says that ℕ is an Ω-category, and that \underline{0} : 1l ⊸ ℕ and succ : ℕ ⊸ ℕ are Ω-functors such that for any Ω-category A and any Ω-functors a : 1l ⊸ A and f : A ⊸ A there are unique Ω-functors s : (ℕ + 1l) ⊸ (A + 1l) and t : ℕ ⊸ A such that the following diagram commutes.

[figure: A; A + 1l; ℕ; ℕ + 1l; (f, a); t; s; (succ, \underline{0})]

It is also easy to see that the natural numbers thus defined are a (strong) natural numbers object in the sense of Lawvere (see e.g. [Lambek & Scott 86]). This is to say that for every a : 1l ⊸ A and every f : A ⊸ A there are unique g, h : ℕ ⊸ A such that the following diagram commutes.

[figure: 1l; 1l; A; ℕ; A; ℕ; ^{id1l}; a; \underline{0}; g; succ; f; h]

Remark 1.19 Notice, how we here have an indication that the cases with ⊤ = 1 will be the most convenient – the commutativity of the above diagram really only speaks about the elements a(∗), f(a(∗)), f(f(a(∗))), …, which all are points x where [x, x] = ⊤.

2 Convergence of sequences and completeness of domains

In denotational semantics it is most often the case that the (co)limits that occur arise from countable sequences, be it sequences of elements in a structured set such as a cpo or a metric space, or be it sequences of domains as resulting from iterated application of a functor in a category of domains. We will therefore restrict ourselves at this point to consider just sequences and their convergence, not e.g. directed sets. Thus our notions of continuity and completeness will also be based on countable sequences.

Concerning completeness, in [Lawvere 73] Lawvere introduces the notion of Cauchy completeness for enriched categories, but this notion renders all preorders Cauchy complete, and it is thus clear that we cannot use his definition to unify chain completeness and Cauchy completeness (in the standard metric sense). In [Wagner 94] we carried the notion of Cauchy sequence over basically verbatim from traditional metric spaces to Ω-categories, and gave our notion of convergence for such sequences. We can now do slightly better, using a more general notion of Cauchy sequence that still generalizes chains and Cauchy sequences in metric spaces, but which renders the ensuing theory more elegant and general. We need a few elementary observations on sequences of elements of an Ω-category first, though.

Definition 2.1 By a sequence of elements of an Ω-category A we mean an Ω-functor α : ℕ ⊸ A. We will usually write an element of a sequence, α(n) say, as α_{n}. □

Thus we write [ℕ, A]_{0} for the set of sequences in A.

First we establish two elementary lemmas about sequences in quantales or more generally complete lattices. The first (Lemma 2.2) says that prefixes are irrelevant when we consider ‘liminfs’ of sequences in a complete lattice. The second (Lemma 2.3) says roughly that given two increasing sequences in Ω, when we want the join of all combinations of an element from one and an element from the other sequence, it is enough to consider just the diagonal.

Lemma 2.2 For any sequence (x_{n})_{n^{∈}ℕ} of elements in a complete lattice, ⋁_{N^{∈}ℕ} ⋀_{n≥N} x_{n} = ⋁_{N≥M} ⋀_{n≥N} x_{n} for any M ^{∈} ℕ.

Proof :

⋁_{N^{∈}ℕ} ⋀_{n≥N} x_{n} ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥max{N,M}}x_{n} = ⋁_{N≥M} ⋀_{n≥N} x_{n} ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} x_{n}.  □

Lemma 2.3 For increasing sequences x_{0} ≤ x_{1} ≤ … and y_{0} ≤ y_{1} ≤ … in Ω we have

⋁_{n^{∈}ℕ} (x_{n} ⊗ y_{n}) = ( ⋁_{n^{∈}ℕ} x_{n}) ⊗ ( ⋁_{n^{∈}ℕ} y_{n}) .

Proof : ‘≤’ is obvious, and ‘≥’ is easy to see as follows:

⋁_{n^{∈}ℕ} (x_{n} ⊗ y_{n}) = ⋁_{n^{∈}ℕ} ⋁_{m^{∈}ℕ} (x_{max{n,m}} ⊗ y_{max{n,m}})
≥ ⋁_{n^{∈}ℕ} ⋁_{m^{∈}ℕ} (x_{n} ⊗ y_{m})

= ( ⋁_{n^{∈}ℕ} x_{n}) ⊗ ( ⋁_{n^{∈}ℕ} y_{n}) .

where the inequality is due to the sequences being increasing (and ⊗ being covariant in both its arguments). The argument of course goes through for any covariant bifunctor which preserves joins in each argument, instead of ‘⊗’. □

In addition to using the hom-functor [ℕ, A] is ‘born’ with, viz. [α, β] = ⋀_{n^{∈}ℕ}[α_{n}, β_{n}], we can compare two sequences α, β : ℕ ⊸ A by considering ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, β_{n}]. Considering the special case of sequences in preorders, we thus go from saying that α ≤ β if it is so index for index to saying that α ≤ β if it is so (index for index) from some point (N) on. For the special case of metric spaces, we go from saying that the distance between two sequences α and β is the supremum of the distance between α_{n} and β_{n} taken over all indices, to being the limsup (in the metric sense) of d(α_{n}, β_{n}) for n → ∞. That this is a nice way of comparing sequences in our general setting follows from Lemma 2.4 below.

Lemma 2.4 The pair ([ℕ, A]_{0}, ⋁_{N} ⋀_{n≥N}[ _{n}, _{n}]) is an Ω-category and ⋁_{N} ⋀_{n≥N}[ _{n}, _{n}] is an Ω-functor from ([ℕ, A]^{op} ⊗ [ℕ, A]) to Ω.

Proof : We want to show reflexivity and transitivity of the Ω-valued relation ⋁_{N} ⋀_{n≥N}[ _{n}, _{n}]. Reflexivity is obvious, and to see transitivity we calculate as follows.

⋁_{N} ⋀_{n≥N}[α_{n}, γ_{n}] ≥ ⋁_{N} ⋀_{n≥N}[α_{n}, β_{n}] ⊗ [β_{n}, γ_{n}]

≥ ⋁_{N} ( ⋀_{n≥N}[α_{n}, β_{n}]) ⊗ ⋀_{n≥N}[β_{n}, γ_{n}]

= (⋁_{N} ⋀_{n≥N}[α_{n}, β_{n}]) ⊗ ⋁_{N} ⋀_{n≥N}[β_{n}, γ_{n}].

Here we have the latter inequality by Lemma 2.3.

To see that ⋁_{N} ⋀_{n≥N}[ _{n}, _{n}] is an Ω-functor from ([ℕ, A]^{op} ⊗ [ℕ, A]) to Ω we have to show that for sequences α, β, γ, δ : ℕ ⊸ A we have [α, β] ⊗ [γ, δ] ⊗ ⋁_{N} ⋀_{n≥N}[β_{n}, γ_{n}] ≤ ⋁_{N} ⋀_{n≥N}[α_{n}, δ_{n}], but this is easy to see. □

Lemma 2.4 makes the following definition legal.

Definition 2.5 We denote by seq(A) the Ω-category ([ℕ, A]_{0}, ⋁_{N} ⋀_{n≥N}[ , ]). The diagonal functor embedding A into seq(A), mapping an element a ^{∈} A_{0} into \overline{a} = (a, a, a, …) is denoted Δ. □

Consider preorders (2-enriched categories). In this case, for two sequences α and β of a preorder, 1 ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, β_{n}] if and only if there exists N ^{∈} ℕ such that α_{n} ≤ β_{n} for all n ≥ N. A weaker way of comparing the two sequences would be not to require that β dominates α index for index after N, but eventually dominates every α_{n} after N, that is, ∃N ^{∈} ℕ. ∀n ≥ N. ∃M ^{∈} ℕ. ∀m ≥ M. α_{n} ≤ β_{m}. Generalizing to sequences in an Ω-category we consider ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{n}, β_{m}]. It is easy to see that this

is an Ω-functor from [ℕ, A]^{op} ⊗ [ℕ, A] to Ω.

Proposition 2.6 The relation ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[ _{n}, _{m}] : ([ℕ, A]^{op} ⊗ [ℕ, A]) ⊸ Ω is transitive.

Proof : Let α, β, and γ : ℕ ⊸ A be given. Then

( ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{K_{1}≥n} ⋀_{k≥K_{1}}[α_{n}, β_{k}]) ⊗ (⋁_{K_{2}} ⋀_{k≥K_{2}} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[β_{k}, γ_{m}])

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{K_{1}≥n} ⋁_{K_{2}} (( ⋀_{k≥K_{1}}[α_{n}, β_{k}]) ⊗ ⋀_{k≥K_{2}} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[β_{k}, γ_{m}])

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{K_{1}≥n} ⋁_{K_{2}} ([α_{n}, β_{max{K_{1},K_{2}}}] ⊗ ⋁_{M≥max{K_{1},K_{2}}} ⋀_{m≥M}[β_{max{K_{1},K_{2}}}, γ_{m}])

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{K_{1}≥n} ⋁_{K_{2}} ⋁_{M≥max{K_{1},K_{2}}} ⋀_{m≥M}[α_{n}, γ_{m}]

= ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{n}, γ_{m}].  □

Definition 2.7 A sequence α : ℕ ⊸ A is Cauchy if 1 ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{n}, α_{m}]. The full subcategory of seq(A), consisting of Cauchy sequences will be denoted cseq(A). □

Thus, the Cauchy sequences are precisely the sequences on which the relation ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[ _{n}, _{m}] is reflexive. This legitimates the following definition.

Definition 2.8 We denote by kseq(A) the Ω-category of Cauchy sequences in A with the relation

⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[ _{n}, _{m}].  □

Remark 2.9 We could call ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{n}, α_{m}] the extent of α (Inspired vaguely from the theory of Ω-sets ([Fourman & Scott 77])), to indicate how well α defines a unique point (its ‘liminf’), regardless of whether this point actually exists or not. The main difference when comparing to Ω-sets is that the extent here is defined in terms of a non-symmetric relation. □

Remark 2.10 Recall the notion of directed net from [Gierz et al. 80]: A function x from a directed set J into a set L equipped with a transitive relation ‘≤’ is called a directed net if for every i ^{∈} J there exists a j ^{∈} J such that for all k ≥ j, we have x(i) ≤ x(k).

Thus, what we call Cauchy sequences in A are really directed nets from (ℕ, ≤) into A, with a couple of generalizations. Firstly, we have generalized the two-valued relation ≤ to an Ω-valued one. Secondly, we have internalized the notion of directed net accordingly, and thirdly, we have generalized to nets which we could call eventually directed, since we require 1 ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{n}, α_{m}] and not 1 ≤ ⋀_{n^{∈}ℕ} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{n}, α_{m}]. □

Remark 2.11 Compare Definition 2.7 with the predicate 1 ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋀_{m≥n}[α_{n}, α_{m}] which was used in [Wagner 94], and which we now could call strongly Cauchy. For preorders the latter predicate expresses that from some point (N) the sequence is a chain. The former only that from some point (N) on, each element (α_{n}) is eventually (after M) dominated by a suffix of α. For such a sequence in a preorder, we easily see that we have a well-defined notion corresponding to least upper bound. Consider the unique sub-sequence β of α obtained by letting β_{0} = α_{N}, where N is the witness of ∃N ^{∈} ℕ. ∀n ≥ N. ∃M ^{∈} ℕ. ∀m ≥ M. α_{n} ≤ β_{m}, and β_{n+1} = α_{M}, where M is the witness for ∃M > n. ∀m ≥ M. β_{n} ≤ α_{m}. It is obvious that β is a chain, and any possible least upper bound of β can be taken as a ‘liminf’ of α. This will be made precise when we consider liminfs.

For an example of a sequence which is Cauchy, but not strongly Cauchy, consider the preorder consisting of the natural numbers with the normal ordering, and consider further the sequence 1, 3, 2, 4, 3, 5, 4, 6, …, alternatingly adding 2 and subtracting 1.

As a slightly more complicated example, take as A the unit square, [0, 1]×[0, 1] seen as a preorder, ordered coordinatewise, such that (0, 0) is the smallest element and (1, 1) the biggest, and thus, the shape is that of a diamond. Let α be any sequence with elements (x_{n}, y_{n}), where x_{n}, y_{n} ^{∈} [0, 1) such that x_{n} + y_{n} ≥ 2 − \frac{1}{n} for all n. The idea is that the points of α are required to be closer and closer to (1, 1), but not in a way which forces them to form a chain. We will leave it as an exercise to show that α is Cauchy, and that this need not have been the case, had we allowed x_{n} and y_{n} to be 1. □

Remark 2.12 It is clear that chains in preorders are Cauchy sequences in our sense. For Ω = [0, ∞]_{+}, the non-negative reals with the opposite ordering and with + as tensor, we saw that any Ω-category A is a generalized metric space, and we see that a sequence is strongly Cauchy if inf_{N^{∈}ℕ} sup_{n≥N} sup_{m≥n} d(α_{n}, α_{m}) = 0, which is equivalent to ∀ϵ > 0. ∃N ^{∈} ℕ. ∀m ≥ n ≥ N. d(α_{n}, α_{m}) ≤ ϵ, which is the usual definition of Cauchy sequences in metric spaces, extended to cope with non-symmetry. A sequence is Cauchy if and only if inf_{N^{∈}ℕ} sup_{n≥N} inf_{M^{∈}ℕ} sup_{m≥M} d(α_{n}, α_{m}) = 0. It is not difficult to see that for ordinary symmetric metric spaces this is equivalent to the usual definition of Cauchy sequence, but notice that this equivalence rests on fundamental and specific properties of the real numbers. □

Remark 2.13 The relation ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[ , ] is not idempotent in general. For an Ω-valued relation R : A^{op} ⊗ A ⊸ Ω to be idempotent we mean that for every a and c ^{∈} A_{0} we have R(a, c) ≤ ⋁_{b^{∈}A_{0}} R(a, b) ⊗ R(b, c), which is just to say (with suitable definition of composition of relations) that R ≤ R ∘ R. We need only consider preorders to find a counterexample. What we want is to find sequences α and β of a preorder, such that ∃N ^{∈} ℕ. ∀n ≥ N. ∃M ^{∈} ℕ. ∀m ≥ M. α_{n} ≤ β_{m}, but such that there is no γ such that ∃N ^{∈} ℕ. ∀n ≥ N. ∃M ^{∈} ℕ. ∀m ≥ M. α_{n} ≤ γ_{m} and ∃N ^{∈} ℕ. ∀n ≥ N. ∃M ^{∈} ℕ. ∀m ≥ M. γ_{n} ≤ β_{m}.

Take as an example the following preorder.

0x 1x 2x  2y 1y 0y 2b 1b 0b^{….} ^{….}^{.....}

Let β = (0b, 1b, 2b, …) and α = (0x, 0y, 1x, 1y, …). It is easy to see that they behave as we requested above: the only sequences ‘above’ α are sequences that from some point on consist entirely of elements of the form nb, and the only sequences ‘below’ β are sequences that from some point on consists entirely of elements of the form nx or ny. No sequence fulfills all those requirements. □

From Lemma 2.2 we have the following corollary.

Corollary 2.14 A sequence is Cauchy if and only if any one of its suffixes is, and in this case, all the suffixes are Cauchy. □

As a slogan, the property of being Cauchy is prefix independent.

It is also easy to see the following.

Proposition 2.15 Every subsequence of a Cauchy sequence is Cauchy. □

It is natural as a generalization of least upper bounds in preorders and metric limits in metric spaces to consider a liminf-like convergence. To make the presentation smoother we discuss representable Ω-functors briefly.

Definition 2.16 Given an Ω-category A, an Ω-functor ϕ : A ⊸ Ω (which you can think of as a covariant predicate, if you like, or as an ‘upward closed’ subset of A) is representable if there exists a ^{∈} A_{0} such that ϕ = [a, ]. In this case a is called the representing element. □

For example, in the case of preorders, ϕ = [a, ] means ϕ(b) iff a ≤ b, so ϕ is the characteristic function for ↑ a. In the case of generalized metric spaces, ϕ = [a, ] means that ϕ(b) is the distance from a to b. The representing element a is in a sense the ‘least’ element to fulfill ϕ. It is unique up to isomorphism. Naturally, with contravariant Ω-functors we have what we could call corepresentables, viz. those of the form [ , a].

We are now ready to define our notion of convergence.

Definition 2.17 A Cauchy sequence α : ℕ ⊸ A converges to a ^{∈} A_{0} if ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, ] = [a, ]. In this case we write a = lim inf α. □

We could just have said that ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, ] should be representable, and that in this case the representing element is the liminf.

The following easy proposition turns out to be very useful in various calculations in the sequel.

Proposition 2.18 Given an Ω-category A, an Ω-functor ϕ : A ⊸ Ω is representable if and only if

(i) ϕ(x) ≤ [a, x] for all x ^{∈} A_{0}, and

(ii) 1 ≤ ϕ(a).

Proof : Easy. □ As an immediate corollary of Proposition 2.18 we have the following.

Corollary 2.19 A Cauchy sequence α : ℕ ⊸ A converges to a ^{∈} A_{0} if and only if

(i) ⋀_{n≥N}[α_{n}, x] ≤ [a, x] for any N ^{∈} ℕ and any x ^{∈} A_{0},

(ii) 1 ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, a].

□

For preorders (Ω = 2) the first condition expresses that a is less than any upper bound of any suffix of α and the second condition says that a is an upper bound for some suffix.

For metric spaces the first condition says that the distance from the liminf a to any point x, is less than the supremum of the distances from any of the elements of any suffix of the sequence to x, and the second condition says that the distances from the elements of the sequence to a converge to 0.

We see that once we have the right categories set up, we can define lim inf as the left adjoint to Δ, the functor that maps x into the sequence with all elements equal to x. This gives us for free for instance that liminf preserves colimits.

Our definition of liminf completeness and continuity should not surprise anyone.

Definition 2.20 An Ω-category is liminf complete if every Cauchy sequence has a liminf. □

Definition 2.21 An Ω-functor is liminf continuous if it preserves liminfs of Cauchy sequences. □

Definition 2.22 We denote by Ω-CCAT the subcategory of Ω-CAT with liminf complete Ω-categories and liminf continuous Ω-functors. Given Ω-categories A and B we write [A, B]^{∘} for the Ω-category of liminf continuous Ω-functors with the hom functor inherited from [A, B]. □

Proposition 2.23 A sequence is liminf convergent if and only if any one of its suffixes is, and in this case all the suffixes are, and they all converge to the same element.

Proof : Obvious by Lemma 2.2. □ So, as desired, liminfs are also prefix independent.

Observation 2.24 If every Cauchy sequence (in our sense) in a preorder has a liminf then every chain (in the traditional sense) has a least upper bound. This is obvious, since every chain is a Cauchy sequence. More interestingly, if every chain in a preorder has a least upper bound, then every Cauchy sequence has a liminf. Take the Cauchy sequence. It has a chain as a subsequence, and you can just take the least upper bound of that chain, since – as is easy to see – every subsequence which is a chain necessarily has the same least upper bound. This least upper bound is the liminf of the Cauchy sequence. All this means that when we consider completeness, the preorder version of completeness we get as a special case of the above definitions is the same as the traditional one.

Concerning our second special case, (symmetric) metric spaces, it is even more straightforward that the old and the new completeness coincide, since the concept of Cauchy sequence is preserved. □

The following proposition shows that we could have replaced condition (ii) in Definition 2.17 with a dual to condition (i).

Proposition 2.25 A Cauchy sequence α : ℕ ⊸ A is convergent to a if and only if (i) ⋀_{n≥N}[α_{n}, x] ≤ [a, x] (as above) and (i^{op}) ⋀_{n≥N}[x, α_{n}] ≤ [x, a] for any N ^{∈} ℕ and any x ^{∈} A_{0}.

Proof : Assume that a Cauchy sequence α : ℕ ⊸ A is convergent to a, and let N ^{∈} ℕ and x ^{∈} A_{0} be given. We then have

⋀_{n≥N}[x, α_{n}] ≤ ( ⋀_{n≥N}[x, α_{n}]) ⊗ ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{m}, a]

= ⋁_{M^{∈}ℕ} ( ⋀_{n≥N}[x, α_{n}]) ⊗ ⋀_{m≥M}[α_{m}, a]

≤ ⋁_{M^{∈}ℕ}[x, α_{max{N,M}}] ⊗ [α_{max{N,M}}, a]
≤ [x, a].

On the other hand, assume that a Cauchy sequence α : ℕ ⊸ A fulfills (i) ⋀_{n≥N}[α_{n}, x] ≤ [a, x] and (i^{op}) ⋀_{n≥N}[x, α_{n}] ≤ [x, a] for any N ^{∈} ℕ and any x ^{∈} A_{0}. In this case, 1 ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{n}, α_{m}] ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, a], so it also fulfills (ii). □

We could also have replaced the join of a meet with a meet of a join, as the following theorem shows, reminiscent of the fact about real numbers that for convergent sequences, liminf is equal to limsup.

Theorem 2.26 For any Cauchy sequence α : ℕ ⊸ A, we have ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, x] = ⋀_{N^{∈}ℕ} ⋁_{n≥N}[α_{n}, x].

Proof : The inequality ‘≤’ is obvious, just by general properties of meets and joins. We can prove the other inequality using that α is Cauchy, as follows.

⋀_{K^{∈}ℕ} ⋁_{k≥K}[α_{k}, x] ≤ ( ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[α_{n}, α_{m}]) ⊗ ⋀_{K^{∈}ℕ} ⋁_{k≥K}[α_{k}, x]

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} (( ⋀_{m≥M}[α_{n}, α_{m}]) ⊗ ⋁_{k≥M}[α_{k}, x])

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋁_{k≥M} ( ⋀_{m≥M}[α_{n}, α_{m}]) ⊗ [α_{k}, x]

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋁_{k≥M} ([α_{n}, x])

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, x].  □

Remark 2.27 It is obviously tempting to try to mimic the situation in the real numbers and do away with the Cauchy condition and define a sequence α to be convergent to a if and only if ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, x] = ⋀_{N^{∈}ℕ} ⋁_{n≥N}[α_{n}, x] = [a, x] for all x. This elegant notion of convergence seems unfortunately at best to make it very difficult to prove the following theorems, such as the Fubini theorem (Theorem 3.1), at worst to make them false. Consider for illustration Example 2.28, where Ω = 2, and where we are thus dealing with preorders. The example illustrates how liberal the suggested convergence criteria is, but provides no counter example to e.g. the Fubini theorem. We have not been able to find such an example. □

Example 2.28 Let (A, ≤) be the ‘diamond’ [0, 1] × [0, 1] with (x, y) ≤ (u, v) if and only if x ≤ u and y ≤ v. Consider the sequence ((a_{n}, 1 − a_{n}))_{n^{∈}ℕ}, where (a_{n})_{n^{∈}ℕ} = (0, \frac{3}{4}, \frac{3}{8}, \frac{9}{16}, …), that is, a_{n} = \frac{1}{2} − (−1)^{n} · 2^{−n−1}. That is, in the sequence (a_{n})_{n^{∈}ℕ} we halve the distance to \frac{1}{2} each step in the sequence, and the elements are alternatingly greater than and less than \frac{1}{2}. Then all the points in α have the same sum of their coordinates, viz. 1, and so they are all unrelated. It is easy to see that ∃N ^{∈} ℕ. ∀n ≥ N. α_{n} ≤ x says that x ^{∈} (\frac{1}{2}, 1] × (\frac{1}{2}, 1], whereas ∀N ^{∈} ℕ. ∃n ≥ N. α_{n} ≤ x means that x ^{∈} [\frac{1}{2}, 1] × [\frac{1}{2}, 1] \ (\frac{1}{2}, \frac{1}{2}), and (\frac{1}{2}, \frac{1}{2}) ≤ x means that x ^{∈} [\frac{1}{2}, 1] × [\frac{1}{2}, 1].

Thus, if we removed from (A, ≤) the points that are \frac{1}{2} in one but not in both coordinates, then ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, x] = ⋀_{N^{∈}ℕ} ⋁_{n≥N}[α_{n}, x] (but not equal to [a, x]) for all x. The consequence would be that our sequence, consisting of entirely unrelated elements, would be convergent to (\frac{1}{2}, \frac{1}{2}) in this very relaxed form, and intuitively this seems quite plausible. Notice also, that if we view our structure not as a preorder, but as a (generalized) metric space, then the sequence above is convergent. □

It will be important that Ω itself, as an Ω-category, is liminf complete.

Remark 2.29 We have ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[x_{n}, x_{m}] = ⋁_{N} ⋀_{n≥N} ⋁_{M}[x_{n}, ⋀_{m≥M} x_{m}] ≤ ⋁_{N} ⋀_{n≥N}[x_{n}, ⋁_{M} ⋀_{m≥M} x_{m}] for ev-

ery sequence (x_{n})_{n^{∈}ℕ} in (Ω, ⊸). □

Proposition 2.30 The Ω-category (Ω, ⊸) is liminf complete, and lim inf_{n^{∈}ℕ} x_{n} = ⋁_{N^{∈}ℕ} ⋀_{n≥N} x_{n} for any sequence of elements x_{n} in Ω.

Proof : We want to prove that [⋁_{N} ⋀_{n≥N} x_{n}, y] = ⋁_{N} ⋀_{n≥N}[x_{n}, y] for every Cauchy sequence (x_{n})_{n^{∈}ℕ} in (Ω, ⊸) and every y ^{∈} Ω.

To see ‘≤’, note that [⋁_{N} ⋀_{n≥N} x_{n}, y] ≤ (⋁_{N} ⋀_{n≥N}[x_{n}, ⋁_{M} ⋀_{m≥M} x_{m}]) ⊗ [⋁_{N} ⋀_{n≥N} x_{n}, y] ≤ ⋁_{N} ⋀_{n≥N}[x_{n}, y]. Here

we have the first inequality by Remark 2.29 and the second by (⋁_{N} ⋀_{n≥N}[x_{n}, z])⊗[z, y] ≤ ⋁_{N} ⋀_{n≥N}[x_{n}, y], which is a special case of Lemma 2.4.

To see ‘≥’ we first observe that [1, x] = x for all x ^{∈} Ω, and then that [⋁_{N} ⋀_{n≥N} x_{n}, y] ≥ ⋁_{N} ⋀_{n≥N}[x_{n}, y]

by adjointness is equivalent to y ≥ (⋁_{N} ⋀_{n≥N} x_{n}) ⊗ ⋁_{N} ⋀_{n≥N}[x_{n}, y], which is true since (⋁_{N} ⋀_{n≥N} x_{n}) ⊗

⋁_{N} ⋀_{n≥N}[x_{n}, y] = (⋁_{N} ⋀_{n≥N}[1, x_{n}]) ⊗ ⋁_{N} ⋀_{n≥N}[x_{n}, y] ≤ ⋁_{N} ⋀_{n≥N}[1, y] = y. □

Accordingly, for any convergent sequence (f_{n})_{n^{∈}ℕ} in [A, Ω] we have lim inf_{n^{∈}ℕ} f_{n} = ⋁_{N^{∈}ℕ} ⋀_{n≥N} f_{n}, where (⋀_{n≥N} f_{n})(a) = ⋀_{n≥N}(f_{n}(a)) etc.

It is not surprising that the process of taking liminf in A respects the ordering on cseq(A), making lim inf a functor for each liminf complete Ω-category, as the following lemma shows.

Lemma 2.31 For Cauchy sequences α, β in A with liminf a and b respectively, we have ⋁_{N} ⋀_{n≥N}[α_{n}, β_{n}] ≤ [a, b].

Proof : We calculate as follows.

⋁_{N} ⋀_{n≥N}[α_{n}, β_{n}] ≤^{(1)} (⋁_{N} ⋀_{n≥N}[α_{n}, β_{n}]) ⊗ ⋁_{N} ⋀_{n≥N}[β_{n}, b]

≤^{(2)} ⋁_{N} ⋀_{n≥N}[α_{n}, b]
= [a, b]

Here we have (1) because b = lim inf β, (2) by Lemma 2.4. □ Notice, as a corollary that if two converging sequences of elements from A are equivalent in seq(A) then their liminfs are equivalent according to A. The converse is not true. Take as example two sequences in the real numbers, say, which both converge to the same real number, both are chains (i.e. increasing), and for all indices, the element of the first sequence is strictly less than the corresponding element from the second sequence. The real line is our A, which is a preorder. Thus for two sequences to be ordered in seq(A) thus, α ≤ β means that there exists an index, N, such that after that index, α_{n} ≤ β_{n}. Equivalence then means that there is an index after which the two sequences are equivalent element for element. This is clearly not the case for our two sequences, but still they may have the same least upper bound.

Since liminf respects the ordering we have the following.

Observation 2.32 By the definition of liminf we see that given a liminf complete Ω-category, A say, lim inf (which we should suffix with A) is an Ω-functor from the category cseq(A) to A, and we have the following adjunction.

[figure: cseq(A); A; lim inf; ⊥; Δ]
□

Liminf also respects the other Ω-valued relation we have considered on sequences - the one that is the basis for the definition of being Cauchy.

Proposition 2.33 For Cauchy sequences α and β in A with liminf a = lim inf α and b = lim inf β, we have ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[α_{n}, β_{m}] ≤ [a, b].

Proof : We calculate as follows.

⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[α_{n}, β_{m}] ≤ (⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[α_{n}, β_{m}]) ⊗ ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[β_{n}, b]

≤ ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[α_{n}, b]

= [a, b].  □

We used transitivity (Proposition 2.6) in the last inequality.

Observation 2.34 By Proposition 2.33, given a liminf complete Ω-category A, we have an Ω-functor lim inf : kseq(A) ⊸ A. Further, if we by abus de language denote by Δ the embedding of A into kseq(A) by taking constant sequences, then we have the following adjunction.

[figure: kseq(A); A; lim inf; ⊥; Δ]
□

Remark 2.35 Since [x, ] is covariant it is clear that [x, y_{n}]_{n^{∈}ℕ} is Cauchy whenever (y_{n})_{n^{∈}ℕ} is. Thus, for Cauchy sequences α and β, we can write ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[α_{n}, β_{m}] as ⋁_{N} ⋀_{n≥N} lim inf_{m}[α_{n}, β_{m}].

Obviously though, it is not the case that for Cauchy sequences α and β, also [α_{n}, β_{n}]_{n^{∈}ℕ} is Cauchy. The best we can do is to notice the easy inequality

⋁_{N} ⋀_{n≥N} lim inf_{m}[[α_{n}, β_{n}], [α_{m}, β_{m}]] ≥ ⋁_{N} ⋀_{n≥N} lim inf_{m}[[α_{n}, α_{m}], [β_{n}, β_{m}]].  □

Remark 2.36 For a sequence of sequences α we introduce the notation α^{∗} for the sequence of sequences such that α^{∗}(n)(m) = α(m)(n), called the transpose of α. Then we notice that for any sequence α we have Δ ∘ α = \overline{α}^{∗}. This means that for any two sequences α and β we have

kseq(A)[α, β] = ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M} A[α_{n}, β_{m}] = ⋁_{N} ⋀_{n≥N} cseq(A)[\overline{α_{n}}, β] = cseq^{2}(A)[\overline{α}^{∗}, \overline{β}].  □

When considering one of the two main examples that we had in mind from the outset, viz. ordinary (that is, among other things symmetric) metric spaces, one question poses itself: a function between symmetric metric spaces that is conservative is also automatically continuous. Does this generalize to our setting? The following definition and proposition answer this question.

Definition 2.37 An Ω-category (A_{0}, [ , ]) is symmetric if [a, a′] = [a′, a] for all a, a′ ^{∈} A_{0}. □

Proposition 2.38 Given an Ω-functor f : A ⊸ B, if either A or B is symmetric, then f is liminf continuous.

Proof : Let a = lim inf α for α : ℕ ⊸ A. We want to show that [f(a), y] = ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f(α_{n}), y] for all y ^{∈} B_{0}. To see one way we calculate as follows.

[f(a), y] ≥ ⋁_{N^{∈}ℕ} ⋀_{n≥N}([f(a), f(α_{n})] ⊗ [f(α_{n}), y])

≥ ( ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f(a), f(α_{n})]) ⊗ ( ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f(α_{n}), y])

≥ ( ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, a]) ⊗ ( ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f(α_{n}), y])

≥ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f(α_{n}), y]

Here the second inequality is due to symmetry of either A or B.

To see the other way we calculate as follows.

⋁_{N^{∈}ℕ} ⋀_{n≥N}[f(α_{n}), y] ≥ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f(α_{n}), f(a)] ⊗ [f(a), y]

≥ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, a] ⊗ [f(a), y]

≥ [f(a), y]  □

Remark 2.39 In ordinary symmetric metric spaces every convergent sequence is Cauchy. Proposition 2.25 gives instantly that whenever A is symmetric, given a sequence α in A and a ^{∈} A_{0}, if [a, x] = ⋁_{N} ⋀_{n≥N}[α_{n}, x] for all x ^{∈} A_{0}, then α is Cauchy. This implies that for symmetric Ω-categories in general, we can let the liminf notion be the basic one, and define the notion of Cauchy from that. □

Proposition 2.40 cseq and kseq are both endo-functors on the category of Ω-categories and Ω-functors.

Proof : Easy. □

In a suitable sense the Cauchy sequences are also characterized by being liminfs of their finite truncations. Noticing that Δ∘α maps a natural number n into the sequence (α(n), α(n), …) we can make this statement precise as follows.

Proposition 2.41 In kseq(A), we have α = lim inf(Δ ∘ α) for any Cauchy sequence α.

Proof : For any Cauchy sequence β we have

kseq(A)[α, β] = ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[α_{n}, β_{m}] = ⋁_{N} ⋀_{n≥N} kseq(A)[\overline{α_{n}}, β].  □

Notice that this does not hold for cseq(A).

3 A Fubini theorem for liminfs

Theorem 3.1 For any Ω-category B, if B is liminf complete, so is [A, B] for every A.

Proof : Let A and B be Ω-categories with B liminf complete, and let (f_{n})_{n^{∈}ℕ} be a Cauchy sequence of Ω-functors from A to B. This means that 1 ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[f_{n}, f_{m}]. Consider the sequence (f_{n}(a))_{n^{∈}ℕ} in B for each a ^{∈} A_{0}. It is Cauchy since

⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[f_{n}(a), f_{m}(a)] ≥ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[f_{n}, f_{m}].

Therefore we can define the mapping f : A_{0} → B_{0} as f(a) = lim inf_{n^{∈}ℕ} f_{n}(a). To see that f is a morphism from A to B we calculate

[f(a), f(a′)] = [lim inf_{n^{∈}ℕ} f_{n}(a), lim inf_{n^{∈}ℕ} f_{n}(a′)]
≥ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f_{n}(a), f_{n}(a′)]
≥ [a, a′].

Here we have the first inequality by Lemma 2.31, and the second because each f_{n} is a morphism. To see that f = lim inf_{n} f_{n}, we must show

[f, g] = ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f_{n}, g]

for all g : A ⊸ B.

[f, g] = ⋀_{x^{∈}A_{0}}[f(x), g(x)] = ⋀_{x^{∈}A_{0}} ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f_{n}(x), g(x)],

so we are left to show

⋀_{x^{∈}A_{0}} ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f_{n}(x), g(x)] = ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋀_{x^{∈}A_{0}}[f_{n}(x), g(x)].

The inequality ‘≥’ is obvious, and to see ‘≤’ we calculate as follows.

⋀_{x^{∈}A_{0}} ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f_{n}(x), g(x)] ≤ ( ⋀_{y^{∈}A_{0}} ⋁_{K^{∈}ℕ} ⋀_{k≥K}[f_{k}(y), g(y)]) ⊗ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M} ⋀_{x^{∈}A_{0}}[f_{n}(x), f_{m}(x)]

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} (( ⋀_{y^{∈}A_{0}} ⋁_{K^{∈}ℕ} ⋀_{k≥K}[f_{k}(y), g(y)]) ⊗ ⋁_{M^{∈}ℕ} ⋀_{m≥M} ⋀_{x^{∈}A_{0}}[f_{n}(x), f_{m}(x)])

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋀_{x^{∈}A_{0}} (( ⋁_{K^{∈}ℕ} ⋀_{k≥K}[f_{k}(x), g(x)]) ⊗ ⋁_{M^{∈}ℕ} ⋀_{m≥M}[f_{n}(x), f_{m}(x)])

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋀_{x^{∈}A_{0}}[f_{n}(x), g(x)].  □

Here we have used transitivity (Lemma 2.4) in the last inequality. An immediate corollary from the proof of Theorem 3.1 is that liminf is pointwise on functions.

Corollary 3.2 If (f_{n})_{n^{∈}ℕ} is a convergent sequence of Ω-functors from A to B, then (lim inf_{n} f_{n}) (a) = lim inf_{n}(f_{n}(a)) for all a ^{∈} A_{0}. □

We wish to prove the theorem corresponding to Theorem 3.1, restricting ourselves this time to liminf continuous functions.

Lemma 3.3 Given a Cauchy sequence (f_{n})_{n^{∈}ℕ} of liminf continuous functions, with each f_{n} : A ⊸ B, where B is liminf complete, and given a convergent sequence α in A with lim inf α = a. Then we have

lim inf_{n} lim inf_{m}(f_{n}(α_{m})) = lim inf_{n} f_{n}(α_{n}) = lim inf_{m} lim inf_{n}(f_{n}(α_{m})),

with the implicit claim that the liminfs above exist, and where the equality as always is up to isomorphism.

Proof : First we notice that Theorem 3.1 ensures that all the liminfs above exist. The proof then has four parts. (Part 1)

[lim inf_{n}(f_{n}(α_{n})), lim inf_{n} lim inf_{m} f_{n}(α_{m})] ≥ ⋁_{N} ⋀_{n≥N}[f_{n}(α_{n}), lim inf_{m} f_{n}(α_{m})]
= ⋁_{N} ⋀_{n≥N}[f_{n}(α_{n}), f_{n}(lim inf_{m} α_{m})]
≥ ⋁_{N} ⋀_{n≥N}[α_{n}, lim inf_{m} α_{m}]
≥ 1.

In the first equality we have used Lemma 2.31. (Part 2)

[lim inf_{n} lim inf_{m} f_{n}(α_{m}), lim inf_{n}(f_{n}(α_{n}))] = ⋁_{N} ⋀_{n≥N}[lim inf_{m} f_{n}(α_{m}), lim inf_{m}(f_{m}(α_{m}))]
≥ ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[f_{n}(α_{m}), f_{m}(α_{m})]
≥ ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[f_{n}, f_{m}]
≥ 1.

Here we have used Lemma 2.31 twice, and we get the last inequality from (f_{n})_{n^{∈}ℕ} being Cauchy. (Part 3)

[lim inf_{m} lim inf_{n} f_{n}(α_{m}), lim inf_{n}(f_{n}(α_{n}))] = ⋁_{M} ⋀_{m≥M}[lim inf_{n} f_{n}(α_{m}), lim inf_{n}(f_{n}(α_{n}))]
≥ ⋁_{M} ⋀_{m≥M} ⋁_{N} ⋀_{n≥N}[f_{n}(α_{m}), f_{n}(α_{n})]
≥ ⋁_{M} ⋀_{m≥M} ⋁_{N} ⋀_{n≥N}[α_{m}, α_{n}]
≥ 1.

Again we have used Lemma 2.31 twice, and we get the last inequality from (α_{n})_{n^{∈}ℕ} being Cauchy. (Part 4)

[lim inf_{m}(f_{m}(α_{m})), lim inf_{m} lim inf_{n}(f_{n}(α_{m}))] ≥ ⋁_{M} ⋀_{m≥M}[f_{m}(α_{m}), lim inf_{n}(f_{n}(α_{m}))]
≥ ⋁_{M} ⋀_{m≥M}[f_{m}, f]
≥ 1.

Here we have the last inequality because f = lim inf_{n} f_{n}. □

Theorem 3.4 Let B be liminf complete and let (f_{n})_{n^{∈}ℕ} be a Cauchy sequence of liminf continuous functions, f_{n} : A ⊸ B. Then lim inf_{n} f_{n} is liminf continuous.

Proof : As in the proof of Theorem 3.1 we define the function f : A ⊸ B as f(a) = lim inf_{n}(f_{n}(a)) and as there it is a legitimate definition, in that (f_{n}(a))_{n^{∈}ℕ} is Cauchy, and f monotone.

Given then a Cauchy sequence α in A with lim inf α = a, we know that f ∘ α is Cauchy, because, as we have seen, f is conservative. We then just have left to prove that f(a) = lim inf f ∘ α. Spelled out this means that we must show lim inf_{n} (f_{n} (lim inf_{m} α_{m})) = lim inf_{m} lim inf_{n}(f_{n}(α_{m})), but since each f_{n} is liminf continuous, this is equivalent to showing

lim inf_{n} lim inf_{m}(f_{n}(α_{m})) = lim inf_{m} lim inf_{n}(f_{n}(α_{m})),

but this is true by Lemma 3.3. □ Theorem 3.4 says that when B is liminf complete, so is [A, B]^{∘} for every A.

4 Scott topology

A usual line in denotational semantics is to equip a partial order with the Scott topology and show e.g. that order continuity (preservation of ω-chains) coincides with continuity wrt. the Scott topology. In this way one has obtained a topological view on convergence and completeness, something which can be conceptually helpful. We can mimic this entire development, replacing the complete Heyting algebras of topology with commutative unital quantales.

The standard definition of a Scott open subset of a partial order is one that is up-closed and where every directed subset with least upper bound in the subset has an element in common with the subset.

Thus we define, using only sequences, not directed sets, as follows.

Definition 4.1 An Ω-functor ϕ : A ⊸ Ω is Scott open if for all convergent sequences α in A,

ϕ(lim inf α) ≤ lim inf(ϕ ∘ α).  □

It should be clear that the definition is the expected internalization of a statement that says that if lim inf α belongs to ϕ, then so does some α_{n}. We have used ⋁_{N^{∈}ℕ} ⋀_{n≥N} (as it occurs in the unfolding of the definition of liminf on the right-hand side of the inequation according to Proposition 2.30) instead of just ⋁_{n^{∈}ℕ} because of the liminf nature of our convergence. In the preorder case we know that ∃n. ϕ(α_{n}) implies ∃N. ∀n ≥ N. ϕ(α_{n}), after the point where α is a chain.

Proposition 4.2 For all ϕ : A ⊸ Ω and all convergent α in A we have

lim inf(ϕ ∘ α) ≤ ϕ(lim inf α).

Proof : First, notice that the definition of liminf gives that 1 ≤ [lim inf α, lim inf α] = ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, lim inf α] ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[ϕ(α_{n}), ϕ(lim inf α)].

The following easy calculation then shows the result:

lim inf(ϕ ∘ α) = ⋁_{N^{∈}ℕ} ⋀_{n≥N} ϕ(α_{n})

≤ ( ⋁_{N^{∈}ℕ} ⋀_{n≥N} ϕ(α_{n})) ⊗ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[ϕ(α_{n}), ϕ(lim inf α)]

≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ϕ(α_{n}) ⊗ [ϕ(α_{n}), ϕ(lim inf α)]

≤ ϕ(lim inf α).  □

This means that we have the following.

Observation 4.3 An Ω-functor ϕ : A ⊸ Ω is Scott open if and only if it is liminf continuous. □

Dually to Scott open we define what it means to be Scott closed. Definition 4.4 An Ω-functor ψ : A^{op} ⊸ Ω is Scott closed if for all convergent sequences α in A,

lim inf(ψ ∘ α) ≤ ψ(lim inf α).

We denote by [A^{op}, Ω]^{▼} the subcategory of [A^{op}, Ω] consisting of the Scott closed Ω-functors from A^{op} to Ω with the inherited hom-functor. □ Notice, that when we compose two functors, F : A ⊸ B and G : B^{op} ⊸ C we get a functor G∘F : A^{op} ⊸ C, and in our particular case, when we compose α : ℕ ⊸ A with ψ : A^{op} ⊸ Ω we get ψ ∘ α : ℕ^{op} ⊸ Ω, but ℕ^{op} is equal to ℕ, since ℕ is discrete.

We have the standard results, modified to our general setting:

• The Scott opens form a commutative unital quantale.

• Liminf continuity coincides with Scott continuity (to be defined below).

We first have to define suitable lattice operations on the Scott opens, and then we prove that with this structure the lattice of Scott opens form a commutative unital quantale. Definition 4.5 For a family { ϕ_{i} : A ⊸ Ω | i ^{∈} I } of Scott opens and ϕ, ψ : A ⊸ Ω Scott open, we define (⋁_{i^{∈}I} ϕ_{i}) (a) = ⋁_{i^{∈}I}(ϕ_{i}(a)) and (ϕ ⊗ ψ)(a) = ϕ(a) ⊗ ψ(a). □ Lemma 4.6 Whenever ϕ and ψ : A ⊸ Ω are Scott open, so is ϕ ⊗ ψ. Proof : Up-closedness is clear. Let a = lim inf α.

(ϕ ⊗ ψ)(a) = ϕ(a) ⊗ ψ(a)
≤ ( ⋁_{N^{∈}ℕ} ⋀_{n≥N} ϕ(α_{n})) ⊗ ( ⋁_{M^{∈}ℕ} ⋀_{m≥M} ψ(α_{m}))
≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ϕ(α_{n}) ⊗ ψ(α_{n})
= lim inf(ϕ ∘ α ⊗ ψ ∘ α)
= lim inf((ϕ ⊗ ψ) ∘ α).

where we have the second inequality by Lemma 2.3. □ Lemma 4.7 Whenever ϕ_{i} are open for all i ^{∈} I, then so is ⋁_{i^{∈}I} ϕ_{i}.

Proof : Up-closedness is clear. Let a = lim inf α.

⋁_{i^{∈}I}(ϕ_{i}(a)) ≤ ⋁_{i^{∈}I} lim inf_{n^{∈}ℕ}(ϕ_{i}(α_{n}))
= lim inf_{n^{∈}ℕ}(⋁_{i^{∈}I} ϕ_{i}(α_{n})).

Here we have the inequality by open-ness of the ϕ_{i}’s and the equality by left-adjointness of liminf. □ Definition 4.8 We denote by SA the set of Scott opens of A, equipped with the operations ⋁ and ⊗ as defined above. □

It is clear that SA is a complete lattice with ⋁ as join.

Lemma 4.9 The tensor, ⊗, distributes over ⋁ in SA.

Proof : Let ψ and ϕ_{i} : A ⊸ Ω be Scott opens for i ^{∈} I, and let a ^{∈} A_{0}.

(ψ ⊗ ⋁_{i^{∈}I} ϕ_{i}) (a) = ψ(a) ⊗ ⋁_{i^{∈}I}(ϕ_{i}(a))

= ⋁_{i^{∈}I} ψ(a) ⊗ ϕ_{i}(a)

= ⋁_{i^{∈}I} ψ ⊗ ϕ_{i}.  □

We therefore, noticing that the solution set condition is trivially fulfilled in preorders, have the following theorem.

Theorem 4.10 SA is a commutative unital quantale.

One of the usual formulations of continuity in topological terms is to say that a function is continuous if and only if the inverse image of any open is open. This definition is naturally extended to our setting in the following way.

Definition 4.11 A function f : A ⊸ B is Scott continuous if for all Scott open ϕ : B ⊸ Ω the ‘inverse image’, ϕ ∘ f : A ⊸ Ω is Scott open. □

We will show that Scott continuous is the same as liminf continuous.

Lemma 4.12 Whenever ϕ : B ⊸ C and ψ : A ⊸ B are liminf continuous, so is ϕ ∘ ψ.

Proof : Let a = lim inf α in A. We must show that [ϕ(ψ(a)), x] = ⋁_{N^{∈}ℕ} ⋀_{n≥N}[ϕ(ψ(α_{n})), x] for all x ^{∈} A_{0}. But this is trivial since by liminf continuity of ψ we have ψ(a) = lim inf(ψ ∘ α). □

Lemma 4.13 For any A and any x ^{∈} A_{0}, the Ω-functor [ , x] : A ⊸ Ω is Scott closed.

Proof : Let x ^{∈} A_{0} and a = lim inf α in A. We want [a, x] ≥ ⋁_{N^{∈}ℕ} ⋀_{n≥N}[α_{n}, x], which is true by definition of liminf. □

Lemma 4.14 When f : A ⊸ B is Scott continuous and ψ : B^{op} ⊸ Ω Scott closed, then ψ ∘ f : A^{op} ⊸ Ω is Scott closed.

Proof : Let a = lim inf α in A. We must show that [ψ(f(a)), x] ≥ ⋁_{N} ⋀_{n≥N}[ψ(f(α_{n})), x]. This follows from the fact that (f(α_{n}))_{n^{∈}ℕ} converges to f(a), and that ψ is Scott closed. □

Proposition 4.15 A function is Scott continuous if and only if it is liminf continuous.

Proof : Let f : A ⊸ B be Scott continuous and let a = lim inf α in A. We will show that f(a) = lim inf(f ∘ α), that is,

[f(lim inf α), ] = ⋁_{N^{∈}ℕ} ⋀_{n≥N}[f(α_{n}), ].

Now, [f(lim inf α), x] = ([ , x] ∘ f)(lim inf α). Since f is Scott continuous and [ , x] Scott closed, then [f( ), x] is Scott closed, that is, [f(lim inf α), x] ≥ lim inf_{n}[f(α_{n}), x] for all x, as desired. □

We have thus not only showed how the dual structure on Ω (as a commutative unital quantale, which is a particularly simple symmetric monoidal closed category, and as an Ω-category) lifts to the functor category [A, Ω] for any given A, but also showed how our notion of convergence and completeness is consistent with this lifting, in the sense that the categorical structure is preserved in the subcategory of [A, Ω] consisting of the liminf continuous Ω-functors. Further, we have shown that if we just define our notion of liminf on Ω, we can use the Scott definition of convergence as a basis for defining our notion of continuity of an Ω-functor into Ω.

5 A categorical account

Our intuition is that the liminf of a sequence is a colimit of a limit. In this section we give an account of how to make our intuition valid, that is, in which categories we take the limits and colimits.

When we look at sequences in Ω, and want to describe in categorical terms the lim inf operation, we observe first, that in general we do not have a functor α : (ℕ, ≤) ⊸ Ω, where n ≤ m is ⊤ if m = succ(succ(… succn)) for some number (possibly 0) of succ’s, and ⊥ otherwise. To see this, remember for instance, that in preorders we allow sequences which are not chains. However, when we just look at a sequence as a functor from ℕ (that is, the discrete natural numbers), to Ω, then we miss the information about the ordering on the natural numbers when we want to describe liminf as a colimit of a limit. There is no inherent ordering in the natural numbers to be taken directly from their structure as an Ω-category.

For sequences in Ω itself, we can replace α : ℕ ⊸ Ω with \overline{α} : (ℕ, ≤) ⊸ Ω where we define \overline{α}(n) = lim_{m^{∈}ℕ} α(n + m). It is clear that \overline{α} is in fact a functor from (ℕ, ≤) to Ω, and now we have that lim inf α = colim(\overline{α}). We notice that whereas the colimit is filtered, the limit is not. We take the limit of the ‘arbitrary’ diagram that α after n constitutes. To sum up, based on α we define for each n ^{∈} ℕ the functor α_{n} : ℕ ⊸ Ω as α_{n}(m) = α(n + m). Then we define the functor \overline{α} : (ℕ, ≤) ⊸ Ω as \overline{α}(n) = lim α_{n}, and then we can define lim inf α = colim(\overline{α}).

The construction above relies on the fact that Ω is complete. When we deal with sequences in Ω-categories other than Ω we do not always have completeness. Think for example of a (metrically complete, if you like) generalized metric space A, and let α be a Cauchy sequence in A. For a ^{∈} A_{0} to be a categorical limit of α, means that A[x, a] = sup_{n^{∈}ℕ} A[x, α_{n}] for all x ^{∈} A_{0}. So this holds in particular for x = α_{n} for any n. This means that in the case of symmetric metric spaces, for every n ^{∈} ℕ the whole sequence lies within the disk with center in a_{n} and radius A[a_{n}, a]. This is not very interesting in the case of symmetric metric spaces, since in this case only constant sequences have limits. Thus, any symmetric generalized metric space with more than one point is not complete in the categorical sense.

We can restore completeness by introducing partial elements. Instead of taking the limit of α_{n} in A we Yoneda-embed A into [A^{op}, Ω] which is complete (by completeness of Ω) and take the limit there. It turns out then, that when we take the colimit of the limits (which then can be partial elements) we have to be careful do it in the right category, viz. that consisting of the Scott closed functors from A^{op} to Ω. Under fortunate circumstances (when A is liminf complete), it so happens that the colimit is then representable, and that the representing element is the liminf of the original sequence. The following spells out the details.

Definition 5.1 Given an Ω-category A, the Yoneda-embedding Y (if necessary disambiguated as Y_{A}) is the mapping that takes an element a ^{∈} A_{0} into [ , a] : A^{op} ⊸ Ω. □

The following lemma in its original (non-enriched) form is attributed to Yoneda.

Lemma 5.2 For a functor F : A ⊸ Ω and a ^{∈} A_{0} we have [[a, ], F] = F (a), and dually, for a functor G : A^{op} ⊸ Ω and a ^{∈} A_{0} we have [[ , a], G] = G(a). □

Remark 5.3 Since, by Yoneda’s lemma (Lemma 5.2), in particular A[a, a′] ≤ [A^{op}, Ω]([ , a], [ , a′]), we see that Y_{A} is an Ω-functor from A to [A^{op}, Ω]. □

So, instead of considering sequences α : ℕ ⊸ A we consider their embedded versions, Y ∘ α : ℕ ⊸ [A^{op}, Ω]. We recall a few elementary categorical lemmas.

Lemma 5.4 Given an Ω-functor F : D ⊸ A, then Y ∘ F : D ⊸ [A^{op}, Ω] has limitlim_{d}(Y ∘ F (d)). □

Lemma 5.5 Y reflects limits, that is, if lim(Y ∘ F) is representable as Y(a) = [ , a], then a = lim F. □

Lemma 5.6 If F : D ⊸ [A^{op}, Ω] is an Ω-functor such that F (d) is Scott closed for every d, then lim F is also Scott closed.

Proof : Let α : E ⊸ A^{op} with lim α = a. We must show that

(lim F)(lim inf α) ≥ lim inf_{n}((lim F)(α_{n})).

We calculate as follows.

lim inf_{n}((lim F)(α_{n})) = lim inf_{n} (⋀_{d} F (d)(α_{n}))
≤ ⋀_{d} lim inf_{n} F (d)(α_{n})
≤ ⋀_{d} F (d)(lim inf α)
= (lim F)(lim inf α),

where we have the second inequality because F (d) is Scott closed for every d. □

Definition 5.7 Given N ^{∈} ℕ the functor α_{N} : ℕ ⊸ A is defined as α_{N}(n) = α(N + n).

Lemma 5.8 Given any sequence α : ℕ ⊸ A, the mapping that takes N into lim(Y ∘ α_{N}) is an Ω-functor from (ℕ, ≤) to [A^{op}, Ω]^{▼}.

Proof : We know that Y ∘ α_{N}(n) = [ , α_{N}(n)] is Scott closed for every n, and by Lemma 5.6 then that lim(Y ∘ α_{N}) is Scott closed. For N ≤ M we have

lim(Y ∘ α_{N}) = ⋀_{k^{∈}ℕ}[ , α(N + k)] = ⋀_{k≥N}[ , α(k)] ≤ ⋀_{k≥M}[ , α(k)] = ⋀_{k^{∈}ℕ}[ , α(M + k)] = lim(Y ∘ α_{M}).

□

For purposes of illustration, consider the Ω-functor from Lemma 5.8 in the special case of preorders. Given a sequence α in a preorder, the functor takes an index N into ⋀_{n≥N} α_{n}, the infimum of the sequence after N. Taking the supremum of this resulting sequence of infima will then give us the liminf of α.

What we want to do now is

(i) explicitly construct the colimit for the functor from Lemma 5.8 above,

(ii) show that when α is Cauchy, the colimit is representable, and

(iii) show that the representing element is lim inf α.

For the explicit construction of the colimit it is convenient to introduce a couple of concepts from [Wagner 94].

Definition 5.9 For an Ω-functor G : A^{op} ⊸ Ω we define ub G : A ⊸ Ω as ub G(a) = [G, [ , a]], and for an Ω-functor F : A ⊸ Ω we define lb F : A^{op} ⊸ Ω as lb F (a) = [F, [a, ]]. □

The intuition behind ub and lb respectively is that they generalize upper and lower bounds respectively, in the following way. Read ‘ub G(a)’ as ‘a is an upper bound of G’. We see G as a down-closed subset of A, and thus we interpret G(b) as ‘b belongs to G’. Then, for a to be an upper bound of G means that given any b in G, necessarily b is less than a, that is, [b, a]. In the same way lb generalizes lower bounds.

Proposition 5.10 ub and lb are Ω-functors, ub : [A^{op}, Ω]^{op} ⊸ [A, Ω], and lb : [A, Ω] ⊸ [A^{op}, Ω]^{op}.

Proof : A straightforward calculation verifies the claim:

[G_{2}, G_{1}] = [[G_{1}, ], [G_{2}, ]]

≤ ⋀_{a}[[G_{1}, [ , a]], [G_{2}, [ , a]]]

= ⋀_{a}[ub G_{1}(a), ub G_{2}(a)]

= [ub G_{1}, ub G_{2}].

Dually for lb . □

Proposition 5.11 We have an adjunction ub ⊣ lb

Proof : Easy. □

The functors lb and ub are useful in slightly wider contexts than ours. For instance, they are central in formulating the MacNeille completion of an enriched category (see [Wagner 94]). The following concept is not strictly necessary for our exposition here, but serves to shed light on how lb and ub work.

Definition 5.12 A cut in an Ω-category A is a pair (F, G), with F : A ⊸ Ω and G : A^{op} ⊸ Ω, where F = ub G and G = lb F. □

We have reversed the order of the elements of the pair, compared to [Wagner 94], because it turns out that when we formulate the theory in terms of bimodules (see [Wagner 94]) often the pair is also an adjoint pair, and F is then the left adjoint.

Remark 5.13 It is easy to see that ([a, ], [ , a]) is a cut for every a ^{∈} A_{0}. □

Remark 5.14 It is clear that a cut is determined by one of its components. We will call the covariant part the upper cut (F above) and the contravariant one (G above) the lower cut. The upper cuts are precisely the fixed-points of ub ∘ lb and the lower cuts are precisely the fixed-points of lb ∘ ub . Obviously we can look at either composition of ub and lb as a (and the same) kind of closure. From the adjointness of lb and ub , notice that lb ∘ ub ≥ id_{[A^{op},Ω]} and ub ∘ lb ≥ id_{[A,Ω]}. □

Lemma 5.15 When a = lim inf α then [a, ] = ub ⋁_{N} lim(Y ∘ α_{N}).

Proof : For b ^{∈} A_{0} we have

ub ⋁_{N} lim(Y ∘ α_{N})(b) = [⋁_{N} lim(Y ∘ α_{N}), [ , b]]
= [⋁_{N} ⋀_{n}[ , α_{N}(n)], [ , b]]
= ⋁_{N} ⋀_{n}[[ , α_{N}(n)], [ , b]]
= ⋁_{N} ⋀_{n}[α_{N}(n), b]
= [a, b].

Here we have the third equality by (the remark after) Proposition 2.30, since we (by Yoneda) have that whenever a sequence α is Cauchy, so is Y ∘ α. □ As an immediate corollary we have the following.

Theorem 5.16 When a = lim inf α then [ , a] = lb ub ⋁_{N} lim(Y ∘ α_{N}).

Proof : By Lemma 5.15, since always [ , x] = lb [x, ]. □ The advantage of this theorem over Theorem 5.17 below is that it provides an explicit construction.

We can now show that liminf is indeed the representing element of a colimit.

Theorem 5.17 When a = lim inf α, then [ , a] = colim_{N} lim(Y∘α_{N}), where the colimit is taken in [A^{op}, Ω]^{▼}.

Proof : We must show [[ , a], f] = ⋀_{N}[lim(Y ∘ α_{N}), f] for any Scott closed Ω-functor f : A^{op} ⊸ Ω. By Yoneda, [[ , a], f] = f(a), and since lim inf_{n}[ , α_{N}(n)] = ⋁_{N^{∈}ℕ} ⋀_{n≥N}[ , α_{N}(n)] we have

⋀_{N}[lim(Y ∘ α_{N}), f] = [⋁_{N} ⋀_{n}[ , α_{N}(n)], f]
= ⋁_{N} ⋀_{n}[[ , α_{N}(n)], f]
= ⋁_{N} ⋀_{n} f(α_{N}(n))
= f(a),

where we have the last equality from the fact that f is Scott closed. □

6 Scott’s inverse limit theorem

We will here give a general version of Scott’s inverse limit theorem. The theorem as well as its proof specializes to the particular cases of preorders and generalized metric spaces. We give a little more than just the proof, for instance we notice that in a suitable sense, the space of retracts of the inverse limit object is liminf complete, and we show that a sequence of domains fulfills the conditions that guarantee that it has an inverse limit in the traditional sense, if a corresponding sequence in the space of retracts is Cauchy in our sense.

First we will give an important lemma.

Definition 6.1 A function f is called idempotent if f ∘ f = f. □

Lemma 6.2 In Ω-CCAT a liminf of idempotents is idempotent.

Let f_{n} : D ⊸ D be idempotent for every n ^{∈} ℕ, and assume that (f_{n})_{n^{∈}ℕ} is Cauchy with liminf f. This means that f(d) = lim inf_{n^{∈}ℕ}(f_{n}(d)), and we calculate as follows, to see that f is idempotent.

f(f(d)) = lim inf_{n^{∈}ℕ}(f_{n}(lim inf_{m^{∈}ℕ}(f_{m}(d))))
= lim inf_{n^{∈}ℕ} lim inf_{m^{∈}ℕ} f_{n}(f_{m}(d))
= lim inf_{n^{∈}ℕ} f_{n}(f_{n}(d))
= lim inf_{n^{∈}ℕ} f_{n}(d)
= f(d),

where we have the third equality by Lemma 3.3. □

Remark 6.3 We remind the reader of some simple definitions and facts about idempotents and retracts. A

retract of an object A in a category is a pair of morphisms (B ↪^{g} ; ←_{f} A), written (f, g), such that f ∘ g = id_{B}.

Here f is called the projection and g the embedding. A split idempotent is an idempotent e : A → A such

that there exists a retract (B ↪^{g} ; ←_{f} A) of A with g ∘ f = e. For every retract (f, g) the morphisms g ∘ f is an

idempotent, and by definition a split one. □

Definition 6.4 Given any Ω-category D we can form the possibly large Ω-category R(D) of retracts of D

as follows. The class part of R(D) is the class of all retracts (A ↪^{g} ; ←_{f} D) of D, and R(D)[A ↪^{g} ; ←_{f} D, B ↪^{k} ; ←_{h} D] =

[g ∘ f, k ∘ h]. □

Definition 6.5 [The inverse limit construction] Given a diagram [figure: D_{0}; D_{1}; ϕ_{0}; ψ_{0}; ϕ_{1}; ψ_{1}; ⋯] in Ω-CCAT,

where (ψ_{n}, ϕ_{n}) is a retract of D_{n+1} for all n ^{∈} ℕ. Define τ_{nm} : D_{n} ⊸ D_{m} as follows.

τ_{nm}(a_{n}) = \{ \begin{matrix}ψ_{m} ∘ ψ_{m−1} ∘ … ∘ ψ_{n−1}(a_{n}) & if & n > m , \\ a_{n} & if & n = m , \\ ϕ_{m−1} ∘ ϕ_{m−2} ∘ … ∘ ϕ_{n}(a_{n}) & if & n < m . \end{matrix}

We define the Ω-category D_{∞} as follows. D_{∞_{0}} = \{ \overline{x} ^{∈} Π_{n^{∈}ℕ}D_{n} | ψ_{n}(x_{n+1}) = x_{n} for all n ^{∈} ℕ \} and D_{∞}[\overline{x}, \overline{y}] = ⋀_{n^{∈}ℕ}[x_{n}, y_{n}].

We further define Ψ_{n} : D_{∞} ⊸ D_{n} as Ψ_{n}(\overline{x}) = x_{n} and Φ_{n} : D_{n} ⊸ D_{∞} as Φ_{n}(x) = (τ_{ni}(x))_{i^{∈}ℕ} for each n ^{∈} ℕ. □

Notice, that D_{∞}[\overline{x}, \overline{y}] = ⋁_{N^{∈}ℕ} ⋀_{n≥N}[x_{n}, y_{n}]. Both Ψ_{n} and Φ_{n} are obviously Ω-functors for every n, and it is easy to see that (Ψ_{n}, Φ_{n}) is a retract of D_{∞} for every n ^{∈} ℕ.

Lemma 6.6 For every n ^{∈} ℕ, we have Φ_{n+1} ∘ ϕ_{n} = Φ_{n} and ψ_{n} ∘ Ψ_{n+1} = Ψ_{n}.

Proof : Easy. □

Proposition 6.7 D_{∞} is liminf complete.

Proof : Let (\overline{x}_{n})_{n^{∈}ℕ} be a Cauchy sequence in D_{∞}. Then, (x_{in})_{n^{∈}ℕ} is a Cauchy sequence in D_{i} for each i ^{∈} ℕ, and we can define x_{i} = lim inf_{n} x_{in}. It is easy to check that (x_{i})_{i^{∈}ℕ} thus defined is an element of D_{∞_{0}}, and that it is the liminf of (\overline{x}_{n})_{n^{∈}ℕ}. □

Proposition 6.8 For every n ^{∈} ℕ, both Ψ_{n} and Φ_{n} are liminf continuous.

Proof : The proof of liminf continuity of Ψ_{n} is easy. To see liminf continuity of Φ_{n} we reason much like in the proof of Theorem 3.1, using a kind of uniformity argument wrt. convergence.

To see that Φ_{n} : D_{n} ⊸ D_{∞} is liminf continuous means to verify that given any convergent sequence α in D_{n} we have that Φ_{n}(lim inf α) = lim inf(Φ_{n} ∘ α), that is,

[Φ_{n}(lim inf α), \overline{y}] = ⋁_{K} ⋀_{k≥K}[Φ_{n}(α(k)), \overline{y}].

Here the left-hand side reduces to ⋀_{m} ⋁_{K} ⋀_{k≥K}[τ_{nm}(α(k)), y_{m}] by liminf continuity of τ_{nm} for each n and m, and the right-hand side to ⋁_{K} ⋀_{k≥K} ⋀_{m}[τ_{nm}(α(k)), y_{m}]. Here ‘≥’ is obvious, and we see ‘≤’ as follows.

⋀_{m} ⋁_{K} ⋀_{k≥K}[τ_{nm}(α(k)), y_{m}] ≤ (⋀_{m} ⋁_{K} ⋀_{k≥K}[τ_{nm}(α(k)), y_{m}]) ⊗ ⋁_{L} ⋀_{l≥L} ⋁_{K} ⋀_{k≥K}[α(l), α(k)]

≤ ⋁_{L} ⋀_{l≥L} ⋀_{m} ((⋁_{K} ⋀_{k≥K}[τ_{nm}(α(k)), y_{m}]) ⊗ ⋁_{K} ⋀_{k≥K}[α(l), α(k)])

≤ ⋁_{L} ⋀_{l≥L} ⋀_{m} ((⋁_{K} ⋀_{k≥K}[τ_{nm}(α(k)), y_{m}]) ⊗ ⋁_{K} ⋀_{k≥K}[τ_{nm}(α(l)), τ_{nm}(α(k))])

≤ ⋁_{L} ⋀_{l≥L} ⋀_{m}[τ_{nm}(α(l)), y_{m}].  □

By now we have established that the D_{∞} construction yields a cone above the diagram, when considered in the proper category.

Definition 6.9 We denote by Ω-CCAT_{⇄} the category of liminf complete Ω-categories with liminf continuous retracts as morphisms, where the morphisms go in the direction of the projection. □

Thus, the sequence [figure: D_{0}; D_{1}; ϕ_{0}; ψ_{0}; ϕ_{1}; ψ_{1}; ⋯] is a diagram in Ω-CCAT_{⇄}, and the arrows go from right to

left.

Proposition 6.10 The diagram

[figure: D_{0}; D_{1}; ϕ_{0}; ψ_{0}; ϕ_{1}; ψ_{1}; ⋯; D_{∞}; Φ_{0}; Ψ_{0}; Φ_{1}; Ψ_{1}; Φ_{2}; Ψ_{2}]

is a cone in Ω-CCAT_{⇄} with D_{∞} as cone object.

Proof : By Lemma 6.6, Proposition 6.7, and Proposition 6.8. □

Proposition 6.11 R(D_{∞}) with D_{∞} defined as above, is liminf complete.

Proof : Let (f_{n}, g_{n})_{n^{∈}ℕ} be a Cauchy sequence in R(D_{∞}). Thus 1 ≤ ⋁_{N} ⋀_{n≥N} ⋁_{M} ⋀_{m≥M}[g_{n} ∘ f_{n}, g_{m} ∘ f_{m}].

We want to construct a retract (E ↪^{g} ; ←_{f} D_{∞}) such that (f, g) = lim inf_{n}(f_{n}, g_{n}), that is, [g ∘ f, g′ ∘ f′] =

⋁_{N} ⋀_{n≥N}[g_{n} ∘ f_{n}, g′ ∘ f′] for all (f′, g′) ^{∈} R(D_{∞})_{0}.

Define f : D_{∞} ⊸ D_{∞} as limsup_{n}(g_{n} ∘ f_{n}), which we can because D_{∞} and thus [D_{∞}, D_{∞}] are liminf complete. Let E be the image of D_{∞} under f, that is, E_{0} = { f(d) | d ^{∈} D_{∞_{0}} } and E[d, d′] = D[d, d′]. As a liminf of idempotents f is idempotent (Lemma 6.2), and we just have to find a splitting of f. For any d ^{∈} E_{0}, e.g. with d = f(d′), we have f(d) = f(f(d′)) = f(d′) = d, so defining f′ : D_{∞} ⊸ E as f′(d) = f(d) and g′ : E ⊸ D_{∞} as g′(d) = d we have f′ ∘ g′(d) = d and g′ ∘ f′(d) = f(d), so (f′, g′) is the desired splitting (i.e. retract of D). □

Definition 6.12 A diagram D = [figure: D_{0}; D_{1}; ϕ_{0}; ψ_{0}; ϕ_{1}; ψ_{1}; ⋯] in Ω-CCAT is called Cauchy, if

1 ≤ ⋁_{N^{∈}ℕ} ⋀_{n≥N} ⋁_{M^{∈}ℕ} ⋀_{m≥M}[τ_{nm} ∘ τ_{mn}, id_{D_{m}}].  □

Definition 6.13 An Ω-functor ϕ : B ⊸ A is called mono if [x, y] = [ϕ ∘ x, ϕ ∘ y] for any pair of Ω-functors x, y : C ⊸ B. □

Definition 6.14 An Ω-functor ψ : A ⊸ B is called epi if [s, t] = [s ∘ ψ, t ∘ ψ] for any pair of Ω-functors s, t : B ⊸ C. □

Lemma 6.15 For any retract B ↪^{ϕ} ; ←_{ψ} A, the embedding ϕ is mono and the projection ψ is epi.

Proof : Let x, y : C ⊸ B be given. Then [x, y] = [ψ ∘ ϕ ∘ x, ψ ∘ ϕ ∘ y] ≥ [ϕ ∘ x, ϕ ∘ y] ≥ [x, y], which shows that ϕ is mono.

Let s, t : B ⊸ C be given. Then [s, t] = [s ∘ ψ ∘ ϕ, t ∘ ψ ∘ ϕ] ≥ [s ∘ ψ, t ∘ ψ] ≥ [s, t], which shows that ψ is epi. □

Proposition 6.16 A diagram D = [figure: D_{0}; D_{1}; ϕ_{0}; ψ_{0}; ϕ_{1}; ψ_{1}; ⋯] in Ω-CCAT is Cauchy if the corresponding

sequence (Ψ_{n}, Φ_{n})_{n^{∈}ℕ} in R(D_{∞}) is Cauchy. In that case (id_{D_{∞}}, id_{D_{∞}}) = lim inf_{n}(Ψ_{n}, Φ_{n}).

Proof : Given n ≤ m ^{∈} ℕ, we have

[Φ_{n} ∘ Ψ_{n}, Φ_{m} ∘ Ψ_{m}] = [Φ_{m} ∘ τ_{nm} ∘ τ_{mn} ∘ Ψ_{m}, Φ_{m} ∘ Ψ_{m}]
= [τ_{nm} ∘ τ_{mn}, id_{D_{∞}}].

Here we have the last equality by Lemma 6.15. We have yet to show that lim inf_{n}(Φ_{n} ∘ Ψ_{n}) = id_{D_{∞}}. To do this we calculate as follows.

[id_{D_{∞}}, t] = ⋀_{m}[Ψ_{m}, Ψ_{m} ∘ t]

≥ ⋀_{m} ((⋁_{N} ⋀_{n≥N}[Ψ_{m}, Ψ_{m} ∘ Φ_{n} ∘ Ψ_{n}]) ⊗ ⋁_{N} ⋀_{n≥N}[Ψ_{m} ∘ Φ_{n} ∘ Ψ_{n}, Ψ_{m} ∘ t])

≥ ⋀_{m} ⋁_{N} ⋀_{n≥N}[Ψ_{m} ∘ Φ_{n} ∘ Ψ_{n}, Ψ_{m} ∘ t]
≥ ⋁_{N} ⋀_{n≥N} ⋀_{m}[Ψ_{m} ∘ Φ_{n} ∘ Ψ_{n}, Ψ_{m} ∘ t]
= ⋁_{N} ⋀_{n≥N}[Φ_{n} ∘ Ψ_{n}, t],

and

⋁_{N} ⋀_{n≥N}[Φ_{n} ∘ Ψ_{n}, t] ≥ ⋁_{N} ⋀_{n≥N}[Φ_{n} ∘ Ψ_{n}, id_{D_{∞}}] ⊗ [id_{D_{∞}}, t]
≥ [τ_{nm} ∘ τ_{mn}, id_{D_{∞}}] ⊗ [id_{D_{∞}}, t]
≥ [id_{D_{∞}}, t],

where we have the last inequality because D is Cauchy. □

In addition to Proposition 6.10 we can show that the D_{∞} construction yields a limit in Ω-CCAT_{⇄} of D, seen as a diagram in that category.

Theorem 6.17 (Scott’s inverse limit theorem) When a diagram D = [figure: D_{0}; D_{1}; ϕ_{0}; ψ_{0}; ϕ_{1}; ψ_{1}; ⋯] in

Ω-CCAT_{⇄} is Cauchy, then it has a limit in Ω-CCAT_{⇄}, viz. (D_{∞}, (Φ_{n}, Ψ_{n})_{n^{∈}ℕ}).

Proof : We have already seen that D_{∞} with (Ψ_{n}, Φ_{n})_{n^{∈}ℕ} forms a cone over D in Ω-CCAT_{⇄}. Let E with (Ψ′_{n}, Φ′_{n})_{n^{∈}ℕ} be another cone over D. First we show that the sequence (Φ′_{n} ∘ Ψ_{n})_{N^{∈}ℕ} is Cauchy in [D_{∞}, E]^{∘}. We calculate for n ≤ m as follows.

[Φ′_{n} ∘ Ψ_{n}, Φ′_{m} ∘ Ψ_{m}] = [Φ′_{m} ∘ τ_{nm} ∘ Ψ_{n}, Φ′_{m} ∘ Ψ_{m}]
= [τ_{nm} ∘ Ψ_{n}, Ψ_{m}]
= [τ_{nm} ∘ τ_{mn} ∘ Ψ_{m}, Ψ_{m}]
= [τ_{nm} ∘ τ_{mn}, id_{D_{m}}],

and since D is Cauchy we have shown that (Φ′_{n} ∘ Ψ_{n})_{N^{∈}ℕ} is Cauchy in [D_{∞}, E]^{∘}.

Since E is liminf complete and Φ′_{n} ∘ Ψ_{n} is liminf continuous for every n we can define Φ : D_{∞} ⊸ E as lim inf_{n}(Φ′_{n} ∘ Ψ_{n}) and know that Φ is liminf continuous (Lemma 3.3).

In a precisely analogous way we can see that the sequence (Φ_{n} ∘ Ψ′_{n})_{N^{∈}ℕ} is Cauchy in [E, D_{∞}]^{∘}, and by liminf completeness of D_{∞} we can define Ψ : E ⊸ D_{∞} = lim inf_{n}(Φ_{n} ∘ Ψ′_{n}) and we know that Ψ is liminf continuous.

We need to show that Ψ ∘ Φ = id_{D_{∞}}. We have that Ψ ∘ Φ = (lim inf_{n}(Φ_{n} ∘ Ψ′_{n})) ∘ lim inf_{m}(Φ′_{m} ∘ Ψ_{m}), which by liminf continuity of Ψ is lim inf_{m} (lim inf_{n}(Φ_{n} ∘ Ψ′_{n})) ∘ Φ′_{m} ∘ Ψ_{m}, which by Corollary 3.2 is equal to lim inf_{m} lim inf_{n} (Φ_{n} ∘ Ψ′_{n} ∘ Φ′_{m} ∘ Ψ_{m}), which by Lemma 3.3 is equal to lim inf_{n} (Φ_{n} ∘ Ψ′_{n} ∘ Φ′_{n} ∘ Ψ_{n}) = lim inf_{n} (Φ_{n} ∘ Ψ_{n}), which by Proposition 6.16 is id_{D_{∞}}.

Finally, to see that (Φ, Ψ) thus defined is unique in making the suitable diagram commute, observe that by Proposition 6.16 we know that Φ = Φ ∘ lim inf_{n} (Φ_{n} ∘ Ψ_{n}), which by liminf continuity of Φ is lim inf_{n} (Φ ∘ Φ_{n} ∘ Ψ_{n}) = lim inf_{n} (Φ′_{n} ∘ Ψ_{n}). □

Theorem 6.17 specializes, including our proof, straightforwardly to the preorder and the metric case. It is instructive to see how the Cauchy condition on the diagram D specializes. In the preorder case, we see that D is Cauchy if and only if every retract (ψ_{n}, ϕ_{n}) fulfills ϕ_{n} ∘ ψ_{n} ≤ id_{D_{n+1}}, which is Scott’s traditional condition. In the metric case we see immediately that the condition specializes to the one given by America and Rutten in [America & Rutten 87].

7 Conclusion

We have given an account of a simple and general domain theory using enriched categories and a notion of liminf convergence as the main conceptual tools. By this simplicity we can obtain greater generality than related approaches to unifying metric spaces with partial orders ([Smyth 88] and [Flagg & Kopperman 94]). Naturally, by allowing a wider class of categories as categories of domains, we also have weaker properties than the above mentioned approaches, which are rich in topological structure. However, as we have shown, ours is enough to do general domain theory. In [Wagner 94] it is further discussed how one can also model a notion of compactness and finiteness inside our framework, but much concerning algebraicity and models of non-determinacy remains open for future investigation. Recently we have developed a notion of ideal completion, based on a generalization of directed sets. This construction will be published in a forthcoming article.

Our most immediate concern is however the development of a language that bases itself naturally on the structure of Ω, that is, on a commutative unital quantale. In this language one would be able to assert properties about our general domains, and about elements in them, and for instance derive Scott’s inverse limit theorem. The advantage of developing such a language is that it would clarify the logical rather than the structural properties needed to solve recursive domain equations in a way similar to what we do now.

The aim of finding a logical (as opposed to ad hoc) unification of metric space and partial order domain theory was set out already in the MSc thesis by Rowlands-Hughes ([Rowlands-Hughes 87]), and we have found that by so doing, we encompass many more structures than just partial orders and metric spaces. It is our hope that applications will make use of these more expressive structures, for instance in semantic analysis that deal with more than just the extensional properties of programs. One such example might be in the work of Schellekens ([Schellekens 94]) which include considerations about complexity, but hopefully many other applications will emerge.

References

[America & Rutten 87] America, P., J.J.M.M. Rutten, Solving reflexive domain equations in a category of complete metric spaces, Centrum voor Wiskunde en Informatica, Report CS-R8709, Feb. 1987. Also in Journal of Computer and System Science, 39(3):343-375, 1989.

[Eilenberg & Kelly 66] Eilenberg, S., G.M. Kelly, Closed categories, Proceedings of La Jolla Conference on Categorical Algebra, Springer Verlag 1966.

[Flagg & Kopperman 94] Flagg, B., R. Kopperman, Fixed Points and Reflexive Domain Equations in Categories of Continuity Spaces, MFPS XI, New Orleans March–April 1995, ENTCS, vol.1, 1995.

[Fourman & Scott 77] Fourman, M., D.S. Scott, Sheaves and logic, in proceedings Durham 1977, Applications of Sheaves, Lecture Notes in Mathematics, vol. 753, eds.: Fourman, Mulvey, Scott. Springer Verlag, 1979.

[Freyd 90] Freyd, P., Recursive types reduced to inductive types, LICS 1990.

[Gierz et al. 80] Gierz, G., K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, D.S. Scott, A Compendium of Continuous Lattices, Springer-Verlag, 1980.

[Johnstone 82] Johnstone, P.T., Stone Spaces, Cambridge Studies in Advanced Mathematics, vol. 3, Cambridge University Press, 1982.

[Lambek & Scott 86] Lambek, J., P.J. Scott, Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, 1986.

[Lawvere 73] Lawvere, F.W., Metric spaces, generalized logic, and closed categories, Rendiconti Seminario Matematico e Fisico di Milano, vol. 43, pp. 135-166, 1974.

[Rowlands-Hughes 87] Rowlands-Hughes, D.M., Domains versus metric spaces, MSc Thesis, Imperial College, September 1987.

[Schellekens 94] Schellekens, M., The Smyth completion: A common foundation for denotational semantics and complexity analysis, MFPS XI, New Orleans March–April 1995, ENTCS, vol.1, 1995.

[Scott 82] Scott, D.S., Domains for denotational semantics, In M. Nielsen and E.M. Schmidt, eds.:International Colloquium on Automata, Languages and Programs, pp 577-613, Lectures Notes in Computer Science vol. 140, Springer Verlag, 1982.

[Smyth 88] Smyth, M.B., Quasi-uniformities: reconciling domains with metric spaces, Proceedings of the 3’rd Workshop on the Mathematical Foundations of Programming Language Semantics, Tulane, April 1987, Lecture Notes in Computer Science, Vol. 298, Springer Verlag, 1988.

[Wagner 94] Wagner, K.R., Solving Recursive Domain Equations with Enriched Categories, Ph.D. Thesis, Carnegie Mellon University, Technical Report CMU-CS-94-159, July 1994.