Lifting as a KZ-doctrine

Marcelo P. Fiore^{⋆}

                                   <mf@dcs.ed.ac.uk>

Department of Computer Science Laboratory for Foundations of Computer Science University of Edinburgh, The King’s Buildings Edinburgh EH9 3JZ, Scotland

Synopsis. In a cartesian closed category with an initial object and a dominance that classifies it, an intensional notion of approximation between maps —the path relation (c.f. link relation)— is defined. It is shown that if such a category admits strict/upper-closed factorisations then it preorderenriches (as a cartesian closed category) with respect to the path relation. By imposing further axioms we can, on the one hand, endow maps and proofs of their approximations (viz. paths) with the 2-dimensional algebraic structure of a sesqui-category and, on the other, characterise lifting as a preorder-enriched lax colimit. As a consequence of the latter the lifting (or partial map classifier) monad becomes a KZ-doctrine.

1 Introduction

One of the concerns of axiomatic domain theory, and a particular concern of this paper, is the analysis of notions of approximation aiming at explaining and justifying (order-theoretic) properties of categories of domains. For example, in [Fio94c, Fio94a], while studying the interaction between partiality and order-enrichment we considered contextual approximation which, in the framework we were working in, coincided with the specialisation preorder. But in the applications carried out in [FP94, Fio94a] we had to work with an axiomatised notion of approximation, instead of the aforementioned one, for the following two reasons: first, the specialisation preorder is not appropriate in categories of domains and stable functions (see [Fio94c]) and, second, we do not know of non-order-theoretic axioms making the specialisation preorder ω-complete. To overcome these drawbacks another notion of approximation was to be considered. And, it was the second problem that motivated the intensional notion of approximation provided by the path relation. In fact, it is shown in [Fio94b] that under suitable axioms the path relation can be equipped with a canonical passage-to-the-limit operator appropriate for fixed-point computations; stronger axioms make this operator be given by lubs of ω-chains.

Incidentally, in the context of synthetic domain theory [Pho90, Hyl91, Tay91] the path relation (called there the link relation) was already considered (mainly as a technical tool) but was required to coincide with the specialisation preorder.

Here we study the path relation independently of the specialisation preorder. First, the path relation is shown to interact nicely with type constructors and, since in general it need not be transitive, an axiom under which it becomes a preorder is proposed. Afterwards, we study the interaction between the path relation and the lifting monad (sometimes called the partial map classifier monad —see, e.g. [Koc91]) arising from the representability of partial maps. In particular, we provide a (non-order-theoretic) axiomatic framework in which the lifting monad becomes a KZ-doctrine with respect to the path relation. We do this motivated by the fact that on posets lifting is the construction that freely adjoins suprema for all subsets with at most one element, whilst KZ-doctrines [Koc94] are equational 2-dimensional categorical algebras underlying the process of freely completing categories under a given class of colimits.

⋆ Research supported by SERC grant RR30735.

The paper is organised as follows. In Section 2 we introduce the basic assumptions on our category of discourse. In the vein of [Fio94a], we equip it with a subcategory of admissible monos allowing us to consider a notion of partiality from which the lifting monad arises. In Section 3 we consider the category of Eilenberg-Moore algebras for the lifting monad as a category of pointed objects (as they come equipped with a bottom element) and strict maps. In Section 4 the path relation is introduced and various algebraic properties of paths are presented. In Section 5 we axiomatise upper-closed subsets as those which are orthogonal (in a parameterised or internal sense) to strict maps and establish their closure properties. In Section 6, we present our main axiom (Axiom 1); intuitively stating that every map X → A with X pointed factors as a strict map X ∘→ U with U a minimal upper-closed subset of A. The path relation is always reflexive but it might not be transitive (a counterexample to transitivity can be found in [Fio94b]). By introducing the above axiom, transitivity is achieved and, in fact, our category of discourse is seen to Preo-enrich (as a cartesian closed category) with respect to the path preorder. In Section 7 the relationship between approximation and upper-closure is established. In Section 8 we introduce Axiom 2 (already present in [Fio94b]) and show how lifting can be characterised as a lax colimit. In Section 9, we endow our algebra of proofs-of-approximation (viz. paths) with the 2-dimensional algebraic structure of a sesqui-category. In Section 10 we introduce Axiom 3 (also present in [Fio94b]) which together with Axiom 2 make our (now Preo-enriched) category of discourse have cotensors with the Sierpinski space. Extending the result of the previous section, we then characterise lifting as a lax Preo-colimit and as a corollary the lifting monad becomes a KZ-doctrine.

2 Lifting monad

We introduce the basic assumptions on our category of discourse C and define the lifting monad.

Definition 2.1 ([Mog86, Ros86]) A domain structure is a pair (C, D) consisting of a category (of total maps) C and a well-powered category (of admissible monos) D, such that D is a full-on-objects subcategory of C all of whose morphisms are monos in C, with the following closure property: every diagram

B ⟶^{f} A ↢^{n} D with f ∈ C and n ∈ D has a pullback in C and if B ↢^{f^{−1}(n)} f^{−1}(D) ⟶^{n^{∗}f} D is any such pullback then f^{−1}(n) ∈ D. □

Convention. Admissible monos are denoted with ↪.

Definition 2.2 The category of partial maps p(C, D) induced by a domain structure (C, D) has the same objects as C; a partial map [m, f] : A ⇀ B is an equivalence class of spans A ↩^{m} D ⟶^{f} B in D × K, where two spans A ↩^{m} D ⟶^{f} B and A ↩^{n} E ⟶^{g} B are equivalent if and only if m = n ∘ i and f = g ∘ i for some isomorphism i : D ≅ E. Composition of partial maps is given as for relations, by pullback; identities have the form [id_{A}, id_{A}]. □

The category of total maps appears as a full-on-objects subcategory of the category of partial maps via the faithful inclusion functor J : C → p(C, D) sending a total map f to the partial map [id, f].

Assumption 1 We assume a domain structure (C, D) such that the inclusion functor J : C → p(C, D) has right adjoint L. □

Convention. We write χ : p(C, D)(A, B) ≅ C(A, LB) for the lifting transpose operator provided by the adjunction J ⊣ L : p(C, D) → C.

We recall from [Fio94a] that the unit η and the counit ε of J ⊣ L : p(C, D) → C are such that, for every A ∈ | C |, η_{A} : A → LA is an admissible mono and ε_{A} = [η_{A}, A] : LA ⇀ A. From Assumption 1 we obtain the lifting monad 𝕃 = (LJ, η, μ) : C → C where L(A ⟶^{f} B) = χ[η_{A}, f], η is cartesian (i.e. the squares required to commute by naturality are pullbacks), and μ_{A} = χ[η_{A} ∘ η_{LA}, A]. Moreover, 𝕃 is a commutative monad [Koc70] with tensorial strength t′ : L(A)×B → L(A×B) given by χ[η_{A} ×B, A×B].

Assumption 2 We assume C has binary products and exponentials, and p(C, D) has a zero object. □

Convention. We write

– ⟨ , ⟩ : C(C, A) × C(C, B) ≅ C(C, A × B), and π_{1} : A × B → A and π_{2} : A × B → B for the pairing operator and the projection maps respectively;

– λ : C(C × A, B) ≅ C(C, B^{A}) and e : A^{B} × B → A for the currying operator and the evaluation map respectively; and

– 0 for the zero object in p(C, D).

It follows that C has an initial object 0 and a terminal object 1 = L0.

Remark. If m : D ↣ A and n : E ↣ B are admissible then so is m × n : D × E ↣ A × B because m × n = (χ[m, D → 1] × χ[n, E → 1])^{−1}(η_{1} × η_{1}).

Convention. For f : A → B, we let ⌜f⌝ be λ(1 × A ≅ A ⟶^{f} B) : 1 → B^{A}

Our leading examples are:

Example 2.3 1. (Poset,Υ) where Poset is the category of small posets and monotone functions, and

Υ is its subcategory of all isomorphisms onto upper-closed subsets.

2. (Cpo,Σ) where Cpo is the category of small cpos (posets, possibly without a least element, closed under lubs of ω-chains) and continuous functions, and Σ is its subcategory of all isomorphisms onto Scott-open subsets. □

3 Pointed objects and strict maps

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

Convention. An algebra for the lifting monad is called a pointed object. The algebra structure on a pointed object X is denoted by ρ_{X} but generally left implicit; in the particular case in which X is of the form LA, we take ρ_{X} = μ_{A}. Algebra homomorphisms are called strict and are denoted with ∘→. When we write X ∘→ Y, X and Y are assumed to be pointed.

We recall that the forgetful functor C^{𝕃} → C has a right adjoint determined by the following universal property: every f : A → X with X pointed has a unique strict extension f^{#} : LA ∘→ X (given by the

composite ρ_{X} ∘ Lf) such that (A ↪^{η_{A}} LA ∘⟶^{f^{#}} X) = f.

Remark. 1 is a zero object in C^{𝕃} because C^{𝕃}(1, X) = C^{𝕃}(L0, X) ≅ C(0, X) ≅ 1.

Pointed objects have least elements (c.f. Proposition 4.4 (4)):

Definition 3.1 (Bottom) For a pointed object X we define ⊥_{X} to be the unique strict map 1 ∘→ X. □

It follows that ⊥_{LA} = χ(1 ⇀ 0 → A). Moreover, for every f : X ∘→ Y, f ∘ ⊥_{X} = ⊥_{Y} and hence ⊥_{X} = ρ_{X} ∘ ⊥_{LX}.

Proposition 3.2 For every object A and every pointed object X,

1. X^{A} (with ρ_{X^{A}} = λ(ρ_{X} ∘ L(e) ∘ t′)) is a pointed object.

2. ⌜A → 1 ∘→ X⌝ : 1 ∘→ X^{A}. □

4 Path relation

Our aim now is to define an intensional notion of approximation between maps in C.

Convention. We write Σ_{m} for L^{m}1, ⊥_{m} for 1 ∘→ Σ_{m} (omitting the subscript when m = 1), and ⊤ for η_{1} : 1 ↪ Σ.

If we consider LA as the object obtained from A by freely adjoining ⊥_{LA} approximating any other element then, in the case A = 1, we have that ⊥ : 1 ∘→ Σ approximates ⊤ : 1 ↪ Σ. In addition, if we visualise this notion as the existence of a canonical (directed) path ⊥ ⊤ from ⊥ to ⊤ (thinking of such a path as a proof of the fact that ⊥ approximates ⊤) then we can consider notions of approximations for arbitrary objects by stating that, for two elements x and y of C, x approximates y whenever the canonical path ⊥ ⊤ can be transformed, via a map Σ → C, into a path x y from x to y in C. Also, by regarding Σ_{m} as the object containing a canonical path of length m, we can generalise the notion to paths of arbitrary finite length. A formalisation of these intuitions leads to the following definitions:

Definition 4.1 (Top) For m ≥ 0 we inductively define ⊤_{m} : 1 ↪ Σ_{m} as follows: ⊤_{0} = 1 and ⊤_{m+1} = η_{Σ_{m}} ∘ ⊤_{m}. □

Definition 4.2 (Path relation) For f, g : A → B and α : Σ_{m} × A → B (m ≥ 0), we set α : f _{m} g : A → B if and only if

α  B Σ_{m} × A  . ⊥_{m} × A1 × A ≅ A f ⊤_{m} × A1 × A ≅ A g

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

Remark. Ideas similar to the above, though in the context of undirected paths, constitute the basics of homotopy theory (see e.g. [Bro88]).

Convention. When the subscript is omitted in Σ_{m}, ⊥_{m}, ⊤_{m} and _{m} , it is assumed to be 1.

For testing approximation, paths of length one suffice:

Proposition 4.3 f ⊑ g if and only if f g.

Proof: Because f _{0} g if and only if f = g, and if α : f _{m+1} g : A → B then α∘(L(⊤_{m})×A) : f g.

□

Paths enjoy the following algebraic properties (c.f. Section 9):

Proposition 4.4 1. id_{f} : f _{0} f : A → B where id_{f} =^{def} (1 × A ≅ A ⟶^{f} B).

2. For f : A′ → A, α : h _{m} h′ : A → B, and g : B → B′, id_{g} ⋆ α ⋆ id_{f} : g ∘ h ∘ f _{m} g ∘ h′ ∘ f : A′ → B′ where id_{g} ⋆ α ⋆ id_{f} =^{def} g ∘ α ∘ (Σ_{m} × f).

3. If α : f _{m} f′ : A → B and β : g _{m} g′ : B → C then β ⋆ α : g ∘ f _{m} g′ ∘ f′ : C → B where β ⋆ α =^{def} β ∘ ⟨π_{1}, α⟩.

4. For every pointed object X and every x : 1 → X, ρ_{X} ∘ (Lx) : ⊥_{X} x.

5. If α : f _{m} g : A → B then (Lα)∘t′′ : Lf _{m} Lg : LA → LB where t′′ =^{def} (L⟨π_{2}, π_{1}⟩)∘t′ ∘⟨π_{2}, π_{1}⟩.

6. α : f _{m} f′ : C → A and β : g _{m} g′ : C → B if and only if ⟨α, β⟩ : ⟨f, g⟩ _{m} ⟨f′, g′⟩ : C → A × B.

7. α : f _{m} g : A × B → C if and only if λ(α ∘ a) : λ(f) _{m} λ(g) : A → C^{B} where a is the canonical isomorphism (Σ_{m} × A) × B ≅ Σ_{m} × (A × B).

8. Let A ⟶^{⨿_{1}} A + B ⟵^{⨿_{2}} B be a coproduct diagram with associated natural isomorphism [ , ] : C(A, –) × C(B, –) ≅ C(A + B, –). Then, α : f _{m} f′ : A → C and β : g _{m} g′ : B → C if and only if γ : [f, g] _{m} [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 4.5 1. (A → 1 ∘→ X) f : A → X.

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

Example 4.6 Using Corollary 4.5 (2) one can readily see that:

– in Poset and Cpo the path relation is the pointwise order; whilst,

– in Poset_{∧} (Cpo_{∧}), the category of posets (cpos) with (continuous) pullbacks and pullback-preserving monotone (continuous) functions, the path relation is the stable order. □

5 Upper-closed monos

To express Axiom 1 a notion of upper-closure needs to be incorporated. In this section, we axiomatise upper-closed monos as those orthogonal (in a parameterised sense) to strict maps, and establish their closure properties.

Definition 5.1 A mono U ↣ A is upper-closed if every commuting square

X × C U  Y × C A h × C

with h : X ∘→ Y, has a (necessarily unique) fill-in. □

Convention. Upper-closed monos are denoted with ▷→.

Remark. It is well-known that orthogonality in the above parameterised sense coincides with orthogonality in an internal sense as a mono m : U ↣ A is upper-closed if and only if for every h : X ∘→ Y, the commuting square

U^{Y}  A^{X} U^{X}m^{X} m^{Y}A^{Y} U^{h} A^{h}

is a pullback.

Justifying our terminology, in the leading examples the usual definition of upper-closure and the above categorical one coincide:

Proposition 5.2 In Poset (Cpo), m : U ↣ A is upper-closed if and only if for every u ∈ U and a ∈ A with m(u) ≤ a, there exists (a necessarily unique) u′ ∈ U such that u ≤ u′ and m(u′) = a.

Convention. We write 1 for the discrete poset {0}, and 2 for the Sierpinski space {0 ≤ 1}.

Proof: (⇒) Let m : U ↣ A be upper-closed and let u ∈ U and a ∈ A be such that m(u) ≤ a. Since the square

U [0 ∣→ u]1  2 A[0 ∣→ m(u), 1 ∣→ a] m [0 ∣→ 0]

commutes, there exists a unique fill-in p : 2 → U such that u = p(0) ≤ p(1) and m(p1) = a. Thus, taking u′ = p(1) we are done.

(⇐) Let (X × C ⟶^{f} U ↣^{m} A) = (X × C ⟶^{h×C} Y × C ⟶^{g} A) with h : X ∘→ Y.

For every (y, c) ∈ Y × C, since m(f(⊥, c)) = g(⊥, c) ≤ g(y, c) it follows that there exists a unique u_{(y,c)} ∈ U such that f(⊥, c) ≤ u_{(y,c)} and m(u_{(y,c)}) = g(y, c). Thus, the mapping sending (y, c) ∈ Y × C to u_{(y,c)} ∈ U is a function from Y × C to U. Moreover it is monotone (continuous) because so is g and for every u, u′ ∈ U, u ≤ u′ ⟺ m(u) ≤ m(u′). Thus, Y × C → U : (y, c) ∣→ u_{(y,c)} is the required fill-in. □

Various closure properties of upper-closed monos are summarised below. In particular, because of our parameterised definition, closure under exponentiation is guaranteed.

Proposition 5.3 1. Upper-closed monos are closed under isomorphisms, composition and pullbacks

(whenever they exist).

2. For every A, 0 ↣ A is upper-closed.

3. If m : U ↣ A and n : V ↣ B are upper-closed then so is m × n : U × V ↣ A × B.

4. If m : U ↣ A is upper-closed then so is m^{B} : U^{B} ↣ A^{B}.

5. If U ↣ A ↣ B is upper-closed then so is U ↣ A. □

Convention. For monos D ↣ A and E ↣ A we write D ⊆_{A} E when there exists D → E such that (D ↣ A) = (D → E ↣ A), and we write D ≃_{A} E when D ⊆_{A} E ⊆_{A} D. (Subscripts are omitted whenever they are understood from the context.)

Remark. It follows from Proposition 5.3 (1) that if C has pullbacks of upper-closed monos under arbitrary maps then (C, U), with U the category of all upper-closed monos in C, is a domain structure.

In the leading examples, admissible monos are upper-closed. This situation is characterised below:

Proposition 5.4 The following are equivalent:

1. Admissible monos are upper-closed.

2. ⊤ is upper-closed.

3. For every admissible mono m : D ↪ Y × C with Y pointed, if ⊥_{Y} × C ⊆ m then m ≃ Y × C.

Proof:

(1) ⟺ (2) By Proposition 5.3 (1).

(2) ⇒ (3) Let ⊥_{Y} × C ⊆ m. Then, the commutativity of

1 × C  Y × C ⊥_{Y} × C D  Σ 1  ⊤  χ[m, D → 1] m

implies (Y × C → 1 ↪^{⊤} Σ) = χ[m, D → 1] and hence m ≃ Y × C.

(3) ⇒ (2) Assuming

X × C  Y × C 1  g h × C  Σ ⊤

with h : X ∘→ Y, we need show that g = (Y × C → 1 ↪^{⊤} Σ), or equivalently that g^{−1}(⊤) ≃ Y × C. Observing that

(h × C)^{−1}(g^{−1}(⊤)) ≃ (g ∘ (h × C))^{−1}(⊤) ≃ (⊤ ∘ (X × C → 1))^{−1}(⊤) ≃ (X × C → 1)^{−1}(1) ≃ X × C

we have that h × C factors through g^{−1}(⊤). So that ⊥_{Y} × C = (h ∘ ⊥_{X}) × C = (h × C) ∘ (⊥_{X} × C) factors through g^{−1}(⊤) and hence we are done. □

6 The strict/upper-closed factorisation

We require the following:

Axiom 1 (Strict/upper-closed factorisation) Every morphism with source a pointed object factors as a strict map followed by an upper-closed mono. □

In the leading examples, every map f : X → A with X pointed has a factorisation as above, namely as X ∘→ ↑ (f(⊥_{X}))▷→A where ↑ (f(⊥_{X})) is the poset with underlying set {a ∈ A | f(⊥_{X}) ≤ a} ordered as in A. Thus the following:

Convention. For f : X → A with X a pointed object, we write X ∘→ ↑ (f) ▷→ A for a factorisation of f according to the strict/upper-closed factorisation axiom.

Proposition 6.1 1. If (X ∘→ Y ↣ A) = (X → U ▷→ A) then Y ⊆ U.

2. For f : X ∘→ Y, ↑ (f) ≃ Y.

3. Let X and Y be pointed objects. For f : X → Y and g : Y → B, ↑ (g ∘ f) ⊆ ↑ (g); and moreover, if f is strict then ↑ (g ∘ f) ⊇ ↑ (g). □

The key to establishing the transitivity of the path order is the following:

Proposition 6.2 The pullback

LX  LY X  Y η_{X}  η_{Y} h Lh  (1)

is a weak pushout.

Proof: Let (X ↪^{η_{X}} LX ⟶^{f} C) = (X ∘→^{h} Y ⟶^{g} C).

Since ↑ (g) ≃ ↑ (g ∘ h) ≃ ↑ (f ∘ η_{X}) ⊆ ↑ (f) it follows that

(X ↪^{η_{X}} LX ∘→^{f′} ↑ (f)) = (X ∘→^{h} Y ∘→^{g′} ↑ (g) ▷→ ↑ (f)).

So, letting LY ∘→↑ (f) be the unique strict extension of Y ∘→^{g′} ↑ (g)▷→↑ (f) we have that LY ∘→↑ (f)▷→C mediates between LX ∘→^{Lh} LY ↩^{η_{Y}} Y and LX ⟶^{f} C ⟵^{g} Y because

(Y ↪^{η_{Y}} LY ∘→ ↑ (f) ▷→ C) = (Y ∘→^{g′} ↑ (g) ▷→ ↑ (f) ▷→ C) = (Y ∘→^{g′} ↑ (g) ▷→ C) = g

and

(X ↪^{η_{X}} LX ∘→^{Lh} LY ∘→ ↑ (f) ▷→ C) = (X ∘→^{h} Y ↪^{η_{Y}} LY ∘→ ↑ (f) ▷→ C)
= (X ∘→^{h} Y ∘→^{g′} ↑ (g) ▷→ C)
= (X ↪^{η_{X}} LX ∘→^{f′} ↑ (f) ▷→ C)
⇒ (X ↪^{η_{X}} LX ∘→^{Lh} LY ∘→ ↑ (f)) = (X ↪^{η_{X}} LX ∘→^{f′} ↑ (f))
⇒ (LX ∘→^{Lh} LY ∘→ ↑ (f)) = (LX ∘→^{f′} ↑ (f))
⇒ (LX ∘→^{Lh} LY ∘→ ↑ (f) ▷→ C) = (LX ∘→^{f′} ↑ (f) ▷→ C) = f.  □

Definition 6.3 Let Preo be the category of small preorders and monotone functions. □

Theorem 6.4 The category C equipped with ⊑ (henceforth denoted C_{⊑}) is a Preo-cartesian-closed-category.

Proof: By Proposition 4.4 (1) the path relation is reflexive. To see that it is transitive first observe that, by Proposition 6.2 and the fact that left adjoints preserve weak colimits, the pullback

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

is a weak pushout. Now, if f ⊑ g ⊑ h : A → B then there exist α : f g and β : g h making Σ × A ⟶^{α} B ⟵^{β} Σ × A a cone for (2) and any mediating morphism γ : Σ_{2} × A → B makes γ : f _{2} h.

Finally, by Proposition 4.4 (3), the composition of morphisms is a monotone operation with respect to the path preorder. And, by Proposition 4.4 (6–7), the cartesian closed structure is Preo-enriched. □

By Proposition 4.4 (5) we have:

Proposition 6.5 𝕃 determines a Preo-monad on C_{⊑} and hence the category of Eilenberg-Moore algebras C^{𝕃} and the Kleisli category C_{𝕃} ≅ p(C, D) Preo-enrich w.r.t. ⊑. □

Proposition 6.6 Coproducts in C_{⊑} are Preo-enriched. □

7 Approximation and upper-closure

Axiom 1 allows a characterisation of approximation in terms of upper-closure: for two elements x and y, we have that x approximates y if and only if the minimal upper-closed containing x includes the minimal upper-closed containing y. More precisely,

Proposition 7.1 The following are equivalent:

1. x y : 1 → A.

2. ↑ (x) ⊇ ↑ (y).

3. y factors through ↑ (x) ▷→ A.

Proof:

(1) ⇒ (2) Let α : x y. Then,

1 ↑ (x)  A Σ α′  α ∘ ⟨Σ, Σ → 1⟩

and hence

1 ⊤Σ α′  ↑ (y) ↑ (x)  A .

(2) ⇒ (1) Let y′ = (1 ∘→ ↑ (y) ▷→ ↑ (x)) and let α = (Σ ∘⟶^{Ly′} L(↑ x) ⟶^{ρ_{↑(x)}} ↑ (x) ▷→ A). Then, α : x y.

(2) ⟺ (3) Straightforward. □

Corollary 7.2 (A → 1 ⟶^{b} B) f if and only if f factors through ↑ (b) ▷→ B.

Proof: For every y : 1 → B we write Ky for the composite (A → 1 ⟶^{y} B).

Then,

Kb f : A → B
⟺ ⌜Kb⌝ ⌜f⌝ : 1 → B^{A}
⟺ ⌜f⌝ factors through ↑ (⌜Kb⌝) ▷→ B^{A}
⟺ ⌜f⌝ factors through (↑ (b) ▷→ B)^{A} : (↑ b)^{A} ▷→ B^{A}
, because ⌜Kb⌝ = (1 ∘⟶^{⌜Kb′⌝} (↑ b)^{A} ▷→^{m^{A}} B^{A}) whenever b = (1 ∘⟶^{b′} ↑ (b) ▷→^{m} B)
⟺ f factors through ↑ (b) ▷→ B.  □

8 Lifting as a lax colimit

In this section, by introducing Axiom 2, we are able to provide a characterisation of lifting as a lax colimit.

We recall the definition of lax colimit. Let A_{≤} be a Preo-category and let A be its underlying ordinary category. Let Δ : G → A. A lax cone for Δ with vertex A, ⨿ : Δ \underrightarrow{.}_{≥}A, is an indexed family of morphisms ⨿_{M} : ΔM → A (M ∈ | G |) in A such that, for e : M → N in G, ⨿_{M} ≥ ⨿_{N} ∘ Δe. We write LaxCone(Δ, A) (LaxCone_{≤}(Δ, A)) for the collection of lax cones for Δ with vertex A (preordered pointwise).

Consider G small. A lax cone ⨿ : Δ \underrightarrow{.}_{≥}A is colimiting if

∘ ⨿ : A(A, ) ≅ LaxCone(Δ, ) : A → Set

and it is Preo-colimiting if

∘ ⨿ : A_{≤}(A, ) ≅ LaxCone_{≤}(Δ, ) : A → Preo.

Remark. (Weak) lax colimits are preserved by left adjoints.

We have:

Proposition 8.1 For every A ∈ | C |, the lax cone

LA  1 ⊒ Aη_{A}  ⊥_{LA}  (3)

is weak colimiting.

Proof: Let (A →^{f} B) ⊒ (A → 1 ⟶^{b} B). Then, by Corollary 7.2, f = (A → ↑ (b) ▷→ B). So, letting LA ∘→↑ (b) be the unique strict extension of A → ↑ (b), we have that LA ∘→↑ (b)▷→B mediates between

A ↪^{η_{A}} LA ⟵∘^{⊥_{LA}} 1 and A ⟶^{f} B ⟵^{b} 1 because

(A ↪^{η_{A}} LA ∘→ ↑ (b) ▷→ B) = (A → ↑ (b) ▷→ B) = f

and

(1 ∘→ LA ∘→ ↑ (b) ▷→ B) = (1 ∘→ ↑ (b) ▷→ B) = b. □

Axiom 2 For every A ∈ | C |, A ↪^{η_{A}} LA ⟵∘^{⊥_{LA}} 1 are jointly epi. □

Corollary 8.2 1. The lax cone (3) is colimiting.

2. Convention. For n ≥ 0, we inductively define η_{C}^{(n)} : C ↪ L^{n}C as η_{C}^{(0)} = C and η_{C}^{(n+1)} = η_{L^{n}C} ∘η_{C}^{(n)} = η_{LC}^{(n)} ∘ η_{C}.

For h : X ∘→ Y, the pullbacks

Y × A L^{n}Y × A η_{Y}^{(n)} × A X × A η_{X}^{(n)} × A L^{n}X × A L^{n}h × A h × A

are pushouts. □

The following characterisation of Axiom 2 for the case A = 1 (especially Proposition 8.3 (2) stating that there is at most one path of length one between any two maps) should help in understanding the axiom.

Proposition 8.3 The following are equivalent:

1. 1 ↪^{⊤} Σ ⟵∘^{⊥} 1 are jointly epi.

2. If α, β : f g : A → B then α = β.

3. The map C(A, B^{Σ}) → Preo(2, C_{⊑}(A, B)) : α ∣→ ⟨B^{⊥} ∘ α ⊑ B^{⊤} ∘ α⟩ is a bijection. □

Proposition 8.4 Colimits in C_{⊑} are Preo-enriched. □

9 An algebra of paths

Using versions of Corollary 8.2 (2) we define a composition operation for paths:

Definition 9.1 For f, g : A → B and α : Σ_{m} × A → B we set α : f g if and only if α : f _{m} g.

And given f ^{α} g ^{β} h : A → B we define β • α : f h as the unique mediating morphism in the diagram

η_{Σ_{n}}^{(m)} × A 1 × A ⊤_{m} × A Σ_{m} × A  α  Bβ Σ_{m+n} × A  . β • α Σ_{n} × A L^{m}⊥_{n} × A ⊥_{n} × A  □

It follows that C is the underlying category of a sesqui-category with paths as 2-cells:

Proposition 9.2 1. For every A, B ∈ | C |, C(A, B) with , • and id_{f} (defined in Proposition 4.4 (1))

is a category.

2. C with , •, id_{f} and id_{g} ⋆α⋆id_{f} (defined in Proposition 4.4 (2)) is a sesqui-category (i.e. a category enriched over CAT, the category of locally small categories and functors, with the funny symmetric monoidal closed structure —see e.g. [Str92]). □

10 Lifting as a KZ-doctrine

We recall the definition of KZ-doctrine (when the 2-categorical structure is quasi-posetal):

Definition 10.1 ([Koc94]) A KZ-doctrine on a Preo-category A_{≤} consists of a Preo-monad 𝕋 = (T, η, μ) : A_{≤} → A_{≤} such that, for every A ∈ | A_{≤} |, T η_{A} ≤ η_{T A}. □

The last axiom (Axiom 3) which together with Axiom 2 makes C_{⊑} have cotensors with the Sierpinski space is introduced. From it we deduce that lax colimits are Preo-enriched, and from the Preo-enrichment of the lax colimit (3) the inequality needed to make 𝕃 into a KZ-doctrine follows.

To state Axiom 3 we need the following:

Definition 10.2 Let \overline{0} = (1 ∘⟶^{⊥} Σ ∘⟶^{L⊥} Σ_{2}), \overline{1} = (1 ↪^{⊤} Σ ∘⟶^{L⊥} Σ_{2}) = (1 ∘⟶^{⊥} Σ ↪^{η_{Σ}} Σ_{2}) and

\overline{2} = (1 ↪^{⊤} Σ ↪^{η_{Σ}} Σ_{2}). □

Convention. For f ⊑ g : A → B, we set [f ⊑ g] : f g. And, for f ⊑ g ⊑ h : A → B we write [f ⊑ g ⊑ h] for [g ⊑ h] • [f ⊑ g] (see Definition 9.1).

Axiom 3 The commuting square

Σ × Σ [⟨⊥, ⊥⟩ ⊑ ⟨⊥, ⊤⟩ ⊑ ⟨⊤, ⊤⟩]  [⟨⊥, ⊥⟩ ⊑ ⟨⊤, ⊥⟩ ⊑ ⟨⊤, ⊤⟩] Σ [\overline{0} ⊑ \overline{2}]  [\overline{0} ⊑ \overline{2}]  Σ_{2} Σ_{2}  (4)

is a pushout. □

More illuminating than the axiom is the following characterisation:

Proposition 10.3 The following are equivalent:

1. Axiom 3.

2. (Diamond property) If

f′  g f g′  (5)

in C_{⊑}(A, B) then [f ⊑ f′] ⊑ [g ⊑ g′] : Σ × A → B.

3. The monotone map C_{⊑}(A, B^{Σ}) → Preo_{⊑}(2, C_{⊑}(A, B)) : α ∣→ ⟨B^{⊥} ∘ α ⊑ B^{⊤} ∘ α⟩ is an isomorphism of preorders. (Hence, C_{⊑} has cotensors with the Sierpinski space 2.)

Proof:

(1) ⇒ (2) Assume (5). Set C = B^{A}, x = ⌜f⌝, x′ = ⌜f′⌝, y = ⌜g⌝, y′ = ⌜g′⌝, and let μ : Σ × Σ → C

be the unique mediating morphism from the pushout (4) to the cone Σ_{2} ⟶^{[x⊑x′⊑y′]} C ⟵^{[x⊑y⊑y′]} Σ_{2}.

Then, since μ ∘ ⟨⊤ ∘ (Σ → 1), Σ⟩ ∘ ⊤ = y′ and μ ∘ ⟨⊤ ∘ (Σ → 1), Σ⟩ ∘ ⊥ = y it follows that μ ∘ ⟨⊤ ∘ (Σ → 1), Σ⟩ = [y ⊑ y′]. Also, μ ∘ ⟨⊥ ∘ (Σ → 1), Σ⟩ ∘ ⊤ = x′ and μ ∘ ⟨⊥ ∘ (Σ → 1), Σ⟩ ∘ ⊥ = x so μ ∘ ⟨⊥ ∘ (Σ → 1), Σ⟩ = [x ⊑ x′]. Hence, μ : [x ⊑ x′] [y ⊑ y′] and thus [f ⊑ f′] ⊑ [g ⊑ g′].

(2) ⇒ (1) If μ : Σ × Σ → C mediates between the pushout (4) and a cone Σ_{2} ⟶^{f} C ⟵^{g} Σ_{2} for it, then μ : [f ∘ \overline{0} ⊑ f ∘ \overline{1}] [g ∘ \overline{1} ⊑ g ∘ \overline{2}]. This shows the uniqueness of the mediating morphism. For existence consider

f ∘ \overline{1} f ∘ \overline{2} = g ∘ \overline{2} f ∘ \overline{0} = g ∘ \overline{0}  . g ∘ \overline{1}

Then, by the diamond property, [f ∘ \overline{0} ⊑ f ∘ \overline{1}] ⊑ [g ∘ \overline{1} ⊑ g ∘ \overline{2}]. Finally, take μ to be the unique such that μ : [f ∘ \overline{0} ⊑ f ∘ \overline{1}] [g ∘ \overline{1} ⊑ g ∘ \overline{2}].

(2) ⇒ (3) It is enough to show that the mapping

Preo_{⊑}(2, C_{⊑}(A, B)) → C_{⊑}(Σ, B^{A}) : ⟨f ⊑ f′⟩ ∣→ [⌜f⌝ ⊑ ⌜f′⌝]

is monotone.

Let f ⊑ f′ and g ⊑ g′ be such that f ⊑ g and f′ ⊑ g′. Then,

⌜f′⌝ ⌜g′⌝ ⌜g⌝ ⌜f⌝

and, by the diamond property, [⌜f⌝ ⊑ ⌜f′⌝] ⊑ [⌜g⌝ ⊑ ⌜g′⌝].

(3) ⇒ (2) Because (2) is equivalent to the monotonicity of the mapping

Preo_{⊑}(2, C_{⊑}(A, B)) → C_{⊑}(Σ × A, B) : ⟨f ⊑ f′⟩ ∣→ [f ⊑ f′]. □

Remark. Axiom 3 does not hold in categories of domains and stable functions. In fact the diamond property exhibits a crucial difference between the pointwise and the stable order; for example, the following proposition does not hold in Poset_{∧} and Cpo_{∧} (c.f. [Fio94b]).

Proposition 10.4 Lax colimits in C_{⊑} are Preo-enriched.

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 ∘ ⨿_{M} f ∘ ⨿^{N} ∘ Δe g ∘ ⨿_{M} g ∘ ⨿_{N} ∘ Δe

so that

[f ∘ ⨿_{M} ⊑ g ∘ ⨿_{M}] ⊒ [f ∘ ⨿_{N} ∘ Δe ⊑ g ∘ ⨿_{N} ∘ Δe] , by the diamond property
= [f ∘ ⨿_{N} ⊑ g ∘ ⨿_{N}] ∘ Δe

and hence Γ =^{def} ⟨[f ∘ ⨿_{M} ⊑ g ∘ ⨿_{M}]⟩_{M} : Δ × Σ \underrightarrow{.}_{≥}D.

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

Finally, if α : Σ × C → D is the unique mediating morphism between Σ × ⨿ : Σ × Δ \underrightarrow{.}_{≥}Σ × C and Γ : Σ × Δ \underrightarrow{.}_{≥}D we have that α : f g because:

1 × ⨿ ⨿  Δ ≅ 1 × Δ C ≅ 1 × C  Σ × Δ Σ × C Σ × ⨿  D Γ  α ⊤ × Δ g ∘ ⨿⊤ × C Δ ≅ 1 × Δ C ≅ 1 × C ⊥ × C ⊥ × Δ Σ × Δ Σ × C Σ × ⨿  D f ∘ ⨿  Γ  α 1 × ⨿  ⨿

and hence α ∘ (⊥ × C) = f ∘ π_{1} whilst α ∘ (⊤ × C) = g ∘ π_{1}. □

Corollary 10.5 The lifting monad 𝕃 is a KZ-doctrine on C_{⊑}.

Proof: Because 𝕃 is a Preo-monad and, for every A ∈ | C |, since (Lη_{A}) ∘ η_{A} = η_{LA} ∘ η_{A} and (Lη_{A}) ∘ ⊥_{LA} = ⊥_{L^{2}A} ⊑ η_{LA} ∘ ⊥_{LA} it follows, using that the lax cone (3) is Preo-colimiting, that Lη_{A} ⊑ η_{LA}. □

From [Koc94] we know that: for every pointed object X, ρ_{X} ⊣_{r} η_{X} (i.e. algebra structures are reflections to units) because ρ_{X} ∘η_{X} = X and η_{X} ∘ρ_{X} = L(ρ_{X})∘η_{X} ⊒ L(ρ_{X})∘Lη_{X} = L(ρ_{X} ∘η_{X}) = LX; moreover, for every object A, Lη_{A} ⊣_{cor} μ_{A} ⊣_{r} η_{LA}.

It follows that the two equivalent statements in the following proposition hold:

Proposition 10.6 Pointed objects have a unique algebra structure (up to path equivalence) if and only if isomorphisms are strict (up to path equivalence).

Proof:

(⇒) Let X and Y be pointed objects, and let f : X ≅ Y : g in C. We show that g ∘ ρ_{Y} ∘ Lf provides an algebra structure on X and hence ρ_{X} ≡ g ∘ ρ_{Y} ∘ Lf; so that, by Proposition 4.4 (3), f ∘ ρ_{X} ≡ ρ_{Y} ∘ Lf.

Writing x for g ∘ ρ_{Y} ∘ Lf, we have that

x ∘ η_{X} = g ∘ ρ_{Y} ∘ (Lf) ∘ η_{X} = g ∘ ρ_{Y} ∘ η_{Y} ∘ f = g ∘ f = X

and that

x ∘ Lx = g ∘ ρ_{Y} ∘ (Lf) ∘ L(g ∘ ρ_{Y} ∘ Lf) = g ∘ ρ_{Y} ∘ (Lρ_{Y}) ∘ (L^{2}f)
= g ∘ ρ_{Y} ∘ μ_{Y} ∘ (L^{2}f)  = g ∘ ρ_{Y} ∘ (Lf) ∘ μ_{X}
= x ∘ μ_{X}.

(⇐) Because identities are strict. □

Acknowledgements. I am indebted to Gordon Plotkin and John Power for conversations, to Paul Taylor for pointing out that a previous definition of upper-closure that I had was equivalent to being orthogonal to strict maps, and to the referees for useful comments.

References

[Bro88] R. Brown. Topology: a geometric account of general topology, homotopy types and the fundamental grupoid. Halsted Press, 1988.

[CPR91] A. Carboni, M.C. Pedicchio, and G. Rosolini, editors. Category Theory, volume 1488 of Lecture Notes in Mathematics. Springer-Verlag, 1991.

[Fio93] M. P. Fiore. Cpo-categories of partial maps. In CTCS-5 (Category Theory and Computer Science Fifth Biennial Meeting), pages 45–49. CWI, September 1993.

[Fio94a] M. P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, University of Edinburgh, 1994. (Available as technical report ECS-LFCS-94-307 or from http://www.dcs.ed.ac.uk/home/mf/thesis.dvi.Z).

[Fio94b] M. P. Fiore. First steps on the representation of domains. Manuscript (available from http://www.dcs.ed.ac.uk/home/mf/path.dvi), December 1994.

[Fio94c] M. P. Fiore. Order-enrichment for categories of partial maps. Mathematical Structures in Computer Science, 1994. To appear.

[FP94] M.P. Fiore and G.D. Plotkin. An axiomatisation of computationally adequate domain theoretic models of FPC. In 9^{th} LICS Conference, pages 92–102. IEEE, 1994.

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

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

[Koc91] A. Kock. Algebras for the partial map classifier monad. In [CPR91], pages 262–278, 1991.

[Koc94] A. Kock. Monads for which structures are adjoints to units. Manuscript (to appear in the Journal of Pure and Applied Algebra), 1994.

[Mog86] E. Moggi. Categories of partial morphisms and the partial lambda-calculus. In Proceedings Workshop on Category Theory and Computer Programming, Guildford 1985, volume 240 of Lecture Notes in Computer Science, pages 242–251. Springer-Verlag, 1986.

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

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

[Str92] R. Street. Categorical structures. Manuscript (to appear in the Handbook of Algebra volume 2, Elsevier, North Holland), November 1992.

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

This article was processed using the LaTEX macro package with LLNCS style