Complete Cuboidal Sets in Axiomatic Domain Theory

(Extended Abstract)

Marcelo Fiore^{∗}

<mf@dcs.ed.ac.uk>

Gordon Plotkin^{†}

<gdp@dcs.ed.ac.uk>

John Power^{∗}

             <ajp@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

Abstract

We study the enrichment of models of axiomatic domain theory. To this end, we introduce a new and broader notion of domain, viz. that of complete cuboidal set, that complies with the axiomatic requirements. We show that the category of complete cuboidal sets provides a general notion of enrichment for a wide class of axiomatic domain-theoretic structures.

Introduction

The aim of Axiomatic Domain Theory (ADT) is to provide a conceptual understanding of why domains are adequate as mathematical models of computation. (For a discussion see [12, § Axiomatic Domain Theory].) The approach taken is to axiomatise the structure needed on a category so that its objects can be considered as domains, and its maps as continuous functions. The task of ADT is to explain the traditional approach, and also to provide new concepts and theorems. In particular, part of our agenda is to establish a representation theory for domains. Here, as a first step, we concentrate on the enrichment of models of ADT. The intention is that the enriched Yoneda-Grothendieck-Dedekind-Cayley embedding [27] will provide the desired representation (c.f. [15, 11]).

Axiomatic versions of various traditional results in domain theory can be found in e.g. [39, 16, 17, 38, 13, 9, 11, 32]. For instance, in [39], the crucial rôle of Cpo-enrichment in the solution of recursive domain equations was recognised and made the central concept of an abstract version of the limit/colimit coincidence theorem [36].

From an axiomatic viewpoint, however, it is desirable not to assume any order-theoretic structure but rather to derive it. The study of the enrichment of domain-theoretic structures in an axiomatic framework began in [11]. There, for a strong axiomatisation, every axiomatic domain-theoretic category was shown to enrich over Cpo (the category of small ω-cpos and continuous functions) with respect to an intensional notion of approximation, viz. the path relation (see e.g. [8]).

In this paper we study the issue of enrichment for the weakest possible axiomatisation (along the lines of [11] that is). To account for the notions of domain permitted by this axiomatic theory we are forced to abandon Cpo-enrichment. Indeed, already the axiomatic considerations of [11] suggested a category of domains that cannot be Cpo-enriched in a relevant sense. Thus, what is needed is to broaden the notion of domain!

We take a radical approach and consider domains with a notion of (higher-dimensional) path replacing the traditional notion of approximation formalised by order-theoretic structures. Further, these domains have an algebraic (rather than a universal) notion of passage to the limit (traditionally formalised by lubs). This results in a new notion of domain, viz. that of a complete cuboidal set, complying with the axiomatic requirements.

Cuboidal sets play a rôle similar to that played by posets in the traditional setting. They are the analogue of simplicial sets (see e.g. [28, 26]) but with the simplicial category enlarged to the cuboidal category of cuboids, i.e. of finite products 𝕆_{n_{1}} × … × 𝕆_{n_{i}} of finite ordinals. These cuboids are the possible shapes of paths. A cuboidal set P has a set P (C) of paths of every shape C = 𝕆_{n_{1}} × … × 𝕆_{n_{i}}; indeed, it is a (rooted) presheaf over . The set of points of P is P (𝕆_{1}). The set of (one-dimensional) paths of length n is P (𝕆_{n+1}); they can be thought of as (linear) computations conditional on the occurrence of n linearly ordered events e_{1} ≤ … ≤ e_{n}. Evidently, 𝕆_{n} is the partial order associated to this simple linear event structure [30], and can be considered as a sequential process of length n. At higher dimensions, P (𝕆_{n_{1}} × … × 𝕆_{n_{i}}) can be thought of as the set of computations conditional on the occurrence of n_{1} + … + n_{i} events ordered by e_{1,1} ≤ … ≤ e_{1,n_{1}}; …; e_{i,1} ≤ … ≤ e_{i,n_{i}}. This is the event structure which can be considered as i sequential processes, of respective lengths n_{1}, …, n_{i}, running concurrently.

∗Research supported by EPSRC grant GR/J84205, Frameworks for Programming Language Semantics and Logic.

†Research supported by an EPSRC Senior Fellowship.

Complete cuboidal sets are cuboidal sets equipped with a formal-lub operator satisfying three algebraic laws, which are exactly those needed of the lub operator in order to prove the fixed-point theorem [35]. Computationally, the passage from cuboidal sets to complete cuboidal sets corresponds to allowing infinite processes. In fact, the formal-lub operator assigns paths of shape C to ‘paths of shape C × ω’, for every C. Here the set of paths of shape C ×ω is the colimit of the paths of shape C × 𝕆_{n}; such paths can be thought of as the higher-dimensional analogue of the increasing sequences of traditional domain theory.

Analogous to what happens in the traditional setting between cpos and posets, the category of complete cuboidal sets appears as the category of Eilenberg-Moore algebras for a certain ideal-completion monad on the category of cuboidal sets.

As a central result of the paper we provide an enrichment theorem stating that every axiomatic domaintheoretic lifting monad enriches over the category of complete cuboidal sets; as a corollary, so does every domain-theoretic model of recursive types in a wide class.

Organisation of the paper. Section 1 presents the basic structures needed in the rest of the paper and their relationships. In Section 2 we show how to construct models of ADT. To this end, we introduce an algebraic notion of passage to the limit, and describe the ideal-completion monad. This theory is applied in Section 3 to obtain the notion of complete cuboidal set. In Section 4, domain-theoretic lifting monads and domain-theoretic models of recursive types are shown to enrich with respect to the category of complete cuboidal sets. Section 5 indicates further directions for research.

1 Basic concepts

We review the basic structures for discussing models of ADT. Domain-theoretic commutative monads are the central concept of study; the special case of lifting is only needed for Section 4. (For the notion of monad see [28]; for the notion of commutative monad see [24, 29]; for the notion of lifting monad see Appendix A.)

Free algebras and fixed-point objects. An algebra for an endofunctor is said to be free [17] if it is initial and if its inverse is a final coalgebra.

A fixed-point object [7] for a monad 𝕃 = (L, η, μ) on a category with a terminal object 1 is an initial L-algebra Lw → w equipped with a global element 1 → w invariant under the successor loop succ =^{def} w ^{η_{w}}→ Lw → w.

Theorem 1.1 For a commutative monad (L, η, μ, t) on a cartesian closed category, the following are equivalent:

1. The pair of arrows L\overline{ω} ^{σ}→ \overline{ω} ←^{∞} 1 is a fixedpoint object.

2. The algebra σ : L\overline{ω} → \overline{ω} is free and ∞ : 1 → \overline{ω} is the unique mediating coalgebra morphism from η_{1} : 1 → L1 to σ^{−1} : \overline{ω} → L\overline{ω}.

Moreover, when either condition is satisfied, the dia-

gram 1 ^{∞}→ \overline{ω} →^{succ} ; _{_{id}→} \overline{ω} is an equaliser.

The fixed-point object for a monad provides a unique uniform fixed-point operator for endomorphisms on objects with bottom (viz. objects equipped with an Eilenberg-Moore algebra structure) —see [7, 17].

Proposition 1.2 Let 𝕃 be a commutative monad on a cartesian closed category C. Assume that L has a free algebra. Then,

1. the terminal object 1 in C becomes a zero object in the category of Eilenberg-Moore algebras C^{𝕃}, and

2. if C has an initial object 0 then L0 ≅ 1 and so 0 becomes a zero object in the Kleisli category C_{𝕃}.

In the situation of the above proposition, one typically writes ⊥_{(A,a)} for the unique 𝕃-algebra homomorphism from the zero 𝕃-algebra L1 → 1 to an 𝕃-algebra a : LA → A. Notice that the endofunctor L is pointed (i.e. it comes equipped with a global element). Indeed, the family {⊥_{(LA,μ_{A})} : 1 → LA} is a natural transformation 1 \underrightarrow{.} L.

Domain-theoretic commutative monads. An algebra s : Lw → w for an endofunctor L on a category with an initial object 0 is said to be inductive if the cone ⟨[s]_{n}⟩ : ⟨L^{n}(0 → L0)⟩ \underrightarrow{.} w inductively defined by [s]_{0} =^{def} (0 → w) and, for n ≥ 0, by [s]_{n+1} =^{def} s ∘ L[s]_{n}, is colimiting.

A pre-domain-theoretic commutative monad is a commutative monad 𝕃 on a cartesian closed category with an initial object, equipped with an inductive initial L-algebra (henceforth denoted ς : Lω → ω).

Examples of pre-domain-theoretic commutative monads are the identity monad; the ( ) + 1 monad on Set (the category of small sets and functions); and the lifting monad ( )_{⊥} on Preo (the category of small preorders and monotone functions), on Poset (the category of small posets and monotone functions), and on Poset_{∧} (the category of small posets with pullbacks —i.e. binary bounded infs— and stable —i.e. pullback preserving— functions).

A domain-theoretic commutative monad 𝕃 is a predomain-theoretic commutative monad in which the inductive initial L-algebra is free. In this context, the free L-algebra is denoted σ : L\overline{ω} → \overline{ω} and the global element 1 → \overline{ω} invariant under succ is denoted ∞.

Examples of domain-theoretic commutative monads are the lifting monad ( )_{⊥} on Cpo (the category of small ω-cpos and continuous functions) and on Cpo_{∧} (the category of small ω-cpos with continuous pullbacks and stable continuous functions). The identity monad is domain-theoretic only on trivial cartesian closed categories.

Models of linear type theory. A symmetric monoidal functor (H, e, m) : V → V′ between symmetric monoidal categories (see [28] for this notion) consists of a functor H : V → V′, a morphism e : I′ → HI, and a natural transformation m_{A,B} : HA⊗′HB → H(A⊗B) such that

m_{A,B⊗C} ∘ (id_{HA} ⊗′ m_{B,C}) ∘ a′_{HA,HB,HC} = H(a_{A,B,C}) ∘ m_{A⊗B,C} ∘ (m_{A,B} ⊗′ id_{HC}),

r′_{HA} = H(r_{A}) ∘ m_{I,A} ∘ (e ⊗ id_{HA}),

m_{B,A} ∘ c′_{HA,HB} = H(c_{A,B}) ∘ m_{A,B}.

A symmetric monoidal functor is said to be strong if e and m_{A,B} are isomorphisms.

There is a standard process that to a symmetric monoidal functor H : V → V′ associates a 2-functor H_{∗} : V-CAT → V′-CAT, where for a monoidal category W we write W-CAT for the (possibly large) 2-category of W-categories, W-functors, and W-natural transformations. For a V-category K, the V′-category H_{∗}K has the same objects as K, hom-objects H_{∗}K(A, B) =^{def} HK(A, B), identities I′ → HI → HK(A, A), and composition HK(B, C) ⊗′ HK(A, B) → H(K(B, C) ⊗ K(A, B)) → HK(A, C). If H is strong, the underlying ordinary categories K_{0} and (H_{∗}K)_{0} are isomorphic.

A model of (intuitionistic) linear type theory [3] is given by a strong symmetric monoidal functor F : C → D between a cartesian closed category C and a symmetric monoidal closed category D with finite products, such that the functor F has a right adjoint. It follows that the right adjoint is a symmetric monoidal functor and thus that the monad on C induced by the adjunction, henceforth denoted 𝕃, is commutative.

The following folklore result (see [21] and the references therein) relates (accessible) commutative monads (on locally presentable cartesian closed categories) to models of linear type theory. (For the notions of locally presentable category and accessible monad see Appendix B.)

Theorem 1.3 Let 𝕃 be an accessible commutative monad on a locally presentable cartesian closed category C. Then, C \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} C^{𝕃} provides a model of linear type theory.

In the above theorem, the symmetric monoidal structure on C^{𝕃} is given by the tensor product ⊗ of algebras; defined, for algebras X and Y, as the universal bilinear map X × Y → X ⊗ Y. For details consult [25, 21].

Models of Axiomatic Domain Theory. Domaintheoretic commutative monads and models of linear type theory provide the enrichment structure for defining models of ADT.

A domain-theoretic enrichment base is a model of linear type theory such that its induced commutative monad is domain-theoretic.

A domain-theoretic model of recursive types with respect to a domain-theoretic enrichment base F : C \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} D : U is a D-category M such that the C-category U_{∗}M is C-algebraically compact (see [17, 9, 32] for this notion). The rôle of algebraic compactness is to provide a universal approach for solving recursive type equations. What is domaintheoretic about these models is that fixed-points of endofunctors (viz. free algebras) are obtained by traditional domain-theoretic methods; viz. the basic lemma [39] and a version of the limit/colimit coincidence theorem [32].

Models of ADT are domain-theoretic models of recursive types admitting a rich type structure (e.g. suitable for interpreting products, higher types, and sums). Canonical examples of models of ADT are pCpo (the category of small ω-cpos and partial continuous functions [31]) and Cppo_{⊥} (the category of small ω-cpos with bottom element and strict continuous functions) with respect to the domain-theoretic enrichment base

( )_{⊥} : Cpo \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} Cppo_{⊥}.

2 Constructing models of ADT

We explore the construction of models of ADT, first from domain-theoretic commutative monads, then from pre-domain-theoretic ones.

2.1 From domain-theoretic commutative monads

The models of ADT Cppo_{⊥} and pCpo are obtained as an application of the following result to the lifting monad on Cpo.

Theorem 2.1 Let 𝕃 be an accessible commutative monad on a locally presentable cartesian closed category C. Assume that L has an inductive free algebra. Then,

1. the category of Eilenberg-Moore algebras C^{𝕃} is a domain-theoretic model of recursive types with respect to the domain-theoretic enrichment base

C \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} C^{𝕃}, and

2. when 𝕃 is a lifting monad, the Kleisli category C_{𝕃} is also a domain-theoretic model of recursive types with respect to the domain-theoretic enrichment base C \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} C^{𝕃}.

Another traditional domain-theoretic commutative monad satisfying the hypothesis of the theorem is the lifting monad on Cpo_{∧}.

2.2 From pre-domain-theoretic commutative monads

Formally ω-complete objects. Domains are spaces equipped with a notion of approximation (the information order) and a notion of passage to the limit (the lub operator). We now consider objects with an algebraic (rather than a universal) notion of passage to the limit. To this purpose we introduce a notion of formal-lub operator [12, § Axiomatic Domain Theory].

Consider a pre-domain-theoretic commutative monad 𝕃 = (L, η, μ, t) on C. Think of the lifting monad on Poset. Recall that we write ς : Lω → ω for the inductive initial L-algebra, and write succ for the successor loop ω ^{η_{ω}}→ Lω ^{ς}→ ω. A formal-lub operator (for ω-chains under the invariance succ) on an object D in C is given by a map ⋁ : D^{ω} → D in C satisfying the following three algebraic laws:

(Constant) \begin{matrix}D & \overline{\underrightarrow{D^{!}}} & D^{ω} \\ [figure] & _{id_{D}} &  \\ D & ^{↓⋁} \end{matrix}  (i.e. ⋁_{n}⟨x⟩ = x),

(Diagonal)  \begin{matrix}D^{ω×ω} & ≅ & (D^{ω})^{ω} & \overline{\underrightarrow{^{⋁ω}}} & D^{ω} \\ D^{ω} & ^{D^{Δ}↓} & \overline{⋁  →} & D & ^{↓⋁} \end{matrix}

(i.e. ⋁_{n}⟨⋁_{m}⟨x_{m,n}⟩⟩ = ⋁_{n}⟨x_{n,n}⟩),

(Shift)  \begin{matrix}D^{ω} & \overline{\underrightarrow{D^{succ}}} & D^{ω} \\ [figure] & ⋁ &  \\ D & ^{↓⋁} \end{matrix}

(i.e. ⋁_{n}⟨x_{n}⟩ = ⋁_{n}⟨x_{succ(n)}⟩).

A formally ω-complete object is an object equipped with a formal-lub operator. For formally ω-complete objects (P, ⋁_{P}) and (Q, ⋁_{Q}), a map f : P → Q in C is said to be ω-continuous if it satisfies the following law:

(Continuity)  \begin{matrix}P^{ω} & \overline{\underrightarrow{f^{ω}}} & Q^{ω} \\ P & ^{⋁P}↓ & \overline{_{f→}} & Q & ↓^{⋁Q} \end{matrix}

(i.e. f(⋁_{P} ⟨x_{n}⟩) = ⋁_{Q}⟨f(x_{n})⟩).

We write ⋁(C) for the category of formally ω-complete objects and ω-continuous maps. For our running example, ⋁(Poset) is Cpo, the category of ω-complete posets and ω-continous functions. If we perform the construction on Preo (the category of preorders and monotone functions) we obtain the same result; ⋁(Preo) is again Cpo. The real surprise comes when we consider the construction on structures with not only a one-dimensional notion of approximation (as the above examples) but also with higher-dimensional notions of approximation. For instance, consider Poset_{∧}; the pullback “squares” in the posets provide a (particular) “two-dimensional” notion of path. Then, the category ⋁(Poset_{∧}) strictly contains the category Cpo_{∧} as a full subcategory and cannot be enriched over Cpo in a relevant sense; see [11]. However, in ⋁(Poset_{∧}) the constructions of domain theory are possible (e.g. ⋁(Poset_{∧}) has finite sums, is cartesian closed, and admits a lifting monad which satisfies the hypothesis of Theorem 2.1). In the next section we will generalise this to cuboidal sets, our structures with (general) finite higher-order notions of path.

A more succint presentation of the ⋁-construction is as follows. Consider the exponentiation commutative monad 𝕎 on C with underlying endofunctor ( )^{ω}, unit

D^{!} : D → D^{ω}, multiplication (D^{ω})^{ω} ≅ D^{ω×ω} ^{D^{Δ}} → D^{ω}, and tensorial strength A × D^{ω} → (A × D)^{ω} the exponential transpose of the composite (A × D^{ω}) × ω ≅ A × (D^{ω} × ω) ^{id_{A}×eval} → A × D (where eval denotes the evaluation map). Then ⋁(C) is the full subcategory of the category of Eilenberg-Moore algebras C^{𝕎} consisting of the algebras satisfying (Shift).

As in traditional domain theory the formal-lub operator allows the definition of a fixed-point operator for endomorphisms on objects with bottom. Define a formally ω-complete pointed object to be a triple (D, d : LD → D, ⋁_{D} : D^{ω} → D) where (D, d) is an 𝕃-algebra and (D, ⋁_{D}) is a formally ω-complete object. For an endomorphism f on D, let it_{(D,d)}(f) : ω → D be the unique L-algebra morphism from the initial L-algebra (ω, ς) to the L-algebra (D, f ∘ d), and set fix_{(D,d,⋁_{D})} =^{def} ⋁_{D} ∘ ⌜it(f)⌝. The algebraic laws of the formal-lub operator are enough to derive formal versions of the fixed-point and uniformity properties of the fixed-point operator.

Proposition 2.2 Let (A, a, ⋁_{A}) and (B, b, ⋁_{B}) be formally ω-complete pointed objects, let f be an endomophism on A and g an endomorphism on B, and let h be an 𝕃-algebra morphism from (A, a) to (B, b). Then,

1. f ∘ fix(f) = fix(f), and

2. if g ∘ h = h ∘ f then h ∘ fix(f) = fix(g).

The ⋁-construction. As we have seen above, sometimes the ⋁-construction takes us from a pre-domain-theoretic commutative monad (e.g. the lifting monad on Poset) to a domain-theoretic one (e.g. the lifting monad on Cpo). What happens if we perform the ⋁-construction on a domain-theoretic commutative monad?

Theorem 2.3 For a domain-theoretic commutative monad on a category C, the forgetful functor ⋁(C) → C is an isomorphism with inverse the functor sending an object D in C to the formally \overline{ω}-complete object (D, D^{∞} : D\overline{ω} → D) in ⋁(C).

Consider a domain-theoretic commutative monad 𝕃 on C. By the above theorem, every object D in C admits a unique formal-lub operator (viz. D^{∞} : D\overline{ω} → D) and so, for an 𝕃-algebra (D, d), we may simply write fix_{(D,d)} for fix_{(D,d,D^{∞})}. With this convention, for every endomorphism f on D, we have that fix_{(D,d)}(f) = it_{(D,d)}(f) ∘ ∞ (c.f. [7]).

Since the exponentiation functor ( )^{ω} preserves binary products, under a mild assumption the ⋁-construction preserves cartesian closure.

Proposition 2.4 Consider a pre-domain-theoretic commutative monad on a category C.

The forgetful functor ⋁(C) → C creates products, and hence ⋁(C) is cartesian. If in addition C has equalisers then ⋁(C) is cartesian closed.

Given a pre-domain-theoretic commutative monad 𝕃 on C, we will be interested in extending 𝕃 to ⋁(C). This is not always possible; e.g. for the ( ) + 1 monad on Set, the category ⋁(Set) is equivalent to the arrow category 0 → 1 . However, one can always extend 𝕃 to C^{𝕎}; this is equivalent to asking for a distributive law of 𝕃 over 𝕎 (see [2] for this notion).

Proposition 2.5 The transformation L( ^{ω}) → (L )^{ω} with components L(D^{ω}) → (LD)^{ω} defined as the expo-

nential transpose of L(D^{ω})×ω →^{t′} L(D^{ω}×ω) ^{L(eval)} → LD yields a distributive law of 𝕃 over 𝕎.

The ideal-completion monad. Consider a predomain-theoretic commutative monad 𝕃 on a category C. Every object in C admits a free formal ω-completion in ⋁(C) if the forgetful functor ⋁(C) → C is monadic. That is, if it has a left adjoint delivering free constructions such that the category of Eilenberg-Moore algebras for the monad on C induced by the adjunction C \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} ⋁(C) is equivalent to ⋁(C). In this case, the monad 𝕀 representing ⋁(C) as C^{𝕀} is called the idealcompletion monad (as it generalises the case of posets). The question arises as to when the ideal-completion monad 𝕀 exists and, if so, whether there exists a distributive law of 𝕃 over 𝕀 to extend 𝕃 to ⋁(C). Details of a general theory addressing these issues will appear elsewhere.

3 A standard domain-theoretic enrichment base

Cuboidal sets. We write 𝕆_{κ} for the ordinal associated to the cardinal κ.

The cuboidal category is defined as the full subcategory of Poset_{∧} determined by the objects (henceforth called cuboids) 𝕆_{n_{1}} × … × 𝕆_{n_{i}} where i ≥ 1, and 0 ≤ n_{j} < ℵ_{0} for all 1 ≤ j ≤ i.

For a small category C with an initial object 0, we write C̃ for the full subcategory of the presheaf topos [C^{op}, Set] consisting of the presheaves P such that P (0) ≅ 1. When the initial object in C is strict, C̃ is the sheaf topos obtained by declaring that the empty cover covers the initial object.

We call the category of cuboidal sets. There are two other presentations of . Let F be the full subcategory of Poset_{∧} containing the initial object and closed under finite products and lifting, and let FDL be the full subcategory of Poset_{∧} consisting of the finite distributive lattices. Since FDL is the Cauchy completion [27] of both and F, the full inclusions

↪ F ↪ FDL induce the following equivalences ≃ F̃ ≃ { \atop FDL}. The category F plays a crucial rôle in the enrichment theorem of Section 4.

The Yoneda embedding ↪ associating to a cuboid C the representable cuboidal set ( , C) provides a full and faithful representation of the cuboidal category into the category of cuboidal sets. As a notational convention, we identify the cuboidal category with its image under the Yoneda embedding in the category of cuboidal sets .

The internal structure of a cuboidal set may be grasped by looking at its paths. A path of shape a cuboid C in a cuboidal set P is a map C → P in (or equivalently, by Yoneda, an element of P (C)). To understand paths in some concrete cases it is instructive to look at the following embeddings. Let C be either Preo, Poset, or Poset_{∧} and let J denote the inclusion functor → C. Then, the functor N : C → associating to an object D in C the cuboidal set N(D) =^{def} C(J , D), called the nerve of D (c.f. [26]), is full and faithful.

A subset of a poset with pullbacks is said to be a stable open if it is upper-closed and closed under pullbacks. The set of stable opens of D in Poset_{∧} is denoted O_{∧}(D). In Poset_{∧} and , stable opens are closed under identities, composition, and pullbacks along arbitrary maps (i.e. they provide a class of admissible subobjects [33].)

The stable opens of a cuboid are easy to visualise; they are either empty or determined by a vertex of the cuboid. The notion of stable open can be extended from the cuboidal category to the category of cuboidal sets. The quickest way to this is by declaring a subobject O ↣ Q of a cuboidal set Q to be locally stable open if it appears in a pullback

\begin{aligned}O & \overline{→} & 𝕆_{1} \\ Q & ^{↓ ∨} & \overline{→} & 𝕆_{2} & ^{↓ ∩} \end{aligned}  (1)

where 𝕆_{1} ↪ 𝕆_{2} is the unique mono with stable-open image. Equivalently, a subobject O ↣ Q in is locally stable open if and only if, for every cuboid C in and every path C → Q in , we have a pullback square

\begin{aligned}V & \overline{→} & O \\ C & ^{↓ ∩} & \overline{→} & Q & ^{↓ ∨} \end{aligned}

for some stable open V of C and a (necessarily unique) map V → O in .

The stable open 𝕆_{1} ↪ 𝕆_{2} not only determines the locally stable opens, but also classifies them. Indeed, every locally stable open O ↪ Q in appears in a pullback (1) for a unique characteristic map Q → 𝕆_{2}. Moreover, as the initial object in is strict, the category is a topos and in it the Sierpinski space 𝕆_{2} is a dominance (see [34] for a general treatment). It follows that the topos of cuboidal sets admits a lifting monad 𝕃 which we now make explicit.

To understand the following definitions think that a path C → LP of shape C in LP is described by a pair consisting of its degree of definedness represented by a stable open V of the cuboid C and a total path V → P of shape V in P.

• The underlying functor L is given by (LP)(C) =^{def} {(V, x) | V ∈ O_{∧}(C), x : V → P } with action on morphisms (LP)(C′ → C) sending (V, V → P), with V a stable open of C, to (V′, V′ → V → P) where the square

\begin{aligned}V′ & \overline{→} & V \\ C′ & ^{↓ ∩} & \overline{→} & C & ^{↓ ∩} \end{aligned}

is a pullback.

• The unit η_{P} : P → LP sends a path C → P to (C, C → P).

• The multiplication μ_{P} : L^{2}P → LP sends (V, (V′, V′ → P)), with V a stable open of C and V′ a stable open of V, to (V′, V′ → P).

• The tensorial strength t_{Q,P} : Q × LP → L(Q × P) sends ⟨C → Q, (V, V → P)⟩, with V a stable open of C, to (V, ⟨V ↪ C → Q, V → P ⟩).

Theorem 3.1 ([14]) The lifting functor on the category of cuboidal sets preserves non-empty connected colimits.

The category of cuboidal sets is locally presentable (as it is a sheaf topos) and, by the above theorem, the lifting monad is accessible. It also follows from the above theorem, e.g. using the basic lemma [39], that the lifting functor has an inductive initial algebra. Since connected colimits in the category of cuboidal sets are given pointwise, the inductive initial L-algebra ω = colim ⟨𝕆_{n} ^{>}^{l_{n}}→ 𝕆_{n+1}⟩_{n}, where l_{n} denotes the inclusion of 𝕆_{n} into 𝕆_{n+1}, has as its set ω(C) of paths of shape C the set of sequences of the form

C ↩ V_{0} ↩ … ↩ V_{n} ↩ ∅ ↩ … ↩ ∅ ↩ …

with each V_{i} a stable open of the cuboid C.

Corollary 3.2 1. The adjunction \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} ^{𝕃} is a model of linear type theory.

2. The lifting monad 𝕃 on is pre-domain-theoretic.

Complete cuboidal sets. A cuboidal set is given a notion of passage to the limit by equipping it with a formal-lub operator. This results in the category ⋁( ) of formally ω-complete cuboidal sets (henceforth simply called complete cuboidal sets).

In this subsection, we study the domain-theoretic structure of ⋁( ). We start by observing that ⋁( ) embeds the categories Cpo and ⋁(Poset_{∧}); hence also Cpo_{∧}. Let C be either Poset or Poset_{∧}. For every object D in C, there is a canonical isomorphism (ND)^{ω} . ; ≅ N(D^{𝕆_{ℵ_{0}}} ) in (c.f. (4) below), where N is the nerve functor C → defined in the previous subsection. Then, the functor ⋁(N) : ⋁(C) → ⋁( ) associating to an object (D, ⋁) in ⋁(C) the complete

cuboidal set (N(D), (ND)^{ω} ≅ N(D^{𝕆_{ℵ_{0}}} ) ^{N(⋁)} → ND) is full and faithful.

Theorem 3.3 1. The category ⋁( ) is locally presentable and cartesian closed.

2. The lifting monad 𝕃 on extends to an accessible commutative monad 𝕃̌ on ⋁( ).

The above result follows from a general theory alluded to in Section 2, § The ideal-completion monad. Here we only give an idea of the proof.

One shows that admits an accessible idealcompletion monad 𝕀; hence ⋁( ) ≃ ^{𝕀} is locally presentable (see Appendix B). The cartesian closure of ⋁( ) follows from Proposition 2.4.

In fact, one can construct the ideal-completion monad 𝕀 as a quotient of the exponentiation monad 𝕎, and show that the distributive law 𝕃 𝕎 \underrightarrow{.} 𝕎 𝕃 collapses to an isomorphism 𝕃 𝕀 . ; ≅ 𝕀𝕃 yielding another distributive law. Then, the functor L on extends to ^{𝕀}; if ⋁_{P} : I(P) → P is an 𝕀-algebra then so is the

composite ILP ≅ LIP ^{L(⋁_{P})} → LP. We conjecture that the commutative monad 𝕃̌ on ⋁( ) is a lifting monad.

For illustrative purposes, for a complete cuboidal set ⋁_{P} : P^{ω} → P, we give an explicit description of the formal-lub operator ⋁_{LP} : (LP)^{ω} → LP in two steps. First, to every generalised chain C → (LP)^{ω} of shape C in LP we associate a path C → L(P^{ω}) again of shape C in L(P^{ω}) by (intuitively) removing bottom elements from the chain whenever possible. Second, we define the action of the formal-lub operator ⋁_{LP} on generalised chains C → (LP)^{ω} as the composite

C → L(P^{ω}) ^{L(⋁_{P})} → LP. We describe the passage from C → (LP)^{ω} to C → L(P^{ω}). We have the following bijective correspondence:

C → (LP)^{ω}
C × ω → LP
C × 𝕆_{n} ← ^{⊃} U_{n}  \overline{→} P
[figure: (n ≥ 0)]
C × 𝕆_{n+1}^{id_{C} × l_{n}↓ ∨}  ←^{⊃} U_{n+1}^{↓ ∨}

with the crucial property that there exists a least j such that, for all n < j, U_{n} = ∅ and, for all n, U_{j+n} ≅ V × 𝕆_{1+n} for a unique V ∈ O_{∧}(C). Then we define C → L(P^{ω}) as the characteristic map of the partial map C ↩ V → P^{ω} where V → P^{ω} is the exponential transpose of the unique mediating map V ×ω → P from the colimiting cone ⟨V × 𝕆_{n+1} → V × ω⟩_{n} to the cone ⟨V × 𝕆_{n+1} ≅ U_{j+n} → P ⟩_{n}.

Theorem 3.4 The commutative monad 𝕃̌ on ⋁( ) is domain-theoretic.

Notice that since I𝕆_{0} ≅ 𝕆_{0} and ILP ≅ LIP, for finite n, we have that 𝕆_{n} is isomorphic to its formal ideal completion I𝕆_{n}. On the other hand, the formal ideal completion \overline{ω} =^{def} I(ω) of ω with structure map σ =^{def} (L(Iω) ≅ I(Lω) Iς ; ≅→ Iω) and global element

∞ =^{def} (1 ^{⌜ι_{ω}⌝} → (Iω)^{ω} ⋁→ Iω), where we write ι for the unit of 𝕀, provides an inductive Ľ-fixed-point object. We give an explict description of \overline{ω} and ∞. We will present \overline{ω} as a quotient of ω^{ω}. The following bijective correspondences describe the paths of ω^{ω}:

C → ω^{ω} C × ω → ω

C × 𝕆_{n}  \overline{→} ω
[figure: (n ≥ 0)]
C × 𝕆_{n+1}^{id_{c} × l_{n}↓ ∨}
V_{n,j+1} ^{⊂} → V_{n,j} ^{⊂} → C × 𝕆_{n}

V_{n+1,j+1}^{↓ ∨}  ^{⊂} → V_{n+1,j}^{↓ ∨}  ^{⊂} → C × 𝕆_{n+1} \begin{matrix}↓ & ∨ \\ id_{C} × l_{n} \end{matrix}

(n, j ≥ 0)

C × 𝕆_{ℵ_{0}} ↩ V_{0} ↩ … ↩ V_{n} ↩ …

v_{0} ≤ … ≤ v_{n} ≤ … in C × 𝕆_{ℵ_{0}}

Then the quotient of ω^{ω} yielding \overline{ω} is done by idealcompleting locally: for every cuboid C, the set \overline{ω}(C), of paths of shape C in \overline{ω}, may be identified with C × 𝕆_{ℵ_{0}+1}. And ∞_{C} ∈ C × 𝕆_{ℵ_{0}+1} is the pair consisting of the least element of C and the greatest element of 𝕆_{ℵ_{0}+1}.

As \overline{ω} admits an 𝕃̌-algebra structure (viz. the com-

posite Ľ\overline{ω} ^{Lσ^{−1}}→ Ľ^{2}\overline{ω} ^{μ\overline{ω}}→ Ľ\overline{ω} ^{σ} → \overline{ω}), by the formal fixed-point property (Proposition 2.2 (1)), endomorphisms on it have fixed-points. It follows that fix(succ) = ∞.

Corollary 3.5 The adjunction ⋁( ) \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} ⋁( )𝕃̌ is a domain-theoretic enrichment base with respect to which

the category of Eilenberg-Moore algebras ⋁( )𝕃̌ is a domain-theoretic model of recursive types.

4 An enrichment theorem for domaintheoretic lifting monads

We show that every domain-theoretic lifting monad enriches over the category of complete cuboidal sets.

More precisely, say that a V-category K provides an enrichment of the ordinary category C if the underlying ordinary category K_{0} (with hom-sets K_{0}(A, B) =^{def} V(I, K(A, B))) and C are isomorphic. Then, for a domain-theoretic lifting monad on C we will construct a ⋁( )-category providing an enrichment of the ordinary category C in such a way that the domain-theoretic structure also enriches. It will follow as a corollary that every domain-theoretic model of recursive types in a wide class also enriches over ⋁( ).

For a symmetric monoidal category W, write γ_{W} (omitting the subscript if it is clear from the context) for the global-sections functor W(I, ) : W → Set. For a symmetric monoidal functor H : V → V′ such that (V ^{H}→ V′ ^{γ_{V′}}→ Set) . ; ≅ (V ^{γ_{V}}→ Set), the V′-category H_{∗}K (defined in Section 1, § Models of linear type theory) provides an enrichment of K_{0}.

Thus, for a domain-theoretic lifting monad on C we aim at producing a cartesian functor C → ⋁( ) such that (C → ⋁( ) ^{γ}→ Set) . ; ≅ (C ^{γ}→ Set). Then, since C enriches over itself (as it is cartesian closed) the above process will provide the aforementioned enrichment result.

We start our considerations with respect to the predomain-theoretic case.

Enrichment for pre-domain-theoretic lifting monads. Let 𝕃 = (L, η, μ) be a pre-domain-theoretic lifting monad on C.

We define a functor S : → C. For n ≥ 0, we write Σ_{n} for L^{n}0 and define the action of S on objects by the mapping sending 𝕆_{n_{1}} × … × 𝕆_{n_{i}} to Σ_{n_{1}} × … × Σ_{n_{i}}. To define the action of S on morphisms we proceed in two steps. First, for n ≥ 0, we define S_{n} : (C, 𝕆_{n}) → C(S(C), Σ_{n}). Second, we let S : (C, 𝕆_{n_{1}} × … × 𝕆_{n_{i}}) → C(S(C), Σ_{n_{1}} × … × Σ_{n_{i}}) be the mapping f ↦ ⟨S_{n_{1}}(f_{1}), …, S_{n_{i}}(f_{i})⟩ where

f_{j} =^{def} (C ^{f} → 𝕆_{n_{1}} × … × 𝕆_{n_{i}} ^{π_{j}}→ 𝕆_{n_{j}}). We

give an inductive definition of S_{n}. For n = 0, the action S_{0} : (C, 𝕆_{0}) → C(S(C), 0) is uniquely determined by its target. For n = m + 1 with m ≥ 0, let C = 𝕆_{n_{1}} × … × 𝕆_{n_{i}} and consider f : C → 𝕆_{m+1} for which the following diagram

\begin{matrix}𝕆_{n′_{1}} × … × 𝕆_{n′_{i}} & \overline{\underrightarrow{f′}} & 𝕆_{m} \\ 𝕆_{n_{1}} × … × 𝕆_{n_{i}} & ^{↓ ∩} & f→ & 𝕆_{m+1} & ^{↓ ∩} \end{matrix}

is a pullback in . Then, we let S_{m+1}(f) be the unique characteristic map making the diagram

\begin{matrix}Σ_{n′_{1}} × … × Σ_{n′_{i}} & \overline{S_{m}(f′)→} & Σ_{m} \\ Σ_{n_{1}} × … × Σ_{n_{i}} & ^{u_{1} × … × u_{i}↓ ∩} & \overline{_{S_{m+1}(f) →}} & Σ_{m+1} & \begin{matrix}↓ & ∩ \\ η_{Σ_{m}} \end{matrix} & , \end{matrix}

where u_{j} =^{def} (Σ_{n′_{j}} ^{⊂} ^{η}→ ⋯ ^{⊂} ^{η}→ Σ_{n_{j}}), a pullback in C. By construction, S is indeed a functor; moreover, it preserves the initial object, finite products, and pullbacks of stable opens along arbitrary maps.

We remark on a more conceptual definition of the functor S. The category F is the free cartesian category with an initial object and a lifting monad 𝕃 such that L0 ≅ 1; and, the functor S : → C is the composite

↪ F → C where F → C is the unique structure preserving functor given by freeness.

Define the nerve functor N : C → with action given by the mapping f ↦ C(S , f). Thus for a cuboid C in and an object D in C, we have the following bijective correspondence

\begin{matrix}C → N(D) \\ S(C) → D \end{matrix}

stating that the paths of shape C in the cuboidal set N(D) are the paths of shape S(C) in the object D. For instance, the C-parameterised paths C × 𝕆_{n} → N(D) in are in bijective correspondance with the S(C)-parameterised paths S(C) × Σ_{n} → D in C. It follows that,

γ_{□} ∘ N . ; ≅ γ_{C}  (2)
(ND)^{𝕆_{n}}  ≅ N(D^{Σ_{n}})  (3)

The nerve functor has the crucial property of preserving limits. We thus have the following two consequences.

1. Applying the N_{∗} functor to C regarded as a C-category we obtain the -category N_{∗}C which, by (2), provides an enrichment of C.

2. The isomorphism (3) extends to the limit; that is,

(ND)^{ω} ≅ N(D^{ω_{C}})  (4)

as (ND)^{ω} ≅ (ND)^{colim 𝕆_{n}} ≅ lim (ND)^{𝕆_{n}} ≅ lim N(D^{Σ_{n}}) ≅ N(lim D^{Σ_{n}}) ≅ N(D^{colim Σ_{n}}) ≅ N(D^{ω_{C}}).

In fact, from (4) we obtain a natural isomorphism ν : (N )^{ω} . ; ≅ N( ^{ω_{C}}) making the pair (N, ν) into a morphism 𝕎_{C} → 𝕎 of monads (see [40] for this notion). We thus get a functor C^{𝕎_{C}} → ^{𝕎}

sending a 𝕎_{C}-algebra D^{ω_{C}} ⋁→ D to the 𝕎-algebra

(ND)^{ω} ν ; ≅→ N(D^{ω_{C}}) ^{N(⋁)} → ND. Moreover, the diagram

(N )^{ω} \overline{\underrightarrow{ν ; ≅}} N( ^{ω_{C}})

(N )^{ω}^{(N )^{succ}↓}  \overline{\underrightarrow{ν ; ≅}} N( ^{ω_{C}})^{↓N( ^{succ^{C}})}

commutes, and so the functor C^{𝕎_{C}} → ^{𝕎} cuts down to a functor ⋁(C) → ⋁( ).

Enrichment for domain-theoretic lifting monads. Applying the above discussion to a domaintheoretic lifting monad 𝕃 on C, we get a limit preserving functor ⋁(N) : C ≅ ⋁(C) → ⋁( ), sending an object D to the complete cuboidal set

(N(D), (ND)^{ω} ν ; ≅→ N(D\overline{ω}) ^{N(D^{∞})} → ND), such that

(C ^{⋁(N)} → ⋁( ) ^{γ}→ Set) . ; ≅ (C ^{γ}→ Set).

We have thus obtained the first part of the following result.

Theorem 4.1 (Enrichment theorem) Let 𝕃 be a domain-theoretic lifting monad on C.

1. The ⋁( )-category ⋁(N)_{∗}C provides an enrichment of C.

2. In ⋁(N)_{∗}C, the cartesian closed structure of C, the commutative monad 𝕃 on C, and the colimit defining \overline{ω} also enrich over ⋁( ).

Enrichment for domain-theoretic models of recursive types. Every domain-theoretic model of recursive types with respect to a domain-theoretic enrichment base inducing a lifting monad enriches over the category of complete cuboidal sets.

Corollary 4.2 Let M be a domain-theoretic model of recursive types with respect to a domain-theoretic enrichment base F : C \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} D : U inducing a lifting monad.

The ⋁( )-category ⋁(N)_{∗}U_{∗}M provides an enrichment of M_{0}.

We conjecture that (possibly under some mild assumptions) domain-theoretic models of recursive types

enrich over ⋁( )𝕃̌.

5 Concluding remarks

We have introduced a new notion of domain, viz. that of complete cuboidal set, that complies with the requirements of ADT. To this end, we have provided an algebraic notion of passage to the limit with respect to which a definition of ideal completion was given. Further, we have shown that the category of complete cuboidal sets provides a general notion of enrichment, traditionally attributed to the category of cpos, for a wide class of domain-theoretic structures (viz. domain-theoretic lifting monads and certain domain-theoretic models of recursive types).

Many further directions of research are possible; we mention a few here.

There are two orthogonal directions for extending the enrichment theorem: by incorporating binary sums into the domain-theoretic lifting monads, or by considering arbitrary commutative monads (rather than lifting ones).

As in [10], the enrichment theorem seems likely to provide the basis for developing a representation theory. This possibility is under investigation.

Connections with synthetic domain theory are envisaged. In particular, a synthetic characterisation of the category of complete cuboidal sets seems to be available. This might help in settling our first conjecture (see Section 3, § Complete cuboidal sets), which is important for our representation programme.

At a more speculative level, we wonder what the relationship is between this work and presheaf or higherdimensional models of concurrency [23, 42, 6, 41, 19, 18, 5, 20].

References

[1] J. Adámek and J. Rosický. Locally Presentable and Accessible Categories. Cambridge University Press, 1994.

[2] M. Barr and C. Wells. Toposes, Triples and Theories. Springer-Verlag, 1985.

[3] N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In CSL’94 Conf., volume 933 of Lecture Notes in Computer Science, 1995.

[4] F. Borceux. Handbook of Categorical Algebra. Cambridge University Press, 1994.

[5] G.L. Cattani and V. Sassone. Higher dimensional transition systems. In 11^{th} LICS Conf., pages 55– 62. IEEE, Computer Society Press, 1996.

[6] G.L. Cattani and G. Winskel. Presheaf models for concurrency. Presented at CSL’96 Conf., 1996.

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

[8] M.P. Fiore. Lifting as a KZ-doctrine. In D. Pitt, D. Rydeheard, and P. Johnstone, editors, CTCS’95 Conf., volume 953 of Lecture Notes in Computer Science, pages 146–158. Springer-Verlag, 1995.

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

[10] M.P. Fiore. Enrichment and representation theorems for categories of domains and continuous functions. Manuscript (available from http://www.dcs.ed.ac.uk/home/mf/), 1996.

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

[12] M.P. Fiore, A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini, and I. Stark. Domains and denotational semantics: History, accomplishments and open problems. In number 59 of Bulletin of the European Association for Theoretical Computer Science, pages 227–256, 1996.

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

[14] M.P. Fiore and G.D. Plotkin. An extension of models of axiomatic domain theory to models of synthetic domain theory. Presented at CSL’96 Conf., 1996.

[15] P. Freyd. Abelian Categories: An Introduction to the Theory of Functors. Harper & Row, 1964.

[16] P.J. Freyd. Recursive types reduced to inductive types. In 5^{th} LICS Conf., pages 498–507. IEEE, Computer Society Press, 1990.

[17] P.J. Freyd. Algebraically complete categories. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory, volume 1488 of Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

[18] E. Goubault. Domains of higher dimensional automata. In CONCUR’93 Conf., volume 715 of Lecture Notes in Computer Science, pages 293–307, 1993.

[19] E. Goubault and T.P. Jensen. Homology of higher dimensional automata. In CONCUR’92 Conf., volume 630 of Lecture Notes in Computer Science, pages 254–268, 1992.

[20] M. Herlihy and S. Rajsbaum. Algebraic topology and distributed computing: A primer. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 203–217, 1995.

[21] B. Jacobs. Semantics of weakening and contraction. Annals of Pure and Applied Logic, 69:73–106, 1994.

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

[23] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127(2):164–185, 1996.

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

[25] A. Kock. Bilinearity and cartesian closed monads. Math. Scand., 29:161–174, 1971.

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

[27] F.W. Lawvere. Qualitative distinctions between some toposes of generalized graphs. Contemporary Mathematics, 92:261–299, 1989.

[28] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[29] E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991.

[30] M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures and domains I. Theoretical Computer Science, 13(1):85–108, 1981.

[31] G.D. Plotkin. Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School, 1985.

[32] G.D. Plotkin. Algebraic completeness and compactness in an enriched setting. Invited lecture given at the Workshop on Logic, Domains, and Programming Languages. Darmstadt, 1995.

[33] E. Robinson and G. Rosolini. Categories of partial maps. Information and Computation, 79:95–130, 1988.

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

[35] D.S. Scott. A type-theoretical alternative to CUCH, ISWIM, OWHY. Manuscript (available as [37]), 1969.

[36] D.S. Scott. Continuous lattices. In F.W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97–136. Springer-Verlag, 1972.

[37] D.S. Scott. A type-theoretical alternative to CUCH, ISWIM, OWHY. Theoretical Computer Science, 121:411–440, 1993. (Reprint of a manuscript).

[38] A.K. Simpson. Recursive types in Kleisli categories. Manuscript (available from http://www.dcs.ed.ac.uk/home/als/), 1992.

[39] M.B. Smyth and G.D. Plotkin. The categorytheoretic solution of recursive domain equations. SIAM Journal of Computing, 11(4):761–783, 1982.

[40] R. Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2:149–168, 1972.

[41] R. van Glabbeek. Bisimulations for higher dimensional automata. Communication to the concurrency mailing list (available from http://theory.stanford.edu/people/rvg/hda), 1991.

[42] G. Winskel. Presheaf semantics for value passing. In CONCUR’96, volume 1119 of Lecture Notes in Computer Science, pages 98–114, 1996.

A Lifting monads

A monad 𝕃 = (L, η, μ) on a category with terminal object is said to be a lifting monad if

• pullbacks of η_{1} along arbitrary maps exist;

• the unit η is cartesian (i.e. the squares required to commute by naturality are pullbacks) and a partial map classifier (i.e. in the situation

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

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

\begin{aligned}D & \overline{→} & B \\ A & ^{↓ ∩} & \overline{→} & LB & \begin{matrix}↓ & ∩ \\ η_{B} \end{matrix} \end{aligned}

is a pullback).

Examples of lifting monads are the identity monad; the ( )+1 monad on Set; the traditional lifting monad ( )_{⊥} on Preo, Poset, Poset_{∧}, Cpo, and Cpo_{∧}; and the partial map classifier monad [22] on a topos.

Recall that lifting monads on cartesian categories are commutative (see e.g. [9]).

B Locally presentable categories

We recall some basic definitions and facts of the theory of locally presentable categories used throughout the paper. For a thorough treatment consult [1, 4].

Let λ be a regular cardinal (i.e. an infinite cardinal which is not a sum of a smaller number of smaller cardinals). An object C of a category C is λ-presentable when its covariant hom-functor C(C, ) preserves λ-directed colimits. A category C is said to be locally λ-presentable if it is cocomplete, and has a small set P_{λ}C of λ-presentable objects such that every object in the category is a λ-directed colimit of objects from P_{λ}C. A functor between locally λ-presentable categories is called λ-accessible if it preserves λ-directed colimits.

A category is said to be locally presentable if it is locally λ-presentable for some regular cardinal λ. Every locally presentable category is complete.

A monad is called accessible if its underlying functor is λ-accessible for some regular cardinal λ. The category of Eilenberg-Moore algebras for an accessible monad on a locally presentable category is locally presentable.