Theory and Applications of Categories, Vol. 10, No. 13, 2002, pp. 301–368.

SUBSPACES IN ABSTRACT STONE DUALITY

PAUL TAYLOR

ABSTRACT. By abstract Stone duality we mean that the topology or contravariant powerset functor, seen as a self-adjoint exponential Σ^{(−)} on some category, is monadic. Using Beck’s theorem, this means that certain equalisers exist and carry the subspace topology. These subspaces are encoded by idempotents that play a role similar to that of nuclei in locale theory.

Paré showed that any elementary topos has this duality, and we prove it intuitionistically for the category of locally compact locales.

The paper is largely concerned with the construction of such a category out of one that merely has powers of some fixed object Σ. It builds on Sober Spaces and Continuations, where the related but weaker notion of abstract sobriety was considered. The construction is done first by formally adjoining certain equalisers that Σ^{(−)} takes to coequalisers, then using Eilenberg–Moore algebras, and finally presented as a lambda calculus similar to the axiom of comprehension in set theory.

The comprehension calculus has a normalisation theorem, by which every type can be embedded as a subspace of a type formed without comprehension, and terms also normalise in a simple way. The symbolic and categorical structures are thereby shown to be equivalent.

Finally, sums and certain quotients are constructed using the comprehension calculus, giving an extensive category.

Contents  6 Structure in \overline{C}  330
1 Introduction  301  7 Algebras  336
2 The subspace topology  307  8 Comprehension  341
3 Beck’s theorem  312  9 Normalisation for types 346
4 Adding Σ-split subspaces  320  10 Normalisation for terms 351
5 Injectives and products in \overline{C} 324  11 Sums and quotients  359

1. Introduction

The existence or otherwise of extensional subspaces is a point of demarcation between pure mathematics and computer science. The ubiquitous axiom of comprehension seems to be what mainstream mathematicians have in mind when they insist that Set Theory provides

Received by the editors 2002 January 21 and, in revised form, 2002 July 3. Transmitted by Andrew Pitts. Published on 2002 July 22. 2000 Mathematics Subject Classification: 03E70, 03G30, 06D22, 06E15, 18B05, 18B30, 18C20,

18E10, 54C35, 54D45.

Key words and phrases: axiom of comprehension; subtype; typed lambda calculus; Stone duality; subspace topology; locally compact spaces; nucleus of a locale; injective object; monadic adjunction; Beck’s theorem.

\begin{matrix}c \\ ◯ \end{matrix} Paul Taylor, 2002. Permission to copy for private use granted.

the foundations of their subject. On the other hand, neither programming languages nor the type theories that are most popular in computer science admit subtypes. (We do not mean the notion of this name in object-oriented programming, which is like an extension of the signature of an algebraic theory.) Subtypes in our sense are used in software development, in the form of Floyd–Hoare logic, with pre- and post-conditions, but it is an up-hill struggle to teach programmers to use them!

The reason for this demarcation is that the essence of the development in a mathematical argument is quite different from that in a computation. Before the referee will allow me to say that an element belongs to a subset, I must prove that it satisfies the defining property. Otherwise, the rest of the argument has no meaning whatever, and my paper is not published. From this point of view, compilation of high level programming languages lies on the mathematical side of the boundary. A (low level) computation, on the other hand, proceeds irrespectively of whether or not a purported mid-condition is satisfied: if it doesn’t, the behaviour of the program may not be what the programmer had in mind, but it nevertheless does something.

I am, of course, in favour of constructive mathematics, and appreciate the analogy between programs and proofs, but opinions differ as to what is regarded as constructive: my notion is stronger than Johnstone’s [Joh82] but weaker than Martin-Löf’s [ML84]. I have argued that what Per Martin-Löf calls the “existential quantifier” and the “axiom of choice” are not those used in geometry [Tay99, Section 2.4], and nor do I consider that an element of a subset needs to be accompanied by a proof of the defining predicate. Such proofs may serve as guarantees, but at some point we must eventually trust (the verification of) the guarantee and carry on with the computation.

In crossing the demarcation from pure mathematics to programming, we therefore have to extend the definition of functions that were intended to be defined on a subset to the whole of the ambient set, possibly at the cost of results that lie outside the intended target. A target object that permits such extension without itself being expanded is called injective, and such objects will play an important role in this paper.

I see the crossing as building a “mathematically comfortable” platform, with more types (sets, spaces) than the underlying programming language, but such that the terms (elements) become programs when the richer type information is erased. The programming language that we shall use was justified and developed in the previous paper [A], so now we must consider ways of building mathematical platforms. Category theory provides the language in which to express both our requirements for “comfort” and the means of satisfying them, although equivalent λ-calculi are needed for the idioms of both mathematics and programming.

Programming languages include constructors for making new types from old ones, but the additional mathematical types depend on terms. A very general theory of such dependent types is formulated in [Tay99, Chapter VIII], although I now consider that to be too complicated. Simpler notions than the axiom of comprehension are familiar in category theory: equalisers, pullbacks, coequalisers and pushouts.

The present work is by no means the first to provide such extensions. One very simple idea is to split idempotents (Remark 4.1), which Dana Scott developed [Sco76]. However, a great deal of artificiality was piled on top of this, notably sum types with spurious additional elements: we shall find in Section 11 that stable disjoint coproducts are a mathematical comfort that we may reasonably demand as standard.

Another idea is to expand the monoid of (partial general) recursive functions on ℕ to the category whose objects are recursively enumerable subsets. Giuseppe Rosolini formulated the abstract notion of partial maps (composing a p-category), and constructed a category with subobjects from it [RR88]. Peter Freyd and Andre Scedrov started instead from binary relations (composing an allegory) [FS90]. Their theory also accounts for the way in which general sets may be obtained from iterated powersets, traditionally known as the von Neumann hierarchy. Bill Lawvere’s treatment [Law70] describes and generalises the behaviour of comprehension in toposes and other categories in which it already exists, but does not explain how it creates new sets [Tay99, Exercises 9.45ff]. Other ways of expanding the class of types include the regular and exact completions of categories.

The particular construction performed in this paper is based on a monad. In the original mathematical development of monads, Eilenberg–Moore algebras were given a preferential role [Eck69, BW85]. Later, Eugenio Moggi demonstrated how they could be used to encode features of computation [Mog91], but the new types that he introduced were objects of the Kleisli category, which consists of just the free algebras. So the literature that has ensued illustrates the demarcation between mathematics and computer science. In particular, the basic form of our construction without the subspaces (Section^{1} A 6) is similar to work of Hayo Thielecke [Thi97], which uses the the Kleisli category.

In none of these constructions is a type defined as a “collection”, as Solomon Feferman claimed to be a necessary ingredient of mathematical foundations [Fef77], and nor is a subtype a sub-collection selected by some kind of demon. Both the underlying programming language and its mathematical enrichment may be defined as λ-calculi with certain syntactic rules of formation. Of course, there is a (recursive) collection of well formed formulae (or of objects and morphisms in the category), but this cannot be what Feferman’s argument means, as it applies equally to Set Theory itself. The metalanguage of category theory and type theory is not only first order, as is that of Set Theory, but essentially algebraic. In our case, the universal properties of Σ-split (co)equalisers are equational, so the quantifier complexity is even less.

Many of the mathematical intuitions on which our calculus is based come from general topology, regarded as a more subtle form of set theory. This research programme is named after Marshall Stone because he was the first to emphasise that one should always look for the topology on any mathematical object that one has constructed, since the appropriate morphisms are continuous functions, not arbitrary set-theoretic ones à la Cantor. (See the Introduction to [Joh82] for a historical survey of this point of view.)

Contrary to what Richard Dedekind and Georg Cantor have told us, this is how the real line ℝ is defined: we understand the topology Σ^{ℝ} because this is the abstraction of the convergence of sequences of rationals (or of otherwise algebraically definable numbers), and this is the only way by which we gain access to transcendental numbers. The space ℝ exists by fiat, being defined formally as pts(Σ^{ℝ}). Indeed, Bourbaki also constructed ℝ at the end of a tortuous chain of definitions that spans an entire volume [Bou66], but essentially recovers it from a topology that is defined in terms of ℚ.

1My papers Sober Spaces and Continuations and Geometric and Higher Order Logic are cited as if they were respectively “Chapters” A and C of a book, this paper being Chapter B.

It was Dana Scott who promoted the analogy between continuity and computability. However, there cannot be a precise connection with the traditional axiomatisation of general topology, because it relies on arbitrary unions, rather than recursive ones. It is principally this problem that Abstract Stone Duality seeks to address.

Monads provide a way of handling infinitary algebra of the kind that we need to reaxiomatise topology, and may be defined over any category, not just the category of sets. Specifically, we define the algebras that replace the lattices of open subsets of a space using a monad over the category of spaces itself.

This use of monads was also inspired by Marshall Stone’s work. By Stone duality we understand the dual equivalence between a category of algebraically defined objects and another whose objects we think of as “spaces”, though they may be sets, posets or algebraic varieties as well as topological spaces.

By abstract Stone duality we mean some category C of “spaces” whose opposite category C^{op} ≃ A is itself “algebraic” over C in the sense of being the category of Eilenberg– Moore algebras over C.

The analogy between the two concrete examples of sets and locally compact spaces drives the intuition behind this programme. Temporarily using classical logic, including the axiom of choice, to present this intuition, these two monadic situations are illustrated by the following diagrams.

[figure: Set^{op}; powerset; ≃; \underline{atoms}; CABA; LKSp^{op}; topology; ≃; \underline{pts}; LKFrm]

Set \begin{aligned}Ω^{(−)} &  \\ & ⊣ Ω^{(−)}_{} \end{aligned}= = = = = = = = = = = = = = = = Set . . . . . . . . . . . . . . . . . ; ⊣ U_{}LKSp \begin{aligned}Σ^{(−)} &  \\ & ⊣ Σ^{(−)}_{} \end{aligned}= = = = = = = = = = = = = LKSp . . . . . . . . . . . . . . . . . ; ⊣ U_{}

Adolf Lindenbaum and Alfred Tarski characterised full powerset lattices classically as complete atomic Boolean algebras [Tar35]. In modern terms, we formulate their result as a mutually inverse pair of functors, one of which takes a set X to its powerset PX, and the other extracts the set of “atomic” elements of any complete atomic Boolean algebra.

The morphisms of CABA preserve arbitrary meets and joins, and the forgetful functor U : CABA → Set from this category has a left adjoint. The free complete atomic Boolean algebra on a set X is its double powerset, PPX, and it may be shown that this adjunction is monadic.

The equivalence of categories re-states this concrete adjunction in more abstract terms: the contravariant powerset functor P : Set^{op} → Set is self -adjoint, and (since the squares commute) the Lindenbaum–Tarski theorem says that this adjunction is also monadic. Robert Paré proved the same result intuitionistically for any elementary topos [Par74]. Classically, PX ≅ 2^{X}, whilst PX ≅ Ω^{X} in a topos, where Ω denotes the type of truth values.

In the second diagram, Frm is the category of frames, i.e. lattices with arbitrary joins over which binary meets distribute, and homomorphisms that preserve finite meets and arbitrary joins. Frames are therefore the kind of lattices that open subsets constitute in general topology, whilst the homomorphisms capture the properties of inverse image maps for continuous functions. LKSp and LKFrm are the categories of locally compact sober spaces and the frames that arise as their topologies, namely those that are also continuous lattices [HM81].

LKSp and LKFrm are dual categories, where the “points” of a frame may be characterised lattice-theoretically [Joh82, Section II 1] or by means of an exponential Σ^{(−)} and its associated λ-calculus [A]. Frm is also a category of Eilenberg–Moore algebras for a monad over Set. However, if U forgets just the finitary lattice structure, but leaves the carrier equipped with its directed joins and so the Scott topology, LKFrm is monadic over LKSp.

Again, the monadic adjunction may be seen abstractly, where the powerset PX ≅ Ω^{X} is replaced by the topology, i.e. the lattice of open subsets of X, and the lattice itself is regarded as a space with the Scott topology. The topology may be expressed as Σ^{X}, where Σ is the Sierpiński space. Classically Σ also has two points, one of which is open.

The theorems of Stone, Tarski and Lindenbaum that we have given identified “atoms” or “points” in the lattices as sets of sets. This turns the set-theoretic membership relation on its head: each “open set” (element of the algebra) belongs to certain “points”, i.e. these correspond to certain subsets of the algebra. However, the existence of enough ideal points to separate the elements of the algebra is equivalent to the axiom of choice, or at least to some weaker proper axiom such as the prime ideal theorem. Just the same problem arises in model theory, models being the “ideal points” of the predicate calculus.

In the following two sections we show how, when the category of “spaces” satisfies the abstract Stone duality, it admits subspaces that carry the subspace topology. This is a special case of Jon Beck’s general characterisation of monadic adjunctions: under the duality, subspaces correspond to quotient algebras, and Beck’s theorem says that we may calculate certain kinds of quotient algebras simply as quotients of their carriers. For textbook accounts of monads and Beck’s theorem, see [ML71, Section VI 7], [BW85, Section 3.3] or [Tay99, Section 7.5]. Our discussion in Section 3 is partly intended to amplify these accounts by giving a worked example of Beck’s theorem, in the hope that it will cross the demarcation and become better understood in the theoretical computer science community.

Theorem 3.11 gives an intuitionistic proof of Stone duality for locally compact locales. After this, there is no more topology in this paper: that story — in particular, the equivalence between Eilenberg–Moore and frame homomorphisms — is taken up in [C, D, F].

Sections 4–6 build a new category \overline{C} with the abstract Stone duality from one that simply has products, powers of Σ and all objects sober. The construction is based directly on Beck’s theorem, formally adding Σ-split equalisers. The main difficulty is in showing that \overline{C} has products, for which injective objects are needed as a tool.

Section 7 briefly describes an alternative construction that uses algebras instead. Sections 8–10 investigate an equivalent λ-calculus, whose types admit subspaces that

are described using something like the axiom of comprehension in set theory. However, these type annotations, like the mid-conditions in Floyd–Hoare logic, are computationally anodyne: they remain in the journal papers and are not used at run-time. The terms may be stripped of this complex type information, leaving a simple λ-calculus with application and abstraction.

The final section constructs stable disjoint coproducts and Σ-split coequalisers.

Some comment is in order on the fact that locally compact locales, rather than all locales, provide the leading model of our axioms. Fundamentally, it is the category that we seek to axiomatise, not the spaces, and one category has the monadic property, whilst the other doesn’t. Indeed, the axioms for locales hardly enjoy the same unanimous acceptance in the mathematical community as do those for, say, groups. Spatial locales agree with sober spaces, but even then disagree as to their products outside the locally compact case, whilst there are numerous competing axiomatisations of convergence and other features of topology. The traditional one has also long been regarded as unsatisfactory on the grounds that its logical properties (such as cartesian closure) are inadequate. This paper breaks new ground in treating topology as λ-calculus.

The simple technical reason for the “restriction” is that the exponential Σ^{X} is only defined when X is locally compact. However, Steven Vickers has shown how the functor Σ^{Σ^{(−)}} may be extended to all locales, decomposing it into two covariant functors that are of interest in themselves [Vic02]. However, the Eilenberg–Moore category for his monad is not the category of frames, but one whose opposite he calls the category of colocales. When X is a locale, Σ^{X} is a colocale, and vice versa, so observations belong not merely to a different type from values, but to another category, whilst meta-observations are again like values. Our experience since Turing that computations are ultimately untyped seems to have been sacrificed on the altar of conformity with a pre-existing mathematical structure.

I acknowledge, on the other hand, that my mathematical platform is not as comfortable as we might like. In particular, the intersection of two Σ-split subspaces need not be another locally compact space. Before we are allowed to form an equaliser or coequaliser, we have to satisfy a very awkward property, which turns out to have no computational meaning anyway. (It also leads to mis-conceived questions such as largest cartesian closed categories: the statement that “John is the tallest person who can stand up in here” may say more about the ceiling than about John, if we are talking about children in a tent.) You pays your money, you takes your choice: my construction has a good λcalculus, whilst locales have (infinitary) algebra, which Vickers’ work has exploited very fluently. Plainly we should be asking for both, and there is no fundamental reason why we shouldn’t have them. The resulting category will have many more objects besides locales and colocales, and will in fact be cartesian closed. So the argument from authority (or at least from familiarity) seems to caution against a too hasty search for generality.

The applications to topology do, unfortunately, go rather quickly outside local compactness. Some account of the category of locales is therefore needed quite urgently in abstract Stone duality, and I hope that Vickers’ work will help towards this. It is possible that such a construction would be the first step of an iteration that would lead to the bigger category, whilst retaining the essence of topology that we distill here. I believe that this lies in the preservation by Σ^{Σ^{(−)}} of certain kinds of equalisers, but more liberal notions of subspace and injectivity will be needed.

Nevertheless, both domain theory and rather a lot of the corpus of pure mathematics may be seen as going on in the category of locally compact spaces, so it is well worth continuing to investigate what can be done in the abstract setting that we have so far.

2. The subspace topology

A subset X ⊂ Y of a topological space is said to carry the subspace topology if its open subsets U ⊂ X are exactly those of the form U = X ∩ V for some open subset V ⊂ Y. Since open subsets U ⊂ X correspond bijectively to continuous maps ϕ : X → Σ, there is a more categorical way of saying this:

2.1. Remark. The Sierpiński space Σ is injective with respect to the inclusion i:

X[figure: i] Y
[figure: ϕ; ...............; ψ]

Σ

for any continuous map ϕ : X → Σ, there is some continuous map ψ : Y → Σ such that ϕ(x) = ψ(ix).

In the traditional axiomatisation of general topology, the collections of open subsets of X and Y admit arbitrary unions, and i^{∗} ≡ (−) ∩ X preserves them. This means that there is a greatest open V = i_{∗}U ⊂ Y such that U = V ∩ X, where i^{∗} ⊣ i_{∗}. In particular, if X ⊂ Y is the closed subspace complementary to open W ⊂ Y, we have V = U ∪ W.

As this argument manipulates open subsets and not points, it can be expressed in locale theory. We say that the locale (represented by the frame) A is a sublocale of B if there are monotone functions i^{∗} ⊣ i_{∗} such that i^{∗} is a frame homomorphism and^{2} i_{∗};i^{∗} = id_{A}. These can be recovered from the endomorphism j = i^{∗};i_{∗} on B, which satisfies id_{B} ≤ j = j^{2} and j(b_{1} ∧ b_{2}) = jb_{1} ∧ jb_{2}. Such a j is called a nucleus. In particular, the nuclei corresponding to the open subspace W ⊂ Y and its closed complement are W ⇒ (−) and W ∪ (−) respectively.

2We write “;” for composition in diagrammatic order as far as Section 7, while we argue categorically.

Then we switch the order and use “·” in the development of our new λ-calculus.

The lattice of open subsets of a space Y is the exponential Σ^{Y} in the category of locally compact spaces and continuous functions, when we equip Y with the Scott topology. In this setting, the inverse image map i^{∗} is Σ^{i}. However, the monotone functions i_{∗} and j need not be morphisms between the objects Σ^{X} and Σ^{Y} in this category, as, in terms of the lattices, they need not be Scott continuous.

Many of the features of general topology can be expressed in terms of the λ-calculus that arises from the exponential Σ^{(−)}, together with finitary lattice operations and laws [A, C]. Apart from Theorem 3.11 and some Examples, whose purpose is to motivate the ideas, the whole theory will be formulated in these abstract terms: C denotes a category with an internal distributive lattice Σ, of which all powers Σ^{X} exist in C. In fact, even the lattice structure is not used in the main development of the present paper.

Returning to the idea of injectivity, in practice we need to state it with parameters.

2.2. Lemma. The following are equivalent for i : X → Y:

(a) Σ is injective with respect to i × U : X × U → Y × U for any object U;

(b) Σ^{U} is injective with respect to i : X → Y for any object U;

(c) there is some morphism I : Σ^{X} → Σ^{Y} such that I ; Σ^{i} = id_{Σ^{X}}.

[figure: X × U; i × U; Y × U; X; i; Y]
[figure: ............; ϕ; ............; ψ]
Σ  Σ^{U}

Proof. Parts (a) and (b) are exponential transposes of each other, and (c) is the special case of (b) with U = Σ^{X} and ϕ = η_{X}. Using (b), we obtain I = η_{Σ^{X}} ; Σ^{ψ} : Σ^{X} → Σ^{Y}, as

I ; Σ^{i} = η_{Σ^{X}} ; Σ^{ψ} ; Σ^{i} = η_{Σ^{X}} ; Σ^{η_{X}} = id.

Conversely, ψ = η_{Y} ; Σ^{I} ; Σ^{Σ^{ϕ}} ; Σ^{η_{U}} satisfies

i;ψ = i;η_{Y};Σ^{I};Σ^{Σ^{ϕ}};Σ^{η_{U}} = η_{X};Σ^{Σ^{i}};Σ^{I};Σ^{Σ^{ϕ}};Σ^{η_{U}} = η_{X};Σ^{Σ^{ϕ}};Σ^{η_{U}} = ϕ;η_{Σ^{U}};Σ^{η_{U}} = ϕ.

We therefore have a situation in which i : X^{}^{}Y is a subspace (and Σ is injective with respect to it) in a very explicit sense, namely that the way in which open subsets U ⊂ X are expanded to V ⊂ Y is dictated by a morphism I.

2.3. Definition. i : X → Y is a Σ-split (mono or) subspace if there is some morphism I : Σ^{X} → Σ^{Y} such that I ; Σ^{i} = id_{Σ^{X}}.

[figure: X; i; Y; Σ^{X}; \underline{Σ^{i}}; I; Σ^{Y}]

We shall mark Σ-split monos with a hook like this.

2.4. Remark. The idempotent E = Σ^{i};I on Σ^{Y} plays a role in our λ-calculus similar to that of the nucleus j in locale theory, except that j is uniquely determined by i, whereas E is not. (So in Section 4 we shall appropriate the name “nucleus” for E.) Beware, however, that it is not enough for E to be idempotent, as its epi part Σ^{i} must be a (frame) homomorphism. For locales, this happens iff

E(ϕ ∧ ψ) = E(Eϕ ∧ Eψ) and E(ϕ ∨ ψ) = E(Eϕ ∨ Eψ),

though we shall characterise E by a different (λ-)equation in our abstract setting.

Σ^{Y} is a continuous lattice, whilst E is Scott-continuous, so its splitting Σ^{X} is also a continuous lattice, and the space X is therefore also locally compact.

2.5. Examples. If a localic nucleus j is Scott-continuous, then it can serve as E. Otherwise, E may still exist, no longer providing the largest V, and the map I may extend open subsets from X to Y in very complicated ways. Some sublocales need not, however, be represented at all in our formulation.

(a) In both approaches, I = i_{∗} and E = j = i^{∗} ; i_{∗} = (− ∨ W) encode a closed subspace of Y, namely that complementary to the open subspace W.

(b) In locale theory, j = (W ⇒ −) encodes the open subspace W, but j is not Scott continuous unless W is also closed. Nevertheless, there is another, and rather more obvious, way of “extending” the open subset U ⊂ X to one of Y, namely as U itself. This is of course the smallest V that does the job, so U ↦ V is the left adjoint i_{!} ⊣ i^{∗}. Then I = i_{!} and E = i^{∗} ; i_{!} = (− ∧ W) provide our encoding.

(c) If X^{}^{i_{1}}^{}Y^{}^{i_{2}}^{}Z are successively Σ-split subspaces, with Σ^{X}^{}^{I_{1}}^{}Σ^{Y}^{}^{I_{2}}^{}Σ^{Z}, then the composite X^{}^{i_{1};i_{2}}^{}Z is Σ-split, with Σ^{X}^{}^{I_{1};I_{2}}^{}Σ^{Z}.

(d) Hence locally closed subspaces (open subsets of closed subsets) may be also expressed in this way.

Compact and overt subspaces are considered in [E].

2.6. Example. In set theory, subspaces and open subspaces are the same thing, but we can still distinguish two roles in the preceding discussion. Consider a predicate ϕ ∈ Ω^{X}, which classifies the “open” subset U = {x : X | ϕ[x]} ⊂ X. This may be expanded from the “subspace” X to Y using either of the quantifiers:

(a) I_{∃}ϕ = ∃_{i}ϕ = λy:Y . ∃x:X. (y =_{Y} ix) ∧ ϕ[x], or

(b) I_{∀}ϕ = ∀_{i}ϕ = λy:Y . ∀x:X. (y =_{Y} ix) ⇒ ϕ[x]. As for open and closed subspaces, ∃_{i} and ∀_{i} are the left and right adjoints respectively to the inverse image map i^{∗}. This analogy between open subspaces and the existential quantifier, and between closed subspaces and the universal quantifier, is explored in [C].

The (Scott) topology on an object Y of Dcpo is determined by its order, and is also the exponential Σ^{Y} in that category. However, for a subset X ⊂ Y that is closed under directed joins, the Scott topology on X derived from the restricted order need not be the subspace topology.

2.7. Example. (Moggi) Let Y be the domain of lazy natural numbers, and X ⊂ Y the subset of maximal points ∘ in it, i.e. the numerals s^{n}0 together with the “top” point ∞, omitting the points • of the form s^{n}⊥.

∘ ∞
[figure]
s^{2}0 ∘  ⋯
[figure]
s0 ∘  • s^{2}⊥
[figure]
0 ∘  • s⊥
[figure]
• ⊥

X is the equaliser of the (continuous, recursive) functions f, g : Y ⇉ Y for which f(s^{n}0) = g(s^{n}0) = s^{n+1}0 but f(s^{n}⊥) = s^{n+1}⊥ and g(s^{n}⊥) = s^{n}⊥.

The order on X is discrete, as therefore is its Scott topology.

However, its subspace topology is that of the one-point compactification of ℕ: any open subset U ⊂ X with ∞ ∈ U is of the form

U = ({s^{m}0 | m ≥ n} ∪ {∞}) ∪ F with F ⊂ {s^{m}0 | m < n}

for some n. Then V = {y ∈ Y | y ≥ s^{n}⊥} ∪ F is open in Y with U = X ∩ V. Choosing the least such n, the assignment I : U ↦ V is monotone, so it is Scott-continuous as there are no non-trivial directed joins to be considered. Hence X ⊂ Y is Σ-split, classically. For intuitionistic locale theory, recursion theory and our λ-calculus, the subspace is still an equaliser but the map I is not well defined.

2.8. Remark. The notion of Σ-split subspace has a direct impact on computation in the λ-calculus associated to the exponential Σ^{X}. In any category where it is meaningful, evaluation ev : Σ^{X} × X → Σ is always dinatural in X with respect to any map i : X → Y [ML71, Section IX 4], i.e. the square from Σ^{Y} × X to Σ commutes:

Σ^{Y} × X [figure: Σ^{i} × id; I × id] Σ^{X} × X

[figure: Σ^{Y} × Y; id × i; ev_{Y}; Σ; ev_{X}]

Combining the splitting I with this property, ev_{X} is equal to the composite around the other three sides, or, in symbols,

ϕ : Σ^{X}, x : X ⊢ ϕx = (Iϕ)(ix).  (η)

This equation will later feature as an η-rule of a new λ-calculus for subspaces, based on the axiom of comprehension in set theory. The associated introduction and elimination rules are provided by Σ^{i} and I, whilst the β-rule expresses the composite Σ^{i} ; I = E:

ψ : Σ^{Y} ⊢ I(λx. ψ(ix)) = Eψ.  (β)

The importance of the η-rule is that it enables us to evaluate a function ϕ on a value x in the subspace X by regarding them both as belonging to the ambient space Y instead. Therefore we may reason mathematically in a rich category of subspaces, but execute the computation using the types of the restricted λ-calculus, simply ignoring the new connectives of the comprehension calculus (Section 10).

2.9. Remark. The equation I ; Σ^{i} = id says what we require of the open subsets of X and Y, but does not in fact even force i to be mono on points. We would actually like it to be regular mono, i.e. for there to be an equaliser

[figure: X; i; Y; u; v; Z.]

The corresponding effect on the topologies is

[figure: Σ^{X}; \underline{Σ^{i}}; I; Σ^{Y}; \underline{Σ^{u}}; .; .; .; .; .; .; .; .; .; .; .; .; J; .; .; .; .; .; .; .; .; .; .; \underline{Σ^{v}}; Σ^{Z},]

where the fifth map J will be explained in the next section.

Any Σ-split subspace may be expressed in this form, with

Z = Σ^{Σ^{Y}} ≡ Σ^{2}Y  u = η_{Y}  v = η_{Y} ; Σ^{I} ; Σ^{Σ^{i}}  J = η_{Σ^{Y}} .

Here the natural transformation η_{Y} is given by the λ-expression y ↦ λψ. ψy and is the unit of the adjunction Σ^{(−)} ⊣ Σ^{(−)}. Iteration of the functor Σ^{(−)} obliges us to use the shorthand Σ^{2}Y.

We have, however, been making an assumption about the category.

2.10. Definition. The maps i = η_{X} : X → Y = Σ^{Σ^{X}} and I = η_{Σ^{X}} always satisfy I ; Σ^{i} = id (we call the equation η_{Σ^{X}} ; Σ^{η_{X}} = id the unit law), so X ought to be a subspace of Σ^{2}X. The diagram above becomes

[figure: X; η_{X}; Σ^{2}X; η_{Σ^{2}X}; Σ^{2}η_{X}; Σ^{4}X]

with J = η_{Σ^{3}X}. Recall from Section A 4 that an object X for which this is an equaliser is called sober. Definition 2.3 and the ensuing discussion only make sense if we assume that all objects of C have this property.

A map P : U → Σ^{2}X that has equal composites with this pair is called prime, and we write focus P : U → X for the mediator to the equaliser. Equivalently, the double exponential transpose H : Σ^{X} → Σ^{U} is an Eilenberg–Moore homomorphism, the algebra structures being Σ^{η_{X}} and Σ^{η_{Y}}. Section A 8 developed the λ-calculus with focus, and in particular focus(λϕ. ϕa) = a.

2.11. Notation. We shall also make use of maps J : Σ^{X} → Σ^{U} that need not be homomorphisms. We write Ĵ : U −× X as if this were a “second class” map between these objects, and HC for the category with these morphisms, but the same objects as C. For example, we may now write the equation for a Σ-split subspace as i; Î = id_{X}.

We define force_{X} ≡ η̂_{Σ^{X}} : Σ^{2}X −× X, which is natural in HC and (by the unit law) satisfies η_{X} ; force_{X} = id_{X}.

If H : Σ^{X} → Σ^{U} is a homomorphism, then we write Ĥ : U → X, with an ordinary arrowhead instead of −×, and SC for the category with these morphisms. When all objects are sober, SC ≅ C, i.e. any such Ĥ : U → X is of the form H = Σ^{f} for some unique ordinary morphism f : U → X in C, and we write f : U → X instead of Σ̂^{f}.

In fact, Ĥ = focus P = P ; force_{X}, where the prime P is the double exponential transpose of H (Lemma A 7.5). The reason for the distinction between focus and force is that the former is part of a denotational calculus, whilst the latter introduces “computational effects”.

2.12. Example. When C = LKLoc is the category of locally compact locales, SC is the opposite of the category of (continuous) frames and frame homomorphisms, so SC ≅ C. H : U −× X denotes a Scott-continuous map from the topology on X to that on U.

3. Beck’s theorem

Now we relate subspaces as we have just described them to Stone duality as presented in Section 1. In the abstract setting, the diagrams shown there are as follows, where A is the category of Eilenberg–Moore algebras for the monad induced by the adjunction Σ^{(−)} ⊣ Σ^{(−)}.

C^{op} [figure: X ↦ (Σ^{X}, Σ^{η_{X}}); ≃; \underline{pts}] A

C \begin{aligned}Σ^{(−)} &  \\ & ⊣ Σ^{(−)}_{} \end{aligned}= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = C \begin{aligned}X ↦ (Σ^{Σ^{X}}, μ_{X}) &  \\ & ⊣ (A, α) ↦ A_{} \end{aligned}

We shall show that subspaces (i.e. certain equalisers) exist in C and carry the subspace topology iff (idempotents split and) the functor C^{op} → A is an equivalence of categories. This functor is full and faithful iff all objects are sober (Theorem A 4.10), so our task in this paper is to say when it is essentially surjective. In fact we shall construct the pseudo-inverse functor. The argument works though the proof Beck’s theorem in our special case.

3.1. Definition. An algebra (A, α) is spatial if there is some algebra isomorphism

[figure: Σ^{2}A; Σ^{2}H; Σ^{3}X; A; α; H; Σ^{X}; Σ^{η_{X}}]

Recall from Lemma A 4.3 that a map H : A → Σ^{U} (not necessarily an isomorphism) is a homomorphism iff its double exponential transpose P has equal composites

[figure: U; P; Σ^{A}; Σ^{α}; η_{ΣA}; Σ^{3}A,]

so our first attempt at spatiality of (A, α) is to form this equaliser [Fak70]. Afterwards we have to find out when H is an isomorphism.

3.2. Proposition. The contravariant functor X ↦ (Σ^{X}, Ση_{X}) : C^{op} → A has a symmetric adjoint on the right, called pts, so

X ^{}pts(A, α) in C = A ^{}Σ^{X} in A

iff for each algebra (A, α) the equaliser

[figure: pts(A, α); i; Σ^{A}; Σ^{α}; η_{ΣA}; Σ^{3}A]

exists in C.

Proof. By the foregoing argument, there must also be a correspondence with maps

[figure: X; Σ^{A}; Σ^{3}A,]

but this is just the universal property of the equaliser.

The inverse functor pts : A → C^{op} takes the algebra A to the “set” A(A, Σ) of homomorphisms, just as the forward one took the object X to the function-space C(X, Σ). (Remark 7.4 explains how A(A, B) can sometimes be defined as an object of C, rather than as an external hom-set.)

3.3. Theorem. The contravariant adjunction of Σ^{(−)} and pts is an equivalence between C^{op} and A iff all objects of C are sober and all algebras in A are spatial.

Proof. Sobriety and spatiality merely say that the units of the symmetric adjunction,

X → pts(Σ^{X}, Σ^{η_{X}}) and H : A → Σ^{ptsA},

are isomorphisms.

More particularly, without assuming that all objects are sober, the functor pts : A^{op} → C is full and faithful (making A^{op} reflective in C) iff all algebras are spatial. Joachim Lambek and Basil Rattray considered this situation abstractly (writing QA for our Σ^{ptsA}), together with applications to Abelian categories and elementary toposes [LR75]. More recently, Giuseppe Rosolini connected their results with topos models of synthetic domain theory [BR98].

We can characterise spatiality in terms more like those of the previous section.

3.4. Proposition. (A, α) ≅ Σ^{X} iff there are i : X → Σ^{A} and I : Σ^{X} → Σ^{2}A such that

i is prime, I ; Σ^{i} = id_{Σ^{X}} and Σ^{i} ; I = α; η_{A} ≡ η_{Σ^{2}A} ; Σ^{2}α.

In this case, X = pts(A, α) ^{i}^{}Σ^{A} is the equaliser in Proposition 3.2, and Σ^{(−)} takes it to a split coequaliser.

[figure: A; η_{A}; \underline{α}; Σ^{2}A; \underline{Σ^{2}α}; \underline{Ση_{ΣA}}; η_{Σ^{2}A}; Σ^{4}A]
[figure: Σ^{i}]
Σ^{X}^{H_{}. . . . . . . . . . . . . . . . .}

Proof. If H : A ≅ Σ^{X} is an isomorphism of algebras then its double exponential transpose i = η_{X} ; Σ^{H} is prime, and we may put I = H^{−1} ; η_{A} = η_{Σ^{X}} ; Σ^{2}H^{−1}. Then

I ; Σ^{i} = η_{Σ^{X}} ; Σ^{2}H^{−1} ; Σ^{2}H ; Σ^{η_{X}} = η_{Σ^{X}} ; Σ^{η_{X}} = id
Σ^{i} ; I = Σ^{2}H ; Σ^{η_{X}} ; H^{−1} ; η_{A} = α; H ; H^{−1} ; η_{A} = α; η_{A}.

Conversely, if i is prime then its double transpose H = η_{A} ; Σ^{i} is a homomorphism, and H^{−1} = I ; α because

η_{A} ; Σ^{i} ; I ; α = η_{A} ; α; η_{A} ; α = id
I ; α; η_{A} ; Σ^{i} = I ; η_{Σ^{2}A} ; Σ^{2}α; Σ^{i} = I ; η_{Σ^{2}A} ; Σ^{η_{Σ^{A}}} ; Σ^{i} = I ; Σ^{i} = id

since i, being prime, has equal composes with Σ^{α} and η_{Σ^{A}}.

To show that X is the equaliser, consider Γ →^{P} Σ^{A} ⇉ Σ^{3}A. The double transpose K : A = Σ^{X} → Σ^{Γ} of P is a homomorphism, so, since X is sober, K = Σ^{k}, where k : Γ → X mediates to the equaliser. The image of the equaliser diagram under Σ^{(−)} is the split coequaliser shown above.

3.5. Remark. In the λ-calculus, these equations are

x : X, ϕ : Σ^{X} ⊢ (Iϕ)(ix) = ϕ(x)  (η)
F : Σ^{A}, F : Σ^{2}A ⊢ I(λx. F(ix))(F) = F (αF).  (β)

The η-equation, which says that Σ^{X} is a retract of A, was discussed in the previous section: it makes X a Σ-split subspace of Σ^{A}.

The β-equation makes H : A^{}^{}Σ^{X} a subalgebra that is “U-split” in Beck’s language, i.e. split by a function that need not be a homomorphism. This property says that there are enough points to distinguish the elements of A, considered as “open subsets” of X.

3.6. Remark. The same caveat applies to our definition of “spatial” algebras as to that of “sober” spaces in Remark A 5.10: the correspondence with the lattice-theoretic notion in [Joh82, Section II 1.5] is a conceptual one rather than a theorem. In particular, recall from [Joh82, Theorem VII 4.3] that (using the axiom of choice) any distributive continuous lattice A has enough points (completely coprime filters) in the classical sense. All algebras over LKLoc are spatial in the constructive sense that there are enough generalised “points” Γ → pts(A, α), cf. [Vic95].

Beck’s theorem and our treatment of subspaces consider the maps and equations in the main equaliser diagram, without requiring the objects to be Σ^{2}A, Σ^{3}X, etc.

3.7. Definition. A parallel pair u, v : Y ⇉ Z in C is called a Σ-split pair if there is some map (not necessarily a homomorphism) J : Σ^{Y} → Σ^{Z} such that

J ; Σ^{u} = id_{Σ^{Y}} and Σ^{u} ; J ; Σ^{v} = Σ^{v} ; J ; Σ^{v}.

Notice that we just mark one of the maps with a hook, to emphasise the fact that the conditions are not symmetrical in u and v.

[figure: Σ^{Y}; \underline{Σ^{u}}; J; \underline{Σ^{v}}; Σ^{Z}; Y; u; v; Z]
[figure: ψ; J; θ]
Y[figure: u; ×  \underline{Ĵ}; v] Z  Σ

It is helpful to see these equations expressed in other ways. Using Notation 2.11, they are

u; Ĵ = id and v ; Ĵ; u = v ; Ĵ; v.

Mixing application with categorical composition, we have

u; J(ψ) = ψ and v ; J(u; θ) = v ; J(v ; θ).

Using the λ-calculus, the equations are

\begin{aligned}y : Y, ψ : Σ^{Y} & ⊢ & (Jψ)(uy) = ψ(y) \\ y : Y, θ : Σ^{Z} & ⊢ & J(λy. θ(uy))(vy) = J(λy. θ(vy))(vy). \end{aligned}

We shall need the equaliser i : X → Y of u and v, for which we would like Σ^{i} : Σ^{Y} → Σ^{X} also to be the coequaliser of Σ^{u} and Σ^{v}. In this case there is a (unique) map I : Σ^{X} → Σ^{Y} with I ; Σ^{i} = id_{Σ^{X}} and Σ^{i} ; I = J ; Σ^{v}.

Reversing the arrows, there is a similar notion of Σ-split coequaliser (Section 11), whilst (unqualified) split equalisers and coequalisers also arise, in which the equations already hold at the base level, without applying the functor Σ^{(−)}. Split (co)equalisers are absolute in the sense that, being equationally defined, they are preserved by all functors. Absolute coequalisers were first studied by Robert Paré [Par71]. Examples of absolute pushouts may be found in Section 7, [Tay99, Exercise 5.3] and [D].

We construct the equaliser of a split pair by splitting an idempotent (Remark 4.1). In particular, Σ^{X} splits E = Σ^{v} ; J. Conversely, any idempotent e : Y → Y gives rise to a split pair (e, id), with J = E = Σ^{e}, so such splittings are necessary.

There is no greater generality in supposing that i is split only after further iteration of the functor Σ^{(−)}, since if I;Σ^{3}i = id then I;Σ^{i} = id by the unit law, where I = η_{Σ^{X}};I;Σ^{η_{Y}}.

3.8. Proposition. If the functor pts exists, all objects are sober and idempotents split, then C has equalisers of all Σ-split pairs. If, additionally, all algebras are spatial, Σ^{(−)} takes these equalisers to (split) coequalisers.

Conversely, if C has equalisers of all Σ-split pairs, and Σ^{(−)} takes them to coequalisers, then all algebras are spatial.

Proof. Let u, v : Y ⇉ Z have splitting J : Σ^{Z} → Σ^{Y}, so that E = Σ^{v} ; J is an idempotent on Σ^{Y}, and let A be its splitting, as in the top rows of the diagrams. Since this coequaliser is absolute, Σ^{2}A is also a coequaliser, so the structure α may be obtained as the mediator; similar arguments involving Σ^{4}A show that it satisfies the equations for an Eilenberg–Moore algebra.

[figure: pts(A, α); .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Y; u; v; Z]

[figure: A; \underline{q}; I; Σ^{Y}; \underline{Σ^{u}}; J; \underline{Σ^{v}}; Σ^{Z}]

[figure: Σ^{A}; i; Σ^{q}; Σ^{2}Y; η_{Y}; Σ^{2}u; Σ^{2}v; Σ^{2}Z; η_{Z}]

[figure: Σ^{2}A; α; Σ^{3}Y; Σ^{η_{Y}}; Σ^{3}Z; Σ^{η_{Z}}]

[figure: Σ^{3}A; Σ^{α}; η_{Σ^{A}}; Σ^{4}Y; Σ^{4}Z]

I claim that pts(A, α) is the equaliser of u and v.

All composites pts(A, α) → Σ^{4}Y are equal, so they factor through η_{Y} since Y is sober. This defines the dotted map. It has equal composites with u and v because all composites pts(A, α) → Σ^{2}Z are equal and η_{Z} is mono.

Any test map Γ → Y having equal composites with u and v also has equal composites with Σ^{2}u and Σ^{2}v, since η is natural, so it factors through their equaliser, Σ^{A}. For the same reasons it has equal composites with Σ^{A} ⇉ Σ^{3}A, and so factors through their equaliser pts(A, α). The mediator is unique because i and Σ^{q} are mono.

Now apply Σ^{(−)} to the left-hand diagram, so Σ^{pts(A,α)} ≅ A and Σ^{i} ≅ α by Theorem 3.3 since A is spatial. Then Σ^{(−)} takes the top two rows of the diagram on the left to the one on the right.

Since pts is itself a Σ-split equaliser, the converse follows from Proposition 3.4.

3.9. Remark. Because of the fact that Σ^{(−)} takes it to the coequaliser of Σ^{Y} ⇇ Σ^{Z}, the diagram X → Y ⇉ Z is also an equaliser in HC, i.e. with respect to “second class” test maps F̂ : Γ −× Y ⇉ Z (Notation 2.11).

This is in contrast to the situation for products, where the failure of the extension of the universal property from C to HC is essentially related to the interpretation of computational effects [Thi97]. The fact that equalisers are valid even in the presence of such effects may be regarded as the categorical justification of the use of Floyd–Hoare logic for imperative as well as functional programs.

It is still not clear precisely what the exactness properties of Σ^{(−)} should be, as not all equalisers are taken to coequalisers:

3.10. Example. Suppose that C has disjoint coproducts, as is the case for Set and LKSp, and also in the abstract situation by Theorem 11.8. Then

[figure: 0; 2; id; swap; 2,]

is an equaliser (where swap interchanges the elements of 2), but Σ^{(−)} takes it to

[figure: 1; Σ; Σ × Σ; \underline{id}; \underline{swap}; Σ × Σ,]

where swap interchanges the components of the product.

We can now prove the intuitionistic form of Stone duality for locally compact locales.

3.11. Theorem. LKLoc is monadic.

Proof. We must show that every object is sober, that equalisers of Σ-split pairs exist, and that Σ^{(−)} takes them to coequalisers. Recall from the theory of locales and continuous lattices [GHK^{+}80, Joh82] that the topology on a locally compact locale is a distributive continuous lattice, whilst the category Cont of continuous lattices and Scott continuous functions is fully embedded (via the Scott topology) as a subcategory of LKLoc that is closed under retracts.

[figure: Σ^{X}; Σ^{3}X; Σ^{5}X]

The equaliser diagram of locales involved in the definition of sobriety gives rise to diagram of frames shown above, where [figure] denotes a frame homomorphism and^{}^{}a Scott continuous function. This is a split coequaliser in Cont and so ā fortiori a coequaliser in LKFrm, i.e. an equaliser in LKLoc.

LKLoc^{op} = = = = = = = LKFrm^{⊂} Frm

LKLoc \begin{aligned}Σ^{(−)} &  \\ & ⊣ Σ^{(−)}_{} \end{aligned}^{_{}Σ(−) ^{⊃}} Cont U′_{}\overline{}Set \begin{aligned}F &  \\ & ⊣ U_{} \end{aligned}

Now let u, v : Y ⇉ Z be a Σ-split pair in LKLoc. We follow it around the diagram of categories and functors above.

E = J ; Σ^{v} is a Scott continuous idempotent on the continuous frame Σ^{Y}, so it is split by some continuous lattice Q. Hence

[figure: Σ^{Z}; Σ^{u}; Σ^{v}; \underline{J}; Σ^{Y}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; q; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; I; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Q]

is a split coequaliser diagram in LKLoc, although we may just as well see it as being in Cont or Set.

The forgetful functor U : Frm → Set, being monadic [Joh82, Theorem II 1.2], creates this coequaliser in Frm, so the lattice Q is actually a frame, and the map Σ^{Y} ↠ Q is a frame homomorphism. This means that Q ≅ Σ^{X} for some locale X, which is locally compact since Q is continuous, and q = Σ^{i}. Hence the diagram is a coequaliser in LKFrm, so X is the equaliser in LKLoc, which Σ^{(−)} takes to the original split coequaliser.

We conclude our introductory discussion with an example of a non-spatial algebra. Classically, the two-point set classifies subsets in Set, open subsets in LKSp (when

it is given the Sierpiński topology), and upper subsets in Pos (when it is given the order ⊥ < ⊤). The monad may therefore be defined on Pos using this object, which we call Υ.

3.12. Example. In (Pos, Υ), all objects are sober classically but not intuitionistically (Remark C 5.10(c)). Pos does not have the monadic property, because the unit interval, A = [0, 1] with the usual arithmetical order, is an Eilenberg–Moore algebra (in a unique way) that does not have enough points.

This discussion of [0, 1] extends that in [FW90, Example 9]. In fact, the algebras for this version of the monad are constructively completely distributive lattices [MRW02].

Proof. Classically, the upper sets of A are of the form (a, 1] or [a, 1]. Indeed Σ^{A·n} = A^{op} · (n + 1), where A · n is A × n with the lexicographic order: ⟨a, i⟩ ≤ ⟨b, j⟩ if a < b, or a = b and i ≤ j.

[figure: ∅; Σ^{A} ≡ A · 2; η_{A·2} : 0, 1 ↦ 1, 2; Σα : 0, 1 ↦ 0, 3; A · 4; A; α; Σ^{Σ^{A}} ≡ A · 3; \underline{2, 2, 1, 0, 0 ← 0, 1, 2, 3, 4 : Ση_{A·2}}; \underline{2, 0, 0, 0, 0 ← 0, 1, 2, 3, 4 : Σ^{2}α}; A · 5]

The maps we’re interested in act as the identity on the real part, and as shown above on the numerical part.

4. Adding Σ-split subspaces

The rest of the paper shows (in three different ways) how to construct a category \overline{C} in which we may form subspaces as just described, i.e. equalisers of Σ-split pairs that Σ^{(−)} takes to coequalisers. As raw material, we simply require a category C with finite products and an exponentiating object Σ, such that all objects of C are sober. A category C of this kind was defined using a λ-calculus in Section A 8. In Section 7 we shall see that A^{op} does the job, but first we do it by adding formal equalisers of Σ-split pairs.

This construction is similar to that of the so-called Karoubi completion of a category, which forces it to have splittings of idempotents. However, as the new construction is rather more complicated, you would be well advised to (re)familiarise yourself with the simpler version by proving

4.1. Remark. The Karoubi completion, KC, of any category C has • as objects, (X, e), where e : X → X is an idempotent, that is, e; e = e, and

• as morphisms f : (X, e_{1}) → (Y, e_{2}), the C-maps f : X → Y with e_{1} ; f = f = f ; e_{2}. Then

(a) composition is inherited from C, but the identity on (X, e) is e, and

(b) the idempotents e′ of KC are those of C, but they split in KC, i.e. there are maps p and i in KC such that i; p = id and p; i = e′.

(c) KC is the universal way (up to equivalence) of splitting idempotents in C.

From a categorical point of view, it would be easier to assume that idempotents split in C. This would “modularise” the construction of \overline{C} as C ↦ KC ↦ A_{KC} ↦ \overline{C}. However, our intention (in Section 10) is to reduce computation in \overline{C} back to the restricted λcalculus, i.e. C. KC already has some subspaces for the convenience of mathematicians, whereas the idempotents infest computations in it, so it has already crossed the line of demarcation between these subjects. For this reason, we develop a representation of \overline{C}-objects directly in terms of C that splits idempotents as well as equalisers.

4.2. Definition. A typical object X of our category \overline{C} is a Σ-split pair (Definition 3.7), which we may write using Notation 2.11 simply as

Y[figure: u; v; ×  \underline{Ĵ}] Z,

such that u; Ĵ = id_{Y} and v ; Ĵ; u = v ; Ĵ; v : Y −× Z. This object will temporarily be called (Y ⇉ Z), or just X, in parts of the argument up to Section 6.

The identity morphism on this object will be Ê = v;Ĵ. As in the Karoubi construction, this is an idempotent endomorphism of Y, but in the auxiliary category HC. In fact, its defining equation is stronger than idempotence.

4.3. Definition. E : Σ^{Y} → Σ^{Y} is called a nucleus on Y if Ê ; η_{Y} ; Σ^{E} = Ê ; η_{Y}, or

F : Σ^{3}Y ⊢ E(λy. F(λϕ. Eϕy)) = E(λy. F(λϕ. ϕy))

using the λ-calculus. Observe carefully that the left hand side has an extra E.

We shall write \{Y | E\} instead of (Y ⇉ Z) for an object of \overline{C} defined in terms of Ê like this.

When Ê is a first class map (E = Σ^{e} and e = Ê), the equation is just idempotence (e = e; e). In general, however, it says more than Ê = Ê; Ê, for the same reason that we remarked in Definition 2.3, namely that, in the splitting of this second class idempotent as Î; i, the inclusion part i must actually be first class.

4.4. Notation. Given two nuclei, E_{1} and E_{2}, we write Ê_{2} ⊂_{Y} Ê_{1} if

Ê_{1} ; Ê_{2} = Ê_{2} = Ê_{2} ; Ê_{1}.

4.5. Definition. A typical morphism from {Y_{1} | E_{1}} to {Y_{2} | E_{2}} is an HC-map Ĥ : Y_{1} −× Y_{2} such that

Ĥ = Ĥ ; Ê_{2} and Ê_{1} ; η_{Y_{1}} ; Σ^{H} = Ĥ ; η_{Y_{2}},

the first equation being equivalent to Ĥ; u_{2} = Ĥ; v_{2} when {Y_{2} | E_{2}} is defined by the pair u_{2}, v_{2} : Y_{2} ⇉ Z_{2}. Using λ-calculus, the second equation is

G : Σ^{3}Y_{2} ⊢ E_{1}(λx:Y_{1}. G(λψ:Σ^{Y_{2}}. Hψx)) = H(λy:Y_{2}. G(λψ. ψy)),

which adds E_{1} to the λ-equation for a homomorphism (Remark A 4.11).

4.6. Lemma. Any morphism Ĥ : {Y_{1} | E_{1}} → {Y_{2} | E_{2}} also satisfies Ĥ = Ê_{1} ; Ĥ.

Proof.

Ĥ = Ĥ ; η_{Y_{2}} ; η̂_{Σ^{Y_{2}}}  unit law
= Ê_{1} ; η_{Y_{1}} ; Σ^{H} ; η̂_{Σ^{Y_{2}}}  second H equation
= Ê_{1} ; η_{Y_{1}} ; η̂_{Σ^{Y_{1}}} ; Ĥ  naturality
= Ê_{1} ; Ĥ  unit law.

4.7. Lemma. For any split pair, E = J ; Σ^{v} is a nucleus (Definition 4.3); in particular, Ê is idempotent in HC.

Proof. The equation for Ê is the same as the second one for a morphism Ĥ = Ê in Remark 4.5. It follows from the defining equations for u, v and J:

Ê ; η_{Y} ; Σ^{E} = v ; Ĵ; η_{Y} ; Σ^{2}v ; Σ^{J}
= v ; Ĵ; v ; η_{Z} ; Σ^{J}  naturality of η
= v ; Ĵ; u; η_{Z} ; Σ^{J}  second uvJ equation
= v ; Ĵ; η_{Y} ; Σ^{2}u; Σ^{J}  naturality of η
= v ; Ĵ; η_{Y} = Ê ; η_{Y}  first uvJ equation.

The first equation for a morphism is idempotence of Ĥ = Ê, which follows from the previous result, but explicitly from the uvJ equations,

Ê ; Ê = v ; Ĵ; v ; Ĵ = v ; Ĵ; u; Ĵ = v ; Ĵ = Ê.

4.8. Proposition. \overline{C} is a category.

Proof. We have to show that composition is well defined. Let Ĥ : Y_{1} → Y_{2} and

K̂ : Y_{2} → Y_{3}. Then Ĥ ; K̂ ; Ê_{3} = Ĥ ; K̂ = { \atop K;H} and

Ê_{1} ; η_{Y_{1}} ; Σ^{K;H} = Ê_{1} ; η_{Y_{1}} ; Σ^{H} ; Σ^{K}
= Ĥ ; η_{Y_{2}} ; Σ^{K}  second H equation
= Ĥ ; Ê_{2} ; η_{Y_{2}} ; Σ^{K}  first H equation
= Ĥ ; K̂ ; η_{Y_{3}}  second K equation,

so Ĥ ; K̂ satisfies the definition of a morphism. Associativity is inherited from C, whilst the equations that say that Ê is the identity on {Y | E} are those in Definition 4.5 and Lemma 4.6.

4.9. Remark. Although there is more to the data for an object of \overline{C} than the maps u and v, the justification of calling such an object a “pair” is that, if we have two splittings J_{1} and J_{2}, then Ê_{1} = v ; Ĵ_{1} and Ê_{2} = v ; Ĵ_{2} define an isomorphism between these objects of \overline{C}. For example, we shall see in Proposition 5.12 that the binary product of any two non-trivial objects has two different splittings.

4.10. Lemma. C is embedded as a full subcategory of \overline{C} by

X ↦ {X | id} ≡ X[figure: id; id; × _{id}] X
f : X → Y ↦ H = Σ^{f} : Σ^{Y} → Σ^{X}.

(Recall that we assume that all objects of C are sober.)

4.11. Remark. Definition 2.10 provided another embedding, which represents X by its standard resolution,

[figure: X; η_{X}; ×  \underline{η̂_{Σ^{X}}}; Σ^{2}X; η_{Σ^{2}X}; Σ^{2}η_{X}; × \underline{η_{Σ^{3}X}}; Σ^{4}X.]

This makes

X [figure: η_{X}; ≅; \underline{η̂_{Σ^{X}}}] \{Σ^{2}X | E\},

where E = η_{Σ^{3}X} ; Σ^{3}η_{X} = Ση_{X} ; η_{Σ^{X}} by F ↦ λF. F (λx. F(λϕ. ϕx)).

The nucleus E is enough on its own to represent the object.

4.12. Lemma. For any object (Y ⇉ Z), we have the isomorphism in \overline{C}

Z  Σ^{2}Y
≅
[figure: Y; Ĵ ; ×; u; v; Y; η̂_{Σ^{Y}} ; ×; η_{Y}; (η_{Y} ; Σ^{E})]

encoded by Ê = v ; Ĵ in both directions.

Proof. The object on the right gives rise to the same nucleus because

η_{Y} ; Σ^{E} ; η̂_{Σ^{Y}} = η_{Y} ; η̂_{Σ^{Y}} ; Ê = Ê

by naturality and the unit law. It satisfies Definition 4.2 because η_{Y} ; η̂_{Σ^{Y}} = id_{Y} and

Ê ; η_{Y} ; Σ^{E} = Ê ; η_{Y}

since E is a nucleus. Hence both objects are {Y | E}, on which Ê is the identity, and it also serves as the isomorphism in both directions.

4.13. Corollary.

(a) Every Σ-split mono arises in this way.

(b) In particular, so does any first class retract.

(c) Composites of Σ-split monos are Σ-split monos (Example 2.5(c)).

Proof. Given X × Î^{[figure: i]} Y with i; Î = id_{X}, put Ê = Î; i as in Remark 2.9.

This satisfies the Ê equation because

Î; i; η_{Y} ; Σ^{I} ; Σ^{2}i = Î; η_{X} ; Σ^{2}i; Σ^{I} ; Σ^{2}i = Î; η_{X} ; Σ^{2}i = Î; i; η_{Y}

by naturality of η and i; Î = id_{X}. For composition, Ê = i_{1} ; i_{2} ; Î_{2} ; Î_{1}.

Although Ê suffices to describe an object of the new category, and will be used in the new calculus in Section 8, it is not very illuminating. The reason for introducing the Σ-split pair (Y ⇉ Z) is that the new object is its formal equaliser, as in Proposition 3.8.

4.14. Proposition. Every object (Y ⇉ Z) of \overline{C} is the equaliser in \overline{C} of the diagram that it suggests, considered to consist of images ( via Lemma 4.10) of objects and maps in C. If this diagram already has an equaliser X in C, and Σ^{(−)} takes it to a coequaliser in C, then (Y ⇉ Z) ≅ X in \overline{C}.

Proof. For any object Γ = (Y_{0} ⇉ Z_{0}) of \overline{C}, we check that an HC-map Ĥ : Y_{0} −× Y satisfies the conditions for being a \overline{C}-map Γ → (Y ⇉ Z) iff it satisfies those for being a \overline{C}-map Γ → (Y ⇉ Y) that has equal composites with u and v. This is simply a matter of changing the status of the equation Ĥ ; u = Ĥ ; v from being part of Definition 4.5 of a \overline{C}-morphism to being a test for the equaliser.

[figure: X; i; Y; u; v; Z; Σ^{X}; \underline{Σ^{i}}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; I; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{Y}; \underline{Σ^{u}}; J; \underline{Σ^{v}}; Σ^{Z}]

For the second part, J ; Σ^{v} : Σ^{Y} → Σ^{Y} has equal composites with Σ^{u} and Σ^{v}, whose coequaliser is Σ^{X} by hypothesis, so E = J;Σ^{v} = Σ^{i};I for some I as shown. Both I;Σ^{i} and id mediate from the equaliser to Σ^{X}, so are equal by uniqueness. Then i : X → (Y ⇉ Z) is an isomorphism, with inverse Î: (Y ⇉ Z) → X.

As the construction of \overline{C} is one that “freely adjoins equalisers” we would expect at this point to have to show that \overline{C} does in fact have such equalisers, including those for newly defined parallel pairs, and that Σ^{(−)} takes them to coequalisers. However, in our case, powers of Σ are involved in this statement, whereas we still have a lot of work to do to construct such powers in \overline{C}. This will be done in Proposition 6.10.

We draw one easy corollary from the Proposition here, largely to show the contrast with the more difficult study of products that follows in the next section.

4.15. Proposition. The functor C → \overline{C} preserves such colimits as exist.

Proof. Let (U_{i}) be a diagram in C. Any cocone under it with vertex (Y ⇉ Z) in \overline{C} is, by the previous result, a cocone with vertex Y such that for each i the composites U_{i} → Y ⇉ Z are equal. But this cocone might as well be in C, and has a mediator U = colimU_{i} → Y, which also has equal composites U → Y ⇉ Z, and is therefore a mediator U → (Y ⇉ Z) in \overline{C}.

5. Injectives and products in \overline{C}

We know from Section A 6, and from the work on continuations by others cited there, that binary products are the crucial issue. These studies have also taught us that we must take just one step at a time. In Section 7 below we sketch the construction of products in \overline{C} as coproducts of algebras, but the motivation of that approach involves the anticipation of results that ought to follow from the conclusion itself.

In this section we argue forwards from the structure in the given category C, using basic (albeit pedestrian) categorical ideas, and sticking to the objects rather than their algebras of predicates. The plan is to regard \overline{C}-objects as equalisers in C as in Proposition 4.14, and then use the given products in C.

However, the universal property of these given products is only tested by diagrams of the form Γ → A × B with Γ ∈ ob C, so we need to generalise this to Γ ∈ ob \overline{C}. This is more difficult than the situation for colimits in Proposition 4.15: in this case we need to be able to turn maps {Y | E} → A into Y → A, which is just the property of injectivity from which we began in Remark 2.1.

5.1. Definition. An object A of \overline{C} is said to be injective if, for any subspace inclusion {Y | E}^{}^{}Y and map f : {Y | E} → A, there is some (not necessarily unique) map h : Y → A such that f = Ê ; h.

{Y | E}[figure: Ê] Y
[figure: f; ...............; h]
A

5.2. Proposition. An object A of \overline{C} is injective iff it is a retract of some Σ^{U} (by which we still mean the exponential in C). Indeed, when A ∈ ob C is injective, there is a map α : Σ^{2}A → A such that η_{A} ; α = id, though this need not satisfy the other equation that is required for (A, α) to be an Eilenberg–Moore algebra, namely μ_{A} ; α = Σ^{2}α; α.

Proof. (⇐) Suppose first that A = Σ^{U}, and put α = Σ^{η_{U}}. By Definition 4.5, any morphism Ĥ : \{Y | E\} → A in \overline{C} satisfies

Ĥ = Ĥ ; η_{A} ; α = Ê ; η_{Y} ; Σ^{H} ; α = Ê ; h,

where h = η_{Y} ; Σ^{H} ; α is in C. The result extends to retracts of Σ^{U} by composition with the inclusion and surjection.

[figure: {Y | E}; Ê; Y; η_{Y}; Σ^{Σ^{Y}}; {Y | E}; Ê; Y]
[figure: Ĥ = id; ...............; h]
[figure: A = \{Y | E\}; A = \{Σ^{U} | Σ^{e}\}; Ĥ; e; \underline{e}; Σ^{U}; h; . . . . . . . . . . . . . . . .]

(⇒) The composite {Y | E}^{}^{}Σ^{2}Y is a subspace by Corollary 4.13; injectivity says that this is split by h. When A = Y ∈ ob C, α = h satisfies η_{A} ; α = id.

5.3. Corollary. \overline{C} has enough injectives: each object \{Y | E\} is a subspace of some injective Σ^{2}Y.

5.4. Examples. In LKSp, the injectives are the continuous lattices equipped with the Scott topology [Sco72], whilst the algebras are also distributive. In Set, injectives are (sets that carry the structure of) complete lattices and algebras are powersets (which, classically, are complete atomic Boolean algebras).

5.5. Lemma. Any finite product of injectives (or algebras) is again injective (respectively, an algebra).

Proof. For the terminal object, α = !_{Σ^{Σ}}.

For injectives (A, α) and (B, β), we define P_{0} = Σ^{2}π_{0} ; α : Σ^{2}(A × B) → A and P_{1} = Σ^{2}π_{1} ; β : Σ^{2}(A × B) → B, and then η_{A×B} ; ⟨P_{0}, P_{1}⟩ = id. This follows from naturality of η, as illustrated in the right-hand trapezium below.

Moreover, if (A, α) and (B, β) are algebras then

Σ^{2}⟨P_{0}, P_{1}⟩; ⟨P_{0}, P_{1}⟩; π_{0}

= Σ^{4}π_{0} ; Σ^{2}α; α
= Σ^{4}π_{0} ; ΣηΣA; α
= ΣηΣ(A × B) ; Σ^{2}π_{0} ; α
= ΣηΣ(A × B) ; ⟨P_{0}, P_{1}⟩; π_{0}

so (A × B, ⟨P_{0}, P_{1}⟩) is also an algebra.

5.6. Lemma. The functor C → \overline{C} preserves the terminal object.

{Y | E}[figure: Ê] Y
[figure: Ĥ; ...............; h]

1

Proof. Since 1 is injective, Ê ; !_{Y} is the only map Ĥ : {Y | E} → 1.

5.7. Lemma. The functor C → \overline{C} preserves binary products of injectives.

\overline{Σ^{F}}
[figure: Σ^{2}Y; Σ^{H}; Σ^{K}; Σ^{2}(A × B); Σ^{2}π_{0}; Σ^{2}A]

[figure: Y; η_{Y}; \overline{f}; A; η_{A}; α]
[figure: ..................................; ⟨f, g⟩, h, k; π_{0}]

[figure: {Y | E}; Ê; Ĥ; K̂; A × B; η_{A×B}; ⟨P_{0}, P_{1}⟩]
\overline{F̂}  ^{}

Proof. Let F̂ : \{Y | E\} → A and Ĝ : \{Y | E\} → B in \overline{C}. Put

f = η_{Y} ; Σ^{F} ; α and g = η_{Y} ; Σ^{G} ; β,

so F̂ = Ê ; f and Ĝ = Ê ; g by Proposition 5.2, and ⟨f, g⟩ is given by the product in C. Then Ĥ = Ê ; ⟨f, g⟩ : {Y | E} → A × B satisfies Ĥ ; π_{0} = F̂ and Ĥ ; π_{1} = Ĝ. Suppose that Ĥ and K̂ both satisfy these equations. Using Lemma 5.5, put

h = η_{Y} ; Σ^{H} ; ⟨P_{0}, P_{1}⟩ and k = η_{Y} ; Σ^{K} ; ⟨P_{0}, P_{1}⟩,

so Ĥ = Ê ; h and K̂ = Ê ; k by Proposition 5.2.

Since Σ^{H} ; Σ^{2}π_{0} = Σ^{F} = Σ^{K} ; Σ^{2}π_{0}, we have h; π_{0} = f = k ; π_{0} by the way in which h, k and f were constructed, and similarly h; π_{1} = g = k ; π_{1}. Hence h = k = ⟨f, g⟩, as these maps are in C, so Ĥ = K̂.

Now we can begin the main business of this section. In view of Corollary 5.3, we may assume that the \overline{C}-objects of which we want to form the product are given by Σ-split pairs of maps between injectives. In fact this restriction will become redundant, as the argument below can be used first to show that all products are preserved, and then to construct products of non-injective pairs.

5.8. Lemma. Let (Y ⇉ Z) ∈ ob \overline{C} and W ∈ ob C. Then

Y × W[figure: u × W; ×  \underline{Ĵ× W}; v × W] Z × W

is also an object of \overline{C}. It is called (Y ⇉ Z) × W because, at least when U, V and W are injective, this is the product in \overline{C}. In the comprehension notation,

{Y | E} × W = {Y × W | E^{W} }^{}Ê^{W} ^{}Y × W.

This is functorial with respect to

g : W_{1} → W_{2}, where {Y | E} × g = Ê^{g}

(recall that id_{{Y | E}} = Ê) and to

F̂ : {Y_{1} | E_{1}} → {Y_{2} | E_{2}}, where F̂ × W = F̂^{W}.

Proof. Apply (−)^{W} to the equations in Definition 4.2 to get J^{W} ; Σ^{u×W} = id and

Σ^{v×W} ; J^{W} ; Σ^{u×W} = Σ^{v×W} ; J^{W} ; Σ^{v×W} .

Proposition 4.14 said that the formal pairs are equalisers, which property commutes with products. In comprehension notation, Σ^{v×W} ; J^{W} = E^{W}.

The formula for {Y | E} × g is merely naturality of Ê^{(−)}.

Using the injectivity of Y_{2}, we may write F̂ as

[figure: Y_{1}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; f; Y_{2}; {Y_{1} | E_{1}}; Ê_{1}; F̂; {Y_{2} | E_{2}}; Ê_{2}]

for some (not necessarily unique) f, where (by Definition 4.5) F̂ = F̂ ; Ê_{2} = Ê_{1} ; f, so F = Σ^{f} ; E_{1}. Applying (−) × W to the commutative square, the formula for F̂ × W has to be Ê_{1} ; (f × W) = Ĝ where G ≡ (Σ^{f} ; E_{1})^{W} = F^{W}.

5.9. Remark. Alternatively, one could show directly that Ê^{g} and F̂^{W} are morphisms, and that they satisfy the equations for the product functor. For F̂^{W}, we need to use the strength

(Σ^{2}Y) × W  \overline{σ_{Y,W} : G, w ↦ λθ. G(λy. θ(y, w)) ^{}}Σ^{2}(Y × W)
[figure: η_{Y} × W; η_{Y ×W}]
Y × W

for the monad, which is a natural transformation and obeys the equation shown.

5.10. Remark. The product of two Σ-split pairs must form a pullback (intersection) in \overline{C}, in the same way that the product of any two maps in a category gives rise to a pullback.

[figure: X_{1} × X_{2}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; X_{1} × Y_{2} = {Y_{1} × Y_{2} | E_{1}^{Y_{2}}}; {Y_{1} × Y_{2} | E_{2}^{Y_{1}}} = Y_{1} × X_{2}; . . . . . . . . . . . . . . . .; Y_{1} × Y_{2}]

Unfortunately, our “comprehension” notation does not admit intersections — either abstractly or in the leading example of LKLoc — so we still have to find an E on Y_{1} ×Y_{2} to describe the subspace. If E_{1}^{Y_{2}} and E_{2}^{Y_{1}} commute (as they do if E_{1} = Σ^{e_{1}} or E_{2} = Σ^{e_{2}}) then their composite encodes the intersection. But it turns out that, even if E_{1}^{Y_{2}};E_{2}^{Y_{1}} ≠ E_{2}^{Y_{1}};E_{1}^{Y_{2}}, either of them will do the job: of course products and pullbacks are unique up to isomorphism, but we have two representations of them.

5.11. Lemma. The composite

[figure: Y_{1} × Y_{2}; u_{1} × Y_{2}; v_{1} × Y_{2}; × \underline{Ĵ_{1} × Y_{2}}; Z_{1} × Y_{2}; Z_{1} × u_{2}; Z_{1} × v_{2}; × \underline{Z_{1} × Ĵ_{2}}; Z_{1} × Z_{2}]

is an object of \overline{C}, where

u = u_{1} × Y_{2} ; Z_{1} × u_{2} = Y_{1} × u_{2} ; u_{1} × Z_{2} = u_{1} × u_{2}
v = v_{1} × Y_{2} ; Z_{1} × v_{2} = Y_{1} × v_{2} ; v_{1} × Z_{2} = v_{1} × v_{2}
Ĵ = Z_{1} × Ĵ_{2} ; Ĵ_{1} × Y_{2} ≠ Ĵ_{1} × Z_{2} ; Y_{1} × Ĵ_{2}
Ê = v ; Ĵ = Y_{1} × Ê_{2} ; Ê_{1} × Y_{2} ⊂_{Y_{1}×Y_{2}} Y_{1} × Ê_{2}

the inclusion on the last line being in the sense of Notation 4.4.

Proof. Clearly u; Ĵ = id, whilst

Ê ≡ v ; Ĵ = v_{1} × Y_{2} ; Z_{1} × v_{2} ; Z_{1} × Ĵ_{2} ; Ĵ_{1} × Y_{2}  definitions of v and J
= v_{1} × Y_{2} ; Z_{1} × Ê_{2} ; Ĵ_{1} × Y_{2}  definition of E_{2}
= Y_{1} × Ê_{2} ; v_{1} × Y_{2} ; Ĵ_{1} × Y_{2}  v_{1} central
= Y_{1} × Ê_{2} ; Ê_{1} × Y_{2}.  definition of E_{1}.

Using the given equations of the form v_{i} ; Ĵ_{i} ; u_{i} = v_{i} ; Ĵ_{i} ; v_{i}, we must prove this equation for the new Σ-split pair:

v ; Ĵ; u = Y_{1} × Ê_{2} ; Ê_{1} × Y_{2} ; v_{1} × Y_{2} ; Z_{1} × v_{2}
= Y_{1} × (v_{2} ; Ĵ_{2} ; u_{2}) ; (v_{1} ; Ĵ_{1} ; u_{1}) × Z_{2}
= v ; Ĵ; v,

using centrality of u_{2}, and the same argument with v in place of u.

Y_{1} × Y_{2}  Y_{1} × Ê_{2} × Y_{1} × Y_{2}  \overline{Ê_{1} × Y_{2} ×} Y_{1} × Y_{2}
[figure: id]
[figure: Y_{1} × Z_{2}; Y_{1} × v_{2}; Y_{1} × u_{2}; \overline{Ê_{1} × Z_{2} ×}; Y_{1} × Z_{2}; Y_{1} × v_{2}; Y_{1} × u_{2}; \overline{Y_{1} × Ĵ_{2} ×}; Y_{1} × Y_{2}]

Finally, Y_{1} × Ê_{2} ; Ê_{1} × Y_{2} ; Y_{1} × Ê_{2} = Y_{1} × Ê_{2} ; Ê_{1} × Y_{2} by centrality of u_{2} and v_{2} with respect to Ê_{1}, and u_{2} ; Ĵ_{2} = id.

5.12. Proposition. The category \overline{C} has finite products, where

{Y_{1} | E_{1}} × {Y_{2} | E_{2}} = {Y_{1} × Y_{2} | E_{1}^{Y_{2}} ; E_{2}^{Y_{1}}},

whilst the product of the morphisms F̂_{1} : X′_{1} → X_{1} and F̂_{2} : X′_{2} → X_{2} is F̂_{1}^{Y′_{2}} ; F̂_{2}^{Y_{1}}. Moreover, the functor C → \overline{C} takes products in C to products in \overline{C}.

Proof. First consider the product of two objects X_{1}, X_{2} ∈ ob C, expressed in \overline{C} by means of their standard resolutions, so the products Σ^{2}X_{1} × Σ^{2}X_{2} etc. are preserved (Lemma 5.7). The formal product of the Σ-split pairs (Lemma 5.11) provides an equaliser in \overline{C} (Proposition 4.14), which is the required product, isomorphic to X_{1} × X_{2}, i.e. this is preserved.

The construction is then applicable to any two Σ-split pairs, so all binary products exist in \overline{C}. Functoriality follows from that in Lemma 5.8.

5.13. Remark. The abstract situation of idempotents ϵ = (E_{2})^{Y_{1}} and ϵ′ = (E_{1})^{Y_{2}} (in this case on the object Σ^{Y_{1}×Y_{2}}) such that ϵ; ϵ′ and ϵ′ ; ϵ are also idempotent is studied in [D, Lemma 7.1]. It is shown there that the splittings of ϵ; ϵ′ and ϵ′; ϵ are isomorphic and form a pushout diagram, in our case of the algebras Σ^{X_{1}×X_{2}} etc. corresponding to objects in the above pullback.

6. Structure in \overline{C}

Now that we have overcome the main difficulty concerning binary products, we are equipped to tackle exponentials, and then to show that \overline{C} does in fact have the monadic property for which it was designed. We still rely on injectivity, first re-casting Proposition 5.2 in terms of the double transpose of h.

6.1. Lemma. There is a natural bijection between \overline{C}-maps Ĥ : \{Y | E\} → Σ^{U} and C-maps p : U → Σ^{Y} such that p = p; E.

Proof. Let Ĥ ↦ p = η_{U} ; H, which satisfies p = p; E by Lemma 4.6. Conversely, let p ↦ Ĥ = Ê ; η_{Y} ; Σ^{p}, which is a composite of \overline{C}-maps \{Y | E\}^{}^{}Y ^{}Σ^{U}.

Then Ĥ ↦ Ê ; η_{Y} ; Σ^{p} = Ê ; η_{Y} ; Σ^{H} ; Σ^{η_{U}} = Ĥ ; η_{Σ^{U}} ; Σ^{η_{U}} = Ĥ by Definition 4.5 and the unit law. Conversely, p ↦ η_{U} ; H = η_{U} ; Σ^{2}p; Σ^{η_{Y}} ; E = p; η_{Σ^{Y}} ; Σ^{η_{Y}} ; E = p; E = p by naturality for η and the unit law.

For naturality, let F̂ : {Y′ | E′} → {Y | E} and g : U′ → U. Then p becomes g;p;F.

6.2. Proposition. \overline{C} has and C → \overline{C} preserves powers of Σ, where

Σ^{{Y | E}} = {Σ^{Y} | Σ^{E}} and ΣF̂ = F.
[figure: Y_{1} × Y_{2}; h; Σ; Y_{1}; k; Σ^{Y_{2}}]
[figure: Ĥ]
[figure: X_{1} × X_{2}; Ê_{1}^{Y_{2}} ; Ê_{2}^{Y_{1}}; X_{1}; Ê_{1}; K̂; Σ^{X_{2}}; E_{2}; E_{2}]

Proof. \overline{C}-maps Ĥ : X_{1} × X_{2} → Σ correspond bijectively to p : 1 → Σ^{Y_{1}×Y_{2}} in C such that p = p ; E_{1}^{Y_{2}} ; E_{2}^{Y_{1}}, by Lemma 6.1. By Remark 5.10, this is equivalent to p; E_{1}^{Y_{2}} = p = p; E_{2}^{Y_{1}}. Let k : Y_{1} → Σ^{Y_{2}} and q : Y_{2} → Σ^{Y_{1}} be the exponential transposes of p, which satisfy k = k; E_{2} and q = q; E_{1}. But then q corresponds to K̂ : X_{1} → Σ^{Y_{2}} by Lemma 6.1, and K̂ = K̂;E_{2} by the other equation, so it factors through Σ^{X_{2}}. Conversely, K̂ defines k, q, p and Ĥ in the same way.

Now let F̂_{1} : X′_{1} → X_{1} and F̂_{2} : X′_{2} → X_{2}, whose product is F̂_{1}^{X′_{2}} ; F̂_{2}^{X_{1}} by Proposition 5.12. Then by the naturality part of the Lemma, p becomes p ; F_{2}^{X_{1}} ; F_{1}^{X′_{2}} and K̂ becomes F̂_{1} ; K̂ ; F_{2}.

6.3. Lemma. η_{X} : X → Σ^{2}X in \overline{C} is given by Ê ; η_{Y} : Y −× Σ^{2}Y.

[figure: Y; η_{Y}; Σ^{2}Y; X = {Y | E}; Ê; η_{X}; Σ^{2}X; Σ^{E}; Σ^{E}]

Proof. From functoriality in the Proposition, Σ^{2} takes the inclusion Ê to Σ^{E}. Then for η to be natural on \overline{C}, we need η_{X} = Ê ; η_{Y} ; Σ^{E}. But this expression is the left hand side of the defining equation for the nucleus E (Definition 4.3), the right hand side being Ê ; η_{Y}.

Alternatively, we may see η_{{Y | E}} as the double transpose of id_{{Y | E}} = Ê. This correspondence is that between k and q on the right hand side of the Proposition, in the case of X_{1} = Σ^{X}, X_{2} = X. Then K̂ = id_{Σ^{X}} = E = k and q = η_{Y} ; Σ^{E}, so η_{{Y | E}} = Ê ; q = Ê ; η_{Y}.

6.4. Corollary. A\overline{C} ≃ A_{KSC} ≅ A_{KC}, cf. A_{SC} ≅ A_{C} in Lemma A 7.3.

Proof. Let (A, α) be an algebra over \overline{C}, with A = \{Y | E\}. Then A ◁ Σ^{2}A ◁ Σ^{2}Y, so A may as well be in KC, since this is fully embedded in \overline{C} by Corollary 4.13.

6.5. Lemma. H\overline{C}-maps Ĥ : X_{1} −× X_{2} are given by

H : Σ^{Y_{2}} → Σ^{Y_{1}} such that H ; E_{1} = H = E_{2} ; H.

So H\overline{C} ⊂ KHC is the full subcategory consisting of those objects (X, Ê) for which E is a nucleus.

[figure: Σ^{Y_{2}}; H; Σ^{Y_{1}}; Σ^{X_{2}}; E_{2}; E_{2}; Σ^{X_{1}}; E_{1}; E_{1}]

Proof. An H\overline{C}-map Ĥ : X_{1} −× X_{2} is a \overline{C}-map H : Σ^{X_{2}} → Σ^{X_{1}}. We have just shown that these exponentials are retracts, so this map is H : Σ^{Y_{2}} → Σ^{Y_{1}} (now just in C) such that E_{2} ;H = H = H;E_{1}. This is also how morphisms of KHC are defined (Remark 4.1).

6.6. Lemma. An H\overline{C}-map Ĥ : X_{1} −× X_{2} is first class (a \overline{C}-map) iff it respects naturality of η, i.e. η_{X_{1}} ; Σ^{2}Ĥ = Ĥ ; η_{X_{2}}, or H : Σ^{X_{2}} → Σ^{X_{1}} is a homomorphism.

Proof. Using the previous two lemmas,

η_{X_{1}} ; Σ^{2}Ĥ = Ê_{1} ; η_{Y_{1}} ; Σ^{2}Ĥ and Ĥ ; η_{X_{2}} = Ĥ ; Ê_{2} ; η_{Y_{2}} = Ĥ ; η_{Y_{2}}.

Equality of these is the second equation in Definition 4.5.

6.7. Corollary. Every homomorphism K̂ : Σ^{X_{2}} → Σ^{X_{1}} in \overline{C} is of the form K̂ = ΣĤ for some unique \overline{C}-map Ĥ : X_{1} → X_{2}. From Section A 7 we deduce that all objects of \overline{C} are sober, that S\overline{C} ≅ \overline{C} and that X × (−) distributes over such colimits as exist in \overline{C}.

6.8. Notation. Recall from Definition A 6.3 that we wrote force : Σ^{2}X −× X for the HC-map η̂_{Σ^{X}}, and that this is natural with respect to HC-maps Ĥ : X −× Y. Similarly, we now write

admit for Î: Y −× {Y | E}.

Like the identity, the inclusion i : (Y ⇉ Z) ↪ Y and its splitting Î are both encoded as Ê. In Section 8 we shall add an operator admit to the λ-calculus, just as we introduced focus in Section A 8, and they both have side-conditions. However, we shall not on this occasion give different names to the operator in \overline{C} and the map in HC.

6.9. Lemma. force_{{Y | E}} = Σ^{2}i; force_{Y} ; admit.

Σ^{2}\{Y | E\}[figure: Σ^{2}i; \underline{Σ^{2} admit}] Σ^{2}Y

[figure: \{Y | E\}; η_{\{Y | E\}}; \begin{matrix}force & \{Y | E\} \\ × \end{matrix}; i; ×  \underline{admit}; Y; η_{Y}; \begin{matrix}force & Y \\ × \end{matrix}]

Hence if Γ ⊢ P : Σ^{2}{Y | E} is prime then so is Γ ⊢ Σ^{2}i P : Σ^{2}Y (Lemma A 4.6) and

focus_{{Y | E}} P = admit ( focus_{Y} (Σ^{2}i P)).

Proof. The diagram shows naturality of force with respect to admit in H\overline{C}, i.e. of η with respect to E in C. Recall from Lemma A 4.3 that P is prime iff it has equal composites with Σ^{2}η_{(−)} and ηΣ^{2}(−), which are natural with respect to i : {Y | E}^{}^{}Y.

Now we can show that \overline{C} has the new structure that it was introduced to provide.

6.10. Proposition. Σ-split equalisers exist in \overline{C}, and Σ^{(−)} sends them to coequalisers. Indeed

{{Y | E_{1}} | E_{2}} = {Y | E_{2}}

where X = \{Y | E_{1}\} is a \overline{C}-object and E_{2} data on it for a \overline{\overline{C}}-object \{X | E_{2}\}.

Proof. The defining equations for Ê_{2} to be an H\overline{C}-map and to be a nucleus (Definition 4.3), i.e. to define an \overline{\overline{C}}-object, are

Ê_{1} ; Ê_{2} = Ê_{2} = Ê_{2} ; Ê_{1} and Ê_{2} ; η_{X} ; Σ^{E_{2}} = Ê_{2} ; η_{X},

the first of which says that Ê_{2} ⊂ Ê_{1} in the sense of Notation 4.4. The second equation, between H\overline{C}-maps, reduces to

Ê_{2} ; η_{Y} ; Σ^{E_{2}} = Ê_{2} ; η_{Y}

in HC, but this is just the definition of a nucleus E_{2} on Y. Hence \{Y | E_{2}\} as a \overline{C}-object, which Lemma 4.12 expresses as the equaliser of a Σ-split pair Y ⇉ Σ^{2}Y:

[figure: {Y | E_{2}}; ×; X = {Y | E_{1}}; ×; Y; ×; Σ^{2}Y]

Finally, Σ^{(−)} acts on this diagram in \overline{C} just as it does in C, taking it to a split coequaliser, as in Proposition 4.14.

6.11. Corollary. (\overline{C}, Σ) is monadic and \overline{C} ≃ A_{KC}^{op}.

Proof. Recall that being monadic means that \overline{C} ≃ Aop ; \overline{C}. By Theorem 3.3, this happens iff all objects are sober (which they are by Corollary 6.7) and all algebras are spatial. The latter follows from the previous result by Proposition 3.8. Finally, the equivalence with A_{KC}^{op} is given by Corollary 6.4.

6.12. Theorem. (\overline{C}, Σ) is the (Karoubi and) monadic completion of (C, Σ):

Let (D, Σ_{D}) be monadic and suppose that idempotents split in D (so D has products, powers of Σ_{D}, equalisers of Σ_{D}-split pairs and Σ_{D}^{(−)} sends them to coequalisers.) Let F : C → D be a functor that preserves products and powers of Σ. Then there is a functor \overline{F} : \overline{C} → D that also preserves these things and makes the square commute, and it is unique up to equivalence.

[figure: \overline{C}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; \overline{F}; \overline{D}; C; F; D; ‖]

Proof. Any object of \overline{C} is interpreted as a Σ-split equaliser diagram in C as in Proposition 4.14. Such diagrams are preserved by the functor F, but the diagram in D has an equaliser, which is the required image of the given C-object. F commutes with the representation of × and Σ^{(−)} in Propositions 5.12 and 6.2.

6.13. Remark. The sober, Karoubi and monadic completions are related by the diagram

[figure: A_{C}^{op}; = = = = = = =; A_{SC}^{op}; A_{KC}^{op}; = = = = = = =; Aop ; \overline{C}; = = = = = = = =; \overline{\overline{C}}]

[figure: SC; SKC; KSC; = = = = = =; SKSC; \overline{C}; ‖]

[figure: C; KC]

in which^{}^{}denotes a full inclusion and = an equivalence. We leave the interested reader to find a properly general recursive idempotent on ℕ (so SKC ≠ KSC, cf. Remark A 9.12), and to show that any retract of a sober object is sober (so KSC = SKSC).

The development so far has been entirely set in the abstract situation of a category C with an exponentiating object Σ, for which all objects are sober. In the intended applications to topology and computation, Σ is a distributive lattice and satisfies the Euclidean principle [C]; this structure is preserved by the inclusion C → \overline{C} since it preserves products and powers of Σ.

We also want C to have a natural numbers object ℕ, i.e. to admit primitive recursion at all C-types, although sobriety of ℕ means that general recursion is also defined (Sections A 9–10). The extension of recursion to \overline{C}-types follows essentially the same argument as in Proposition 4.15 for colimits.

6.14. Proposition. The inclusion C → \overline{C} preserves ℕ.

Proof. The recursion data in the fully parametrised version of this result consist of

z : Γ → {Y | E} and s : Γ × ℕ × {Y | E} → {Y | E},

and we shall prove it symbolically like this in Lemma 8.14. Here, for brevity, we omit the parameters in s.

First, {Y | E} may be expressed as an equaliser as shown.

Γ

[figure: 0]
[figure: ℕ; .; .; .; .; .; .; .; .; .; .; .; .; .; .; {Y | E}; z; Σ^{2}Y; Σ^{4}Y]

[figure: ℕ; +1; .; .; .; .; .; .; .; .; .; .; .; .; .; .; {Y | E}; s; Σ^{2}Y; S; Σ^{4}Y]

Then use injectivity to extend s : {Y | E} → {Y | E} to endofunctions of Σ^{2}Y and Σ^{4}Y, so that s becomes a mediator between equalisers. Then recursion in C defines a map ℕ → Σ^{2}Y that makes the squares commute and also has equal composites to Σ^{4}Y. Finally, the required map ℕ → {Y | E} mediates to the equaliser.

7. Algebras

A perhaps more obvious way to construct the monadic completion of C (as I did in 1993) is to consider the algebras, and in fact \overline{C} ≃ A_{KC}^{op} does the job. As in other approaches, the central difficulty remains that of binary products in \overline{C}, i.e. coproducts of algebras. For convenience, we assume in this section alone that idempotents split in C, so KC ≃ C.

The equivalence \overline{C} ≃ A^{op} says that every algebra (A, α) is to be (Σ^{X}, Σ^{η_{X}}) for some new object X ∈ ob \overline{C} (Definition 3.1). This means that we have to prove properties of A on the basis of its algebra structure that would be obvious if we already knew that A = Σ^{X}. The key such property turns out to be the double exponential transposition,

A(Σ^{A}, B) = \overline{C}(Y, Σ^{X}) ≅ \overline{C}(X, Σ^{Y}) = A(Σ^{B}, A),

where X and Y are the \overline{C}-objects corresponding to the algebras A and B, and Σ^{X} corresponds to Σ^{A} because the functor C → \overline{C} is supposed to preserve Σ^{(−)}.

In effect, using algebras means that we insist on representing each \overline{C}-object in “normal form” by means of its standard resolution

[figure: X; η_{X}; ×  \underline{η̂_{Σ^{X}}}; Σ^{2}X; η_{Σ^{2}X}; Σ^{2}η_{X}; × \underline{η_{Σ^{3}X}}; Σ^{4}X]

[figure: A; \underline{α}; η_{A}; Σ^{2}A; \underline{μ_{A} = Σ^{η_{Σ^{A}}}}; \underline{Σ^{2}α}; η_{Σ^{2}A}; Σ^{4}A,]

whereas Section 4 was much more flexible about Σ-split pairs. For example, Lemma 5.8 gave the obvious formula for (Y ⇉ Z) × W, but this does not take standard resolutions to standard resolutions: the structure map α^{W} that it provides must be composed with a map

Σ^{τ^{Σ^{X},W}} : ΣΣ^{Σ^{(X×W)}} ^{}Σ(Σ^{Σ^{X}} × W).

When we generalise from Σ^{X} to A, we must replace Σ^{X×W} by A^{W}.

7.1. Remark. For any algebra (A, α) and object W, the object A^{W} splits the idempotent E^{W}, where A itself splits E = α ; η_{A}. Then A^{W} carries a power algebra structure, Σ^{τ_{A,W}} ; α^{W}, where the natural transformation

τ_{A,W} : W × Σ^{A} → Σ^{A^{W}} by x, ϕ ↦ λf. ϕ(fx)

plays a similar role to that of the strength σ of the monad (Remark 5.9). If H : A → B is a homomorphism them so is H^{W} : A^{W} → B^{W}, by naturality of τ_{(−),W}.

In fact, for any strong monad T whose algebras are exponentiable, an algebra structure T (A^{W}) → A^{W} is given by the transpose of

[figure: W × T (A^{W}); σ_{W,A^{W}}; T (W × A^{W}); T ev; T A; α; A.]

7.2. Remark. When X and Y are expressed by means of the standard resolution, the pullback in Remark 5.10 is as shown on the left. As Σ^{X×Σ^{2}Y} = (Σ^{X})^{(Σ^{2}Y)} = A^{Σ^{B}}, the corresponding diagram in A is the one on the right, and is to be a pushout of homomorphisms.

[figure: X × Y; X × η_{Y}; X × Σ^{2}Y; A ⊗ B; A^{Σ^{B}}]

[figure: Σ^{2}X × Y; η_{X} × Y; Σ^{2}X × η_{Y}; Σ^{2}X × Σ^{2}Y; η_{X} × Σ^{2}Y; B^{Σ^{A}}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; (η_{B})^{(Σ^{A})}; .; .; .; .; .; .; .; .; .; .; .; .; .; \underline{β^{(Σ^{A})}}; Σ^{Σ^{A}×Σ^{B}}; (η_{A})^{(Σ^{B})}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; α^{(Σ^{B})}]

As often happens when we consider algebras, the homomorphisms on the bottom and right are split by functions, the two idempotents in Remark 5.10 being E_{1}^{Σ^{B}} and E_{2}^{Σ^{A}}, where E_{1} = α; η_{A} and E_{2} = β ; η_{B}. When we construct the pushout, we shall find that the other two maps are also split, with the result that the pushout of functions, like the coequalisers that we have used, is absolute. In particular, Σ^{2}(A ⊗ B) is also a pushout, enabling us to define the algebra structure Σ^{2}(A ⊗ B) → (A ⊗ B).

(The reason for using the symbol ⊗ for the coproduct of algebras is simply that the corresponding construction in locale theory is a tensor product of the underlying join semilattices.)

That is the plan for the later parts of the construction, but it also provides the idea for the central technical result. The composite B^{Σ^{A}} → Σ^{Σ^{A}×Σ^{B}} → A^{Σ^{B}} takes G to λψ. α(λϕ. ψ(Gϕ)). We now make use of the corresponding external transformation. For A = Σ^{X} and B = Σ^{Y}, this is just the double exponential transposition C(Σ^{Σ^{X}}, Σ^{Y}) ≅ C(Σ^{Σ^{Y}} , Σ^{X}).

7.3. Lemma. G ↦ Σ^{G} ; α and F ↦ Σ^{F} ; β restrict to a bijection A(Σ^{A}, B) ≅ A(Σ^{B}, A) that’s natural with respect to homomorphisms.

C(Σ^{B}, A)  C(Σ^{A}, B)

[figure]

[figure: A(Σ^{B}, A); ≅; A(Σ^{A}, B)]

Proof. Whatever G is, F = Σ^{G} ; α is a homomorphism, being a composite of two homomorphisms. If G is itself a homomorphism then Σ^{F} ; β = Σ^{α}; Σ^{Σ^{G}}; β = Σ^{η_{B}} ; G = G. Given homomorphisms u : A → A′ and v : B → B′, the correspondence takes Σ^{v} ; F ; u to Σ^{u} ; G; v.

7.4. Remark. We can define an internal notion of “object of homomorphisms” (which should also have its own notation) by interpreting the external Eilenberg–Moore equation as the equaliser

[figure: A((C, γ), (B, β)); B^{C}; γ ; (−); Σ^{2}(−) ; β; B^{Σ^{2}C}]

or by a generalisation of the equaliser in Proposition 3.2 with B in place of Σ.

The argument in the Lemma internalises, to show that A(Σ^{A}, B) is a split equaliser (retract) of B^{Σ^{A}}. Moreover, it is isomorphic in C to A(Σ^{B}, A), and we write A ⊗ B for either of them. The same argument shows that A⊗B is an absolute pushout in C, whence it carries a unique algebra structure that makes it a pushout of algebras.

From the external result we can deduce Lemma 5.7, that C → \overline{C} preserves products of injectives (actually, just carriers of algebras, but that’s no handicap).

7.5. Lemma. If C, D ∈ ob C are carriers of algebras then

[figure: Σ^{C}; Σ^{π_{0}}; Σ^{C×D}; Σ^{π_{1}}; Σ^{D}]

is a coproduct diagram of algebras.

Proof. For any other algebra Θ (playing the role of Σ^{Γ} in Section 5),

A(Σ^{C}, Θ) × A(Σ^{D}, Θ) ≅ A(Σ^{Θ}, C) × A(Σ^{Θ}, D) ≅ A(Σ^{Θ}, C × D) ≅ A(Σ^{C×D}, Θ)

using Lemma 7.3 three times. Lemma 5.5 gave the algebra structure on C × D.

7.6. Corollary. The algebra Σ^{Σ^{A}×Σ^{B}} has the universal property that

C(A, Θ) × C(B, Θ) ≅ A(Σ^{Σ^{A}×Σ^{B}}, Θ).

Proof. Put C = Σ^{A} and D = Σ^{B} and recall that C(A, Θ) ≅ A(Σ^{Σ^{A}}, Θ).

Next we prove that the power algebra does the job for which it was introduced in Remark 7.1. Here A and D play the roles of Σ^{{Y | E}} and W in Lemma 5.8

7.7. Lemma. For algebras A and D, the diagram A ^{}A^{D} ^{}Σ^{D} is a coproduct of algebras.

A ^{...................................^{}}A^{D}

[figure]

[figure: Σ^{2}A; α; Σ^{π_{0}}; Σ^{(Σ^{A}×D)}; α^{D}; Σ^{π_{1}}; Σ^{D}]
[figure: Σ^{π_{1}}]
[figure: Σ^{4}A; Σ^{Σ^{α}}; Σ^{η_{ΣA}}; Σ^{π_{0}}; Σ^{(Σ^{3}A×D)}; Σ^{Σ^{α}×D}; Σ^{η_{ΣA}×D}]

Proof. The left-hand column is a U-split coequaliser of algebras, i.e. an absolute coequaliser in C, which the functor (−)^{D} therefore preserves. So the middle column is a coequaliser of (power) algebras, in which the middle and bottom objects are coproducts by Lemma 7.5. But the universal properties of coproducts and coequalisers commute, cf. products and equalisers in Lemma 5.8.

7.8. Corollary. The algebra A^{Σ^{B}} has the universal property that

A(A, Θ) × C(B, Θ) ≅ A(A^{Σ^{B}}, Θ).

7.9. Theorem. A ⊗ B carries the structure of the coproduct of the algebras A and B.

Proof. By Remark 7.2, A ⊗ B is an absolute pushout of the diagram in C, so there is a unique algebra structure on it that makes this diagram a pushout in A.

Hence we have isomorphic pullbacks in Set,

[figure: A(A, Θ) × A(B, Θ); A(A, Θ) × C(B, Θ); A(A ⊗ B, Θ); A(A^{Σ^{B}}, Θ)]

[figure: C(A, Θ) × A(B, Θ); C(A, Θ) × C(B, Θ); A(B^{Σ^{A}}, Θ); A(Σ^{Σ^{A}×Σ^{B}}, Θ)]

or, in plain English, if the functions A → Θ and B → Θ are actually both homomorphisms then they correspond to a homomorphism from A ⊗ B. Therefore this has the universal property of the coproduct.

7.10. Example. Recall that any idempotent defines a partition and chooses an element from each equivalence class. In this case the two partitions are the same but the choices of elements are different. For example in the simplest case, A = B = 1, the two representations are embedded as the singletons {⌜π_{0}⌝} and {⌜π_{1}⌝} in Σ^{Σ^{2}}.

[figure: 0 × 0; 0 × Σ; 1; 1; F; Σ × 0; Σ × Σ; 1; ⌜π_{1}⌝; Σ^{Σ×Σ}; ⌜π_{0}⌝; λϕψ. ϕ(F ψ)]

7.11. Proposition. Powers of \overline{Σ} (as we write it) in \overline{C} ≡ A^{op} are given by

\overline{Σ}^{(A,α)} = (Σ^{A}, Σ^{η_{A}}) and η̄_{(A,α)} = α, where \overline{Σ} = (Σ^{Σ}, Σ^{η_{1}}).

Proof. Since A ⊗ B was defined to have A(Σ^{A}, B) as its set of global elements,

\overline{C}(Γ × X, Σ) = A(Σ^{Σ}, A ⊗ B) = C(1, A ⊗ B) = A(Σ^{A}, B) = \overline{C}(Γ, Σ^{X})

where A = Σ^{Γ} and B = Σ^{X}.

7.12. Remark. For the other structure in terms of algebras,

(a) the terminal object is (Σ, Σ^{η_{1}});

(b) the natural numbers object is Σ^{ℕ};

(c) \overline{\overline{C}} ≅ \overline{C} because A\overline{C} ≅ A_{C}. The last part says that \overline{C} = A^{op} is monadic, and therefore admits subspaces as described in Sections 3 and 6, since we assumed that idempotents split in C.

8. Comprehension

Now we develop a λ-calculus for \overline{C}, just as Section A 8 did for SC.

The new calculus is based on a type-theoretic presentation [Tay99, Section 2.2] of Zermelo’s original set theory, with Σ^{X} playing the role of the powerset (PX) and the object {X | E} from Section 4 that of comprehension. Whereas comprehension is often presented in a way that allows each term to belong to many types, the new operators admit, i and I in our calculus, whilst perhaps being a little bureaucratic, ensure that each term has a unique type.

Writing D for the category obtained from the new calculus as explained in [Tay99, Sections 4.3 & 4.7] and more briefly in Remark A 2.7, we shall show in the following sections that \overline{C} ≃ D. This will be done by means of a weak normalisation theorem, thereby showing that we have stated enough equations. It is a categorical equivalence, rather than the isomorphism that we had for SC, because we’re now manipulating types.

8.1. Remark. In the calculus that we have in mind for set theory, the rules for the powerset PX ≡ Ω^{X} are those of the restricted λ-calculus, where ξ[a] means a ∈ {X | ξ}. Then comprehension has formation and introduction rules,

X type ⊢ ξ : PX
{X | ξ} type

Γ ⊢ a : X Γ ⊢ ξ[a]
Γ ⊢ admit a : {X | ξ}

elimination rules,

x : {X | ξ} ⊢ i_{X,ξ}x : X x : {X | ξ} ⊢ ξ[i_{X,ξ}x]

and β and η-rules

Γ ⊢ a : X  Γ ⊢ ξ[a] Γ ⊢ a = i_{X,ξ}(admit a) : X  x : {X | ξ} ⊢ x = admit(i_{X,ξ}x).

The intent of these rules is to specify when there is a term admit a that makes the triangle commute:

Γ

[figure: ...............; admit a; a]
{X | ξ}[figure: i_{X,ξ}] X

Notice that we have required ξ : PX to be a closed term (defined in the empty context), because we do not want to get involved in dependent types in this paper.

8.2. Remark. The rules that we give below for our own monadic situation are not very pretty if seen as a piece of pure λ-calculus. But they are in the spirit of the treatment of comprehension above, so long as we read the the type-formation rule as

X type  subtype data on X

{X | subtype data} type

where any predicate ξ : PX provides subtype data in set theory, and the nucleus E (Definition 4.3) does so for our own calculus. Similarly, the introduction rule means

Γ ⊢ a : X Γ ⊢ a is admissible to the subtype

Γ ⊢ admit a : {X | subtype data}

where our admissibility condition is unfortunately more complicated and less intuitive than that in set theory.

You may think of

{X | E} as {x : X | ∀ϕ:Σ^{X}. Eϕx =_{Σ} ϕx},

but this can only be internalised if Σ^{X} is compact (so ∀ϕ : Σ^{X} is meaningful) and Σ is discrete (so =_{Σ} is defined). These conditions (along with what is needed in Example 2.6(a) to define I_{X,E}θ in terms of ∃) would make \overline{C} into a topos (Theorem C 11.12), and thereby bring the comprehension calculus back to that for Zermelo type theory.

8.3. Remark. As we have learned throughout this paper, we need to be explicit about the subspace topology. The elimination rule for elements ({}E_{0}) below provides the restriction of an open subset ϕ of X to the subspace {X | E}, which we may re-interpret as the introduction rule for predicates,

Γ ⊢ ϕ : Σ^{X}
Σ^{{}}I
Γ ⊢ Σ^{i}ϕ ≡ λx. ϕ(i_{X,E}x) : Σ^{{X | E}}

For the corresponding elimination rule, we need a new operator I_{X,E} to expand an open subset θ of the subspace to the whole space.

Γ × {X | E}[figure: Γ × i_{X,E}] Γ × X
[figure: θ; ...............; I_{X,E}θ]

Σ

For reference, we repeat Definitions A 2.1, A 8.1, A 8.2 and 4.3.

SUBSPACES IN ABSTRACT STONE DUALITY  343

8.4. Definition. The restricted λ-calculus has just the type-formation rules

1 type

X_{1} type … X_{k} type
Σ^{(−)}F
Σ^{X_{1}×···×X_{k}} type

but with the normal rules for λ-abstraction and application,

Γ, x : X ⊢ σ : Σ^{Y} ; Σ^{(−)}I ; Γ ⊢ λx:X. σ : Σ^{X×Y}  Γ ⊢ ϕ : Σ^{X×Y} Γ ⊢ a : X ; Σ^{(−)}E ; Γ ⊢ ϕ[a] : Σ^{Y}

together with the usual α, β and η rules. 8.5. Definition. Γ ⊢ P : Σ^{Σ^{X}} is prime if Γ, F : Σ^{3}X ⊢ FP = P (λx. F(λϕ. ϕx)). 8.6. Definition. The sober λ-calculus has the additional rules

Γ ⊢ P : Σ^{Σ^{X}} P is prime

Γ ⊢ focus P : X

focus I
Γ ⊢ P : Σ^{Σ^{X}} P is prime
Γ, ϕ : Σ^{X} ⊢ ϕ(focus P) = P ϕ : Σ

focus β
{Γ ⊢ a, b : X  Γ, ϕ : Σ^{X} ⊢ ϕa = ϕb \atop Γ ⊢ a = b}  T_{0}

8.7. Definition. ϕ : Σ^{Y} ⊢ Eϕ : Σ^{Y} is called a nucleus if

F : Σ^{3}Y ⊢ E(λy. F(λϕ. Eϕy)) = E(λy. F(λϕ. ϕy)).

8.8. Definition. The {}-rules of the monadic λ-calculus define the subspace itself.

X type x : X, ϕ : Σ^{X} ⊢ Eϕx : Σ E is a nucleus

{X | E} type

{}F

Γ ⊢ a : X Γ, ϕ : Σ^{X} ⊢ ϕa = Eϕa
Γ ⊢ admit_{X,E} a : {X | E}

{}I

x : {X | E} ⊢ i_{X,E}x : X  {}E_{0}
x : {X | E}, ϕ : Σ^{X} ⊢ ϕ(i_{X,E}x) = Eϕ(i_{X,E}x)  {}E_{1}
Γ ⊢ a : X Γ, ϕ : Σ^{X} ⊢ ϕa = Eϕa
Γ ⊢ a = i_{X,E}(admit_{X,E} a) : X

{}β

x : {X | E} ⊢ x = admit_{X,E}(i_{X,E}x)  {}η

8.9. Definition. The Σ^{{}}-rules say that it has the subspace topology, where I_{X,E} expands open subsets of the subspace to the whole space.

θ : Σ^{{X | E}} ⊢ I_{X,E}θ : Σ^{X}  Σ^{{}}E

The β-rule says that the composite Σ^{X} [figure] Σ^{{X | E}}^{}^{}Σ^{X} is E:

ϕ : Σ^{X} ⊢ I_{X,E}(λx:{X | E}. ϕ(i_{X,E}x)) = Eϕ  Σ^{{}}β

Notice that this is the only rule that introduces E into the λ-expressions. The η-rule, which we first saw in Remark 2.8, says that the other composite Σ^{{X | E}}^{}^{}Σ^{X} [figure] Σ^{{X | E}} is the identity:

θ : Σ^{{X | E}}, x : {X | E} ⊢ θx = I_{X,E}θ(i_{X,E}x)  Σ^{{}}η.

In any type theory where terms are embedded in the definitions of types, we must check that, when two terms are equal according to the rules of the calculus, they give rise to interchangeable types. This result has the flavour of the normalisation proof that follows (Proposition 9.11), whilst being a lot simpler, so you may find it helpful to fill in the details of the verifications as a preparatory exercise.

8.10. Lemma. If E_{1} = E_{2} then there is an isomorphism {X | E_{1}} ≅ {X | E_{2}} that commutes with the structure (admit, i and I).

Proof. The isomorphism for values is x_{1} ↦ admit_{2}(i_{1}x_{1}) and vice versa. This is well formed, i.e. the side condition for {}I is satisfied and justifies the use of admit_{2}, because of the equation E_{1} = E_{2}. The isomorphism for properties is θ_{1} ↦ Σ^{i_{2}}(I_{1}θ_{1}). The equations for the isomorphisms and commutativity with the structure follow easily from the β- and η-rules for the two sides.

Before embarking on the main normalisation theorem, we investigate some of the interactions between the new admit operation and the underlying sober and recursive structures. The first result is the symbolic analogue of Remark 4.11, showing that admit does the same for a general Σ-split inclusion as focus does for η.

8.11. Lemma. The standard resolution defines an isomorphism

X [figure: admit ·η_{X}; ≅; \underline{focus ·i}] \{Σ^{2}X | E\} where E = η_{Σ^{X}} · Σ^{η_{X}}.

Proof. The term x : X ⊢ admit(λϕ. ϕx) is well formed because of the unit law. The right hand side of Definition 8.5 is EFP, so the subspace {Σ^{2}X | E} exactly captures the primes and

P : {Σ^{2}X | E} ⊢ focus(iP) : X

is well formed. Then focus (i(admit(λϕ. ϕx))) = focus(λϕ. ϕx) = x by {}β and focus η. Conversely, admit (η_{X}(focus(iP))) = admit(iP) = P by focus β and {}η.

The interaction between admit and substitution, i.e. cut elimination, is as expected, cf. Lemma A 8.4.

8.12. Lemma. Let Γ ⊢ admit_{X,E} a : {X | E} be a well formed term and u : Δ → Γ a substitution [Tay99, Section 4.3]. Then Δ ⊢ admit_{X,E} u^{∗}a : {X | E} is also well formed, and

Δ ⊢ u^{∗}(admit_{X,E} a) = admit_{X,E}(u^{∗}a).

Proof. In the context [Δ, ϕ : Σ^{X}], since E and ϕ do not depend on Γ,

ϕ(u^{∗}a) ≡ u^{∗}(ϕa) = u^{∗}(Eϕa) ≡ Eϕ(u^{∗}a).

This is consistent with the {}β- and η-rules when we put u^{∗}(i_{X,E}a) = i_{X,E}(u^{∗}a), and with the Σ^{{}}-rules since u^{∗}(I_{X,E}θ) = I_{X,E}(u^{∗}θ).

Much of the business of Section A 8, which introduced the focus operation to handle sobriety, was to eliminate it. In particular, Proposition A 8.10 showed that focus is redundant for logical terms (i.e. of type Σ^{U}), whilst Sections A 9–10 replaced it with descriptions for numerical terms (i.e. of type ℕ). The following result adds a new case to that reduction, for terms of type {Y | E}, so focus can still be pushed to the outside of any term of the comprehension calculus, or eliminated altogether.

8.13. Lemma. If Γ ⊢ P : Σ^{2}{Y | E} is prime then

focus_{{Y | E}} P = admit_{Y,E} ( focus_{Y} (Σ^{2}i_{Y,E}P)).

So {Y | E} is sober, cf. Lemma 6.9.

Proof. Since Γ ⊢ Σ^{2}iP : Σ^{2}Y is also prime (Lemma A 4.6), we may form

Γ ⊢ a ≡ focus_{Y} (Σ^{2}iP) : Y,

which satisfies

ϕa = ϕ( focus_{Y} (Σ^{2}iP))
= Σ^{2}iP ϕ  focus β
= P (Σ^{i}ϕ) = P (λy. ϕ(iy))  definition of Σ^{2}i
= P (λy. Eϕ(iy))  {}E_{1}
= Eϕa  in the same way,

so we may then form Γ ⊢ admit_{Y,E} ( focus_{Y} (Σ^{2}iP)). Applying θ : Σ^{{X | E}},

θ( admit ( focus_{Y} (Σ^{2}iP)))
= Iθ( focus_{Y} (Σ^{2}iP))  {}β, Σ^{{}}η
= Σ^{2}iP (Iθ)  focus β
= P (Σ^{i}(Iθ)) = P θ  Σ^{{}}η
= θ(focus_{{Y | E}} P)  focus β,

whence the result follows by T_{0}.

Finally, admit can also be moved to the outside of the term, although that is in fact the normalisation theorem to which the next two sections are devoted. Here we just consider the interaction with recursion, which is the symbolic analogue of Proposition 6.14.

8.14. Lemma. Let X = {Y | E} with terms

Γ ⊢ n : ℕ,  Γ ⊢ z : Y  and  Γ, m : ℕ, y : Y ⊢ s(m, y) : Y

such that Γ ⊢ admit z : X and Γ, m : ℕ, x : X ⊢ admit s(m, ix) : X are well formed. Then

Γ ⊢ rec(n, admit z, λmx. admit s(m, ix)) = admit rec(n, z, λmy. s(m, y)) : X,

omitting the subscripts on i_{Y,E} and admit_{Y,E}.

Proof. Using the {}β- and η-rules, the claim is equivalent to

Γ ⊢ i rec(n, admit z, λmx. admit s(m, ix)) = rec(n, z, λmy. s(m, y)) : Y

and is valid for n = 0. In order to use the rec η-rule to prove the claim, we have to check the same equation as for the induction step in an ordinary proof by induction, namely

i rec(n + 1, admit z, λmx. admit s(m, ix))  recursion step
= i admit s(n, i rec(n, admit z, λmx. admit s(m, ix)))
= i admit s(n, rec(n, z, λmy. s(m, y)))  induction hypothesis
= s(n, rec(n, z, λmy. s(m, y)))  {}β
= rec(n + 1, z, λmy. s(m, y)).  recursion step.

9. Normalisation for types

This section shows how each new type (generated arbitrarily from comprehension and powers of products) may be expressed as a subtype (by a single comprehension) of a type in the original calculus. This is like expressing any set in Zermelo set theory as a subset of an iterated powerset, as in the von Neumann hierarchy. It will relate back to the categorical construction in Section 4, where every new object of \overline{C} is a formal equaliser in C.

The structure maps in this isomorphism are, of course, terms to be defined, but they behave like the constructors i, I and admit of the comprehension calculus. That is, the lemmas that we have to prove towards this isomorphism are like the β- and η-rules of the calculus, and will therefore be presented and named as such. This is not a serious overloading of the i and I notations, as the old use has two subscripts.

9.1. Remark. Given any λ-calculus (such as ours) with all of the usual structural rules, the corresponding category has products simply because they are concatenations of contexts. The problem with products that was a central concern in the two categorical constructions does not, unfortunately, go away so easily: we have merely pushed it into the exponents.

A power type is Σ^{(−)} applied to (the product of) a list of types, and λ-abstraction and application involve the list operations of push and pop (or cons and (head,tail)) on types. The normalisation process for types must therefore also deal with lists. This could be formalised by introducing meta-variables to denote either lists of types, or powers of lists. However, as this complication does not have any impact on the real issues in the argument, we leave the interested reader to carry this through for themselves, and simply consider the case of lists of length two. We take Σ^{Y ×Z} to mean (Σ^{Z})^{Y}, a typical term of which is λy. ϕ, where y : Y and ϕ : Σ^{Z}. In this sense, Σ contains the empty list.

The main technical question with products then manifests itself in this situation as the choice between I \overline{Y} ; Z · I_{Y}^{Z} and the other term that could serve as i_{Σ^{Y ×Z}}.

Extended notation

9.2. Notation. By structural recursion on the type X, we define a type \overline{X}, terms

[figure: X; i_{X}; × \underline{admit_{X}}; \overline{X}; Σ^{X}; I_{X}; \underline{Σ^{i_{X}}}; Σ^{\overline{X}}]

and the idempotent E_{X} on Σ^{\overline{X}}. The base cases are 1, Σ and ℕ, for which these maps are identities.

X  Σ^{Y ×Z}  {Y | E}
\overline{X}  Σ^{\overline{Y} × \overline{Z}}  \overline{Y}
i_{X}  Σ^{Y ×Z}^{}I_{Y}^{Z} ^{}Σ^{\overline{Y} ×Z}^{}I \overline{Y} ; Z ^{}Σ^{\overline{Y} × \overline{Z}}  \{Y | E\}^{}i_{Y,E}^{}Y^{}i_{Y} ^{}\overline{Y}
admit_{X}  Σ^{\overline{Y} × \overline{Z}}  Σ^{i_{Y} ×i_{Z}} [figure] Σ^{Y ×Z}  \overline{Y} ^{admit_{Y}}× Y ^{admit_{Y,E}}× \{Y | E\}
I_{X}  Σ^{2}(Y × Z)^{}Σ^{2}(i_{Y} × i_{Z})^{}Σ^{2}( \overline{Y} × \overline{Z}) Σ^{\{Y | E\}}^{}I_{Y,E}^{}Σ^{Y}^{}I_{Y} ^{}Σ^{\overline{Y}}
E_{X} Σ^{2}( \overline{Y} × \overline{Z}) Σ(E \overline{Y} ; Z · E \overline{Z} ; Y)^{}Σ^{2}( \overline{Y} × \overline{Z}) Σ^{\overline{Y}} Σ^{i_{Y}} [figure] Σ^{Y} E^{}Σ^{Y}^{}I_{Y}^{}Σ^{\overline{Y}}

So \overline{X} erases the comprehensions from X, and i_{X} embeds X as a subspace of \overline{X}. This has the subspace topology because of I_{X}.

Lemma 10.10 shows that E_{\{Y | E\}} = \overline{E}, where the translation \overline{E} for terms is defined in the next section.

348  PAUL TAYLOR

The normalised type 9.3. Lemma. The Σ^{{}}η rule, Σ^{i_{X}} · I_{X} = id_{Σ^{X}} or ϕ : Σ^{X}, x : X ⊢ (I_{X}ϕ)(i_{X}x) = ϕx, is valid. Proof. By structural induction on the type X. If X = Σ^{Y ×Z} then

Σ^{i_{X}} · I_{X} = Σ(I \overline{Y} ; Z · I_{Y}^{Z}) · Σ^{2}(i_{Y} × i_{Z})
= Σ(Σ^{i_{Y} ×Z} · (Σ^{i_{Z}} · I_{Z})^{\overline{Y}} · I_{Y}^{Z})  Σ^{i_{Y} ×i_{Z}} = Σ^{i_{Y} ×Z} · (Σ^{i_{Z}})^{\overline{Y}}
= Σ((Σ^{i_{Y}} · I_{Y})^{Z})  induction hypothesis for Z
= id  induction hypothesis for Y.

If X = {Y | E} then

Σ^{i_{X}} · I_{X} = Σ^{i_{Y,E}} · Σ^{i_{Y}} · I_{Y} · I_{Y,E}
= Σ^{i_{Y,E}} · I_{Y,E}  induction hypothesis for Y
= id  Σ^{{}}η for {Y | E}.

9.4. Lemma. The Σ^{{}}β rule, I_{X} · Σ^{i_{X}} = E_{X}, is valid. Proof. By structural induction on the type X. If X = Σ^{Y ×Z} then

I_{X} · Σ^{i_{X}} = Σ^{2}(i_{Y} × i_{Z}) · Σ(I \overline{Y} ; Z · I_{Y}^{Z})
= Σ(I \overline{Y} ; Z · (I_{Y} · Σ^{i_{Y}})^{Z} · Σ^{\overline{Y} ×i_{Z}})
= Σ(I \overline{Y} ; Z · E_{Y}^{Z} · Σ^{\overline{Y} ×i_{Z}})  induction hypothesis for Y
= Σ((I_{Z} · Σ^{i_{Z}})^{\overline{Y}} · E \overline{Z} ; Y )  E_{Y}^{(−)} natural w.r.t. i_{Z}
= Σ(E \overline{Y} ; Z · E \overline{Z} ; Y)  induction hypothesis for Z.

If X = {Y | E} then

I_{X} · Σ^{i_{X}} = I_{Y} · I_{Y,E} · Σ^{i_{Y,E}} · Σ^{i_{Y}}
= I_{Y} · E · Σ^{i_{Y}}  Σ^{{}}β for {Y | E}.

9.5. Proposition. \{ \overline{X} | E_{X}\} is a well formed type, with structure i_{X} and I_{X}. Proof. E_{X} on \overline{X} is a nucleus (Definition 8.7), by the same argument as we used in Corollary 4.13.

SUBSPACES IN ABSTRACT STONE DUALITY  349

The other rules for the extended notation 9.6. Lemma. The {}E_{0} rule is well formed and the {}E_{1} rule is valid. Proof. There is no issue of well-formedness, as i_{X} at any type is built using i_{Y,E} and I_{Y,E} but not admit_{Y,E} from the comprehension calculus. Now let x : X and ϕ : Σ^{\overline{X}}. From Lemmas 9.3 and 9.4 we have

Σ^{i_{X}} · E_{X} = Σ^{i_{X}} · I_{X} · Σ^{i_{X}} = Σ^{i_{X}},

so ϕ(i_{X}x) = Σ^{i_{X}}ϕx = (Σ^{i_{X}} · E_{X})ϕx = E_{X}ϕ(i_{X}x). 9.7. Lemma. The {}I rule is well formed, and the {}β rule is valid, at type X = Σ^{Y ×Z}.

Γ ⊢ ϕ : \overline{X} ≡ Σ^{\overline{Y} × \overline{Z}} Γ, F : Σ^{\overline{X}} ≡ Σ^{2}( \overline{Y} × \overline{Z}) ⊢ F ϕ = E_{X}F ϕ

Γ ⊢ i_{X}(admit_{X} ϕ) = ϕ : X ≡ Σ^{Y ×Z}

Proof. In the introduction rule, admit_{X} ϕ = Σ^{i_{Y} ×i_{Z}}ϕ with no issue of well-formedness, as this expression does not use admit from the comprehension calculus. Also,

F ϕ = E_{X}F ϕ  given side condition
= I_{X}(Σ^{i_{X}}F)ϕ  Lemma 9.4
= Σ^{admit^{X}}(Σ^{i_{X}}F)ϕ
= F (i_{X} admit_{X} ϕ).

So ϕ = i_{X} admit_{X} ϕ by T_{0}. 9.8. Lemma. If X = \{Y | E\} then Ê_{X} ⊂_{\overline{Y}} Ê_{Y} in the sense of Notation 4.4. Proof. E_{X} = E_{{Y | E}} = I_{Y} · E · Σ^{i_{Y}}, whilst E_{Y} = I_{Y} · Σ^{i_{Y}} by Lemma 9.4. Then E_{Y} · E_{X} = I_{Y} · Σ^{i_{Y}} · I_{Y} · E · Σ^{i_{Y}} = I_{Y} · E · Σ^{i_{Y}} = E_{X} = I_{Y} · E · Σ^{i_{Y}} · I_{Y} · Σ^{i_{Y}} = E_{X} · E_{Y} by Lemma 9.3 (Σ^{{}}η for Y). 9.9. Lemma. The {}I rule is well formed, and the {}β rule is valid, at all types. Proof. By structural induction on the type X, with Y = ℕ or Σ^{Z} as the base case (even when Z is itself a product or comprehension type), so consider X = {Y | E}.

Γ ⊢ a : \overline{X} Γ, ϕ : Σ^{\overline{X}} ⊢ ϕa = E_{X}ϕa

Γ ⊢ a = i_{X}(admit_{X} a) ≡ i_{Y} (i_{Y,E}(admit_{Y,E}(admit_{Y} a))) : X

First, ϕa = E_{X}ϕa = (E_{Y} · E_{X})ϕa = E_{Y} ϕa using the given side-condition twice, and since Ê_{X} ⊂ Ê_{Y}. Hence b ≡ admit_{Y} a : Y is well formed, and i_{Y} b = a by the induction hypothesis, {}β for Y.

For the whole expression to be well formed, we need ψ : Σ^{Y} ⊢ ψb = Eψb. Put ϕ = I_{Y} ψ : Σ^{\overline{Y}} . Then

ψb = (I_{Y} ψ)(i_{Y} b)  Σ^{{}}η for Y
= ϕa
= E_{X}ϕ a  hypothesis
= (I_{Y} · E · Σ^{i_{Y}})ϕ a  definition of E_{X}
= (I_{Y} · E · Σ^{i_{Y}})ϕ (i_{Y} b)
= (E · Σ^{i_{Y}})ϕ b  Σ^{{}}η for Y
= (E · Σ^{i_{Y}} · I_{Y})ψ b
= Eψ b  Σ^{{}}η for Y.

Finally, i_{X}(admit_{X} a) = i_{Y,E}(i_{Y} (admit_{Y} (admit_{Y,E} a))) = i_{Y,E}(admit_{Y,E} a) by the induction hypothesis, but this is a by {}β for {Y | E}.

9.10. Lemma. The {}η rule, admit_{X} ·i_{X} = id_{X}, is valid.

Proof. The expression is well formed by Lemmas 9.6 and 9.9. We prove the equation by structural induction on the type X. If X = Σ^{Y ×Z} then, as in Lemma 9.3,

admit_{X} ·i_{X} = Σ^{i_{Y} ×Z} · Σ^{\overline{Y} ×i_{Z}} · I \overline{Y} ; Z · I_{Y}^{Z}
= Σ^{i_{Y} × \overline{Z}} · I_{Y}^{Z}  induction hypothesis for Z
= id  induction hypothesis for Y.

If X = {Y | E} then admit_{X} ·i_{X} = admit_{Y,E} · admit_{Y} ·i_{Y} · i_{Y,E}, which is admit_{Y,E} ·i_{Y,E} by the induction hypothesis, but this is id_{{Y | E}} by {}η for {Y | E}.

The isomorphism

9.11. Proposition.

X x ↦ admit_{\overline{X} ,E_{X}}(i_{X}x) ^{} ≅

admit_{X}(i_{\overline{X} ,E_{X}} \overline{x}) ← \overline{x}

\{ \overline{X} | E_{X}\}

Proof. For the two admit-expressions to be well formed, we need properties of the form E_{X}ϕ(ix) = ϕ(ix), where ix is either i_{X}x or i_{\overline{X} ,E_{X}} \overline{x}, cf. Lemma 8.10.

admit_{\overline{X} ,E_{X}}(i_{X}x) is well formed by Lemma 9.6 (\{\}E_{1} for X) and \{\}I for \{ \overline{X} | E_{X}\}. admit_{X}(i_{\overline{X} ,E_{X}} \overline{x}) is well formed by \{\}E_{1} for \{ \overline{X} | E_{X}\} and Lemma 9.9 (\{\}I for X). admit_{X}(i_{\overline{X} ,E_{X}}(admit_{\overline{X} ,E_{X}}(i_{X}x))) = admit_{X}(i_{X}x) by \{\}β for \{ \overline{X} | E_{X}\}, but this is x

by Lemma 9.10 ({}η for X).

admit_{\overline{X} ,E_{X}}(i_{X}(admit_{X}(i_{\overline{X} ,E_{X}} \overline{x}))) = admit_{\overline{X} ,E_{X}}(i_{\overline{X} ,E_{X}} \overline{x}) by Lemma 9.9 (\{\}β for X), but this is \overline{x} by \{\}η for \{ \overline{X} | E_{X}\}.

9.12. Proposition. This induces Σ^{X} [figure: ϕ ↦ λ \overline{x} . I_{X}ϕ(i_{\overline{X} ,E_{X}} \overline{x}); ≅; λx. I_{\overline{X} ,E_{X}}ϕ(i_{X}x) ← θ] Σ^{\{ \overline{X} | E_{X}\}}.

Proof. ϕ( admit_{X}(i_{\overline{X} ,E_{X}} \overline{x})) = I_{X}ϕ(i_{X}(admit_{X}(i_{\overline{X} ,E_{X}} \overline{x}))) = I_{X}ϕ(i_{\overline{X} ,E_{X}} \overline{x}) because of Lemmas 9.3 and 9.9 (Σ^{{}}η and {}β for X).

θ( admit_{\overline{X} ,E_{X}}(i_{X}x)) = I_{\overline{X} ,E_{X}}θ(i_{\overline{X} ,E_{X}}(admit_{\overline{X} ,E_{X}}(i_{X}x))) = I_{\overline{X} ,E_{X}}θ(i_{X}x) by Σ^{\{\}}η and \{\}β for \{ \overline{X} | E_{X}\}.

10. Normalisation for terms

In the previous section we defined the translation \overline{X} of each type X simply by erasing comprehensions. Although the inclusion map i_{X} : X^{}^{}\overline{X} was more complicated, we shall now see that the corresponding translation \overline{a} of terms is equally simple: erase the connectives i and admit, but replace (the in any case unnatural) I with \overline{E}.

10.1. Notation. By structural recursion on terms, we define the translation

\overline{⊤} = ⊤  \overline{⊥} = ⊥
\overline{0} = 0  \overline{succn} = succ \overline{n}
\overline{ϕ ∧ ψ} = \overline{ϕ} ∧ \overline{ψ}  \overline{ϕ ∨ ψ} = \overline{ϕ} ∨ \overline{ψ}
\overline{λx. ϕ} = λ \overline{x} . \overline{ϕ}  \overline{ϕa} = \overline{ϕ} \overline{a}
\overline{admit_{X,E} a} = \overline{a}  \overline{i_{X,E}a} = \overline{a}
\overline{I_{X,E}θ} = \overline{E} \overline{θ}  \overline{∃n. ϕ[n]} = ∃ \overline{n} . \overline{ϕ[n]}
\overline{rec(n, z, λmu. s)} = rec( \overline{n} , \overline{z} , λm \overline{u} . \overline{s})

For the variable x : X, the symbol \overline{x} (either as a term or as a λ-binding) is not a translation as such, but a new variable of type \overline{X}. We shall also define

\overline{focus P} = force \overline{P} .

Notice that focus is not translated into focus, and we shall not allow terms to involve it in the main part of the discussion. The problem is that the translation \overline{Γ} ⊢ \overline{P} : Σ^{2} \overline{X} does not respect the equation that says that P is prime and so justifies use of the focus operator. However, from Lemma 8.13 and Proposition A 8.10, focus is only needed on the outside of a term, and then only for type ℕ, so we shall deal with it separately at the end of the section.

10.2. Notation. For any context Γ, define \overline{Γ} by replacing each typed variable x : X in Γ by \overline{x} : \overline{X}. Similarly, let i_{Γ} : Γ^{}^{}\overline{Γ} be the list of [i_{X}(x)/ \overline{x}] : X^{}^{}\overline{X}. We write i_{X}^{∗} and i_{Γ}^{∗} for the substitutions that relate terms involving these free variables, whereas Σ^{i_{X}} relates the corresponding λ-abstractions, cf. Lemma 10.7 below. Hence

i_{[ ]}^{∗} \overline{a} = \overline{a} and i_{[Γ,x:X]}^{∗} \overline{a} = [i_{X}(x)/ \overline{x}]^{∗}i_{Γ}^{∗} \overline{a} .

Most of this section is devoted to proving

10.3. Theorem. For any term Γ ⊢ a : X in the comprehension calculus without focus, \overline{Γ} ⊢ \overline{a} : \overline{X} is well formed in the original calculus, whilst

Γ ⊢ a = admit_{X}(i_{Γ}^{∗} \overline{a}) : X  and  Γ ⊢ i_{X}a = i_{Γ}^{∗} \overline{a} : \overline{X}

are provable in the comprehension calculus, i.e. the square

\overline{Γ}  \overline{\overline{a} ^{}}\overline{X}

[figure: Γ; i_{Γ}; a; X; i_{X}; \begin{matrix}admit & X \\ × \end{matrix}]

commutes. The two forms are equivalent by the {}β and {}η rules, Lemmas 9.9 and 9.10. In particular, if Γ and X don’t involve comprehension then Γ ⊢ a = \overline{a} : X.

The proof is by structural induction on the term Γ ⊢ a : X, and therefore has a case for each connective: λ, i, admit, I, etc. Each of these cases is a lemma below, whereas the lemmas in the previous section were self-contained. To avoid repetitious language, the enunciation of each lemma is simply the introduction or elimination rule that defines the connective; by this we mean to assert that “if the premises (sub-terms) obey the equation a = admit_{X}(i_{Γ}^{∗} \overline{a}) then so does the conclusion”.

Since the transformation is also applied to nuclei (Lemma 10.10), the proof is actually on the history of formation of a, rather than simply on the expression without type annotations.

Variables, constants and algebraic operations

10.4. Lemma. For x : X ⊢ x : X, we have admit_{X}(i_{X}^{∗} \overline{x}) = x.

Proof. i_{X}^{∗} \overline{x} = [i_{X}x/ \overline{x}]^{∗} \overline{x} = i_{X}x, and admit_{X}(i_{X}x) = x by Lemma 9.10 (\{\}η for X).

There is nothing to prove for the constants ⊤, ⊥ and 0, and almost nothing for succ, so we just consider ∧ as (an example of) an algebraic operation.

10.5. Lemma.

{Γ ⊢ ϕ : Σ^{X} Γ ⊢ ψ : Σ^{X} \atop Γ ⊢ ϕ ∧ ψ : Σ^{X}}

Recall from the statement of Theorem 10.3 that, by displaying this rule, we mean to claim that if ϕ and ψ satisfy a certain equation then so does ϕ ∧ ψ.

Proof. The general plan is to expand the term in the conclusion of the rule (here ϕ ∧ ψ), using the induction hypothesis for the sub-terms (here ϕ and ψ) and the formulae for admit (Notation 9.2) and i_{Γ}^{∗} (Notation 10.2), then apply the extended “rules” from the previous section, followed by the same procedure in reverse to obtain the translation of the term in question.

ϕ ∧ ψ = (admit_{Σ^{X}} i_{Γ}^{∗} \overline{ϕ}) ∧ (admit_{Σ^{X}} i_{Γ}^{∗} \overline{ψ}) induction hypothesis for ϕ, ψ
= (Σ^{i_{X}}i_{Γ}^{∗} \overline{ϕ}) ∧ (Σ^{i_{X}}i_{Γ}^{∗} \overline{ψ})  Notation 9.2
= Σ^{i_{X}}(i_{Γ}^{∗} \overline{ϕ} ∧ i_{Γ}^{∗} \overline{ψ})  Σ^{i_{X}} is a homomorphism
= Σ^{i_{X}}i_{Γ}^{∗}( \overline{ϕ} ∧ \overline{ψ})  subsitution into ∧
= Σ^{i_{X}}i_{Γ}^{∗} \overline{ϕ ∧ ψ}  Notation 10.1
= admit_{Σ_{X}} i_{Γ}^{∗} \overline{ϕ ∧ ψ}  Notation 9.2.

10.6. Lemma.

{Γ, n : ℕ ⊢ ϕ[n] : Σ^{X} \atop Γ ⊢ ∃n. ϕ[n] : Σ^{X}}

Proof.

∃n. ϕ[n] = ∃n. admit_{Σ^{X}} i_{Γ,n:ℕ}^{∗} \overline{ϕ[n]}  induction hypothesis for ϕ[n]
= ∃n. Σ^{i_{X}}i_{ℕ}^{∗}i_{Γ}^{∗} \overline{ϕ[n]}  Notation 9.2 and 10.2
= Σ^{i_{X}}∃n. i_{ℕ}^{∗}i_{Γ}^{∗} \overline{ϕ[n]}  Σ^{i_{X}} is a homomorphism
= Σ^{i_{X}}i_{Γ}^{∗}∃ \overline{n} . \overline{ϕ[n]}  substitution into ∃
= admit_{Σ^{X}} i_{Γ}^{∗} \overline{∃n. ϕ[n]}  Notation 9.2 and 10.1.

354  PAUL TAYLOR

The lambda calculus

The difference between Σ^{i_{Y}} and i_{Y}^{∗} is that Σ^{i_{Y}} acts on the exponent of the type by λ-reduction, whilst i_{Y}^{∗} acts on the context by substitution.

10.7. Lemma. If Γ, \overline{y} : \overline{Y} ⊢ θ : Σ^{\overline{Z}} then Γ ⊢ Σ^{i_{Y} ×i_{Z}}λ \overline{y} . θ = λy. Σ^{i_{Z}}i_{Y}^{∗} θ : Σ^{Y ×Z}.

Proof.

Σ^{i_{Y} ×i_{Z}}λ \overline{y} . θ = λyz. (λ \overline{y} . θ)(i_{Y} y)(i_{Z}z)  definition of Σ^{i_{Y} ×i_{Z}}
= λyz. ([i_{Y} (y)/ \overline{y}]^{∗}θ)(i_{Z}z)  λβ
= λyz. (i_{Y}^{∗} θ)(i_{Z}z)  definition of i_{Y}^{∗}
= λy. Σ^{i_{Z}}i_{Y}^{∗} θ  definition of Σ^{i_{Z}}.

10.8. Lemma.

{Γ, y : Y ⊢ ϕ : Σ^{Z} \atop Γ ⊢ λy. ϕ : Σ^{Y ×Z}}

Proof. We use Lemma 10.7 with Γ, \overline{y} : \overline{Y} ⊢ θ ≡ i_{Γ}^{∗} \overline{ϕ} : Σ^{\overline{Z}}.

λy. ϕ = λy. admit_{Σ^{Z}} i_{Γ,y:Y}^{∗} \overline{ϕ}  induction hypothesis for ϕ
= λy. Σ^{i_{Z}}i_{Y}^{∗} i_{Γ}^{∗} \overline{ϕ}  Notation 9.2 and 10.2
= Σ^{i_{Y} ×i_{Z}}λ \overline{y} . i_{Γ}^{∗} \overline{ϕ}  Lemma 10.7
= Σ^{i_{Y} ×i_{Z}}(i_{Γ}^{∗}λ \overline{y} . \overline{ϕ})  substitution into λ
= admit_{Σ^{Y ×Z}} i_{Γ}^{∗} \overline{λy. ϕ}  Notation 9.2 and 10.1.

10.9. Lemma.

{Γ ⊢ ϕ : Σ^{Y ×Z} Γ ⊢ a : Y \atop Γ ⊢ ϕ[a] : Σ^{Z}}

Proof.

ϕa = (admit_{Σ^{Y ×Z}} i_{Γ}^{∗} \overline{ϕ})(admit_{Y} i_{Γ}^{∗} \overline{a}) induction hypothesis for ϕ and a
= (Σ^{Y ×i_{Z}}Σ^{i_{Y} × \overline{Z}} i_{Γ}^{∗} \overline{ϕ})(admit_{Y} i_{Γ}^{∗} \overline{a})  Notation 9.2
= Σ^{i_{Z}}(i_{Γ}^{∗} \overline{ϕ} (i_{Y} admit_{Y} i_{Γ}^{∗} \overline{a}))
= Σ^{i_{Z}}(i_{Γ}^{∗} \overline{ϕ} (i_{Γ}^{∗} \overline{a}))  \{\}β for Y
= Σ^{i_{Z}}i_{Γ}^{∗}( \overline{ϕ} \overline{a})  substitution into \overline{ϕ} \overline{a}
= admit_{Σ^{Z}} i_{Γ}^{∗} \overline{ϕa}  Notation 9.2 and 10.1.

Subtypes

Here is where we use the main induction hypothesis in Theorem 10.3 for the nucleus E that defines the subtype {X | E}. The prohibition on focus is not a problem: it can be eliminated, as the type of E is Σ^{X} (Proposition A 8.10).

10.10. Lemma. Σ^{i_{X}} · \overline{E} = E · Σ^{i_{X}} and E_{\{X | E\}} = I_{X} · E · Σ^{i_{X}} = \overline{E}.

Proof. The induction hypothesis for Eϕ and ϕ yields

Eϕ = admit_{Σ^{X}}( \overline{E} \overline{ϕ}) = Σ^{i_{X}}( \overline{E} \overline{ϕ}) and ϕ = admit_{Σ^{X}} \overline{ϕ} = Σ^{i_{X}} \overline{ϕ} ,

so E(Σ^{i_{X}} \overline{ϕ}) = Σ^{i_{X}}( \overline{E} \overline{ϕ}), which is the first equation. The induction hypothesis also says that E_{X} = \overline{E_{X}} , since the type of E_{X} doesn’t involve comprehension. Then

E_{\{X | E\}} = I_{X} · E · Σ^{i_{X}} = I_{X} · Σ^{i_{X}} · \overline{E} = E_{X} · \overline{E} = \overline{E_{X} · E} = E

by Notation 10.2 and Lemmas 9.4, 10.9 and 9.8.

10.11. Lemma.

Γ ⊢ a : X Γ, ϕ : Σ^{X} ⊢ ϕa = Eϕa
Γ ⊢ admit_{X,E} a : {X | E}

Proof.

admit_{X,E} a = admit_{X,E} admit_{X} i_{Γ}^{∗} \overline{a}  induction hypothesis for a
= admit_{\{X | E\}} i_{Γ}^{∗} \overline{a}  Notation 9.2
= admit_{\{X | E\}} i_{Γ}^{∗} \overline{admit_{X,E} a}  Notation 10.2.

10.12. Lemma.

{Γ ⊢ a : \{X | E\} \atop Γ ⊢ i_{X,E}a : X}

Proof.

i_{X,E}a = i_{X,E} admit_{\{X | E\}} i_{Γ}^{∗} \overline{a}  induction hypothesis for a
= i_{X,E} admit_{X,E} admit_{X} i_{Γ}^{∗} \overline{a}  Notation 9.2
= admit_{X} i_{Γ}^{∗} \overline{a}  \{\}η for X, E
= admit_{X} i_{Γ}^{∗} \overline{i_{X,E}a} .  Notation 10.2.

10.13. Lemma.

{Γ ⊢ θ : Σ^{\{X | E\}} \atop Γ ⊢ I_{X,E}θ : Σ^{X}}

Proof.

I_{X,E}θ = I_{X,E} admit_{Σ^{\{X | E\}}} i_{Γ}^{∗} \overline{θ}  induction hypothesis for θ
= I_{X,E}Σ^{i_{X,E}}Σ^{i_{X}}i_{Γ}^{∗} \overline{θ}  Notation 9.2
= EΣ^{i_{X}}i_{Γ}^{∗} \overline{θ}  Σ^{\{\}}β for X, E
= Σ^{i_{X}} \overline{E} i_{Γ}^{∗} \overline{θ}  Lemma 10.10
= Σ^{i_{X}}i_{Γ}^{∗} \overline{E} \overline{θ}  substitution into \overline{E} \overline{θ}
= admit_{Σ^{X}} i_{Γ}^{∗} \overline{I_{X,E}θ}  Notation 9.2 and 10.2.

Recursion

10.14. Lemma.

{Γ ⊢ n : ℕ  Γ ⊢ z : X  Γ, m : ℕ, x : X ⊢ s(m, x) : X \atop Γ ⊢ rec(n, z, λmx. s) : X}

Proof. Let Γ ⊢ z′ = i_{Γ}^{∗} \overline{z} : \overline{X} and Γ, m : ℕ, \overline{x} : \overline{X} ⊢ s′(m, \overline{x}) = i_{Γ}^{∗} \overline{s} (m, \overline{x}) : \overline{X} . So the induction hypotheses say that Γ ⊢ n = i_{Γ}^{∗} \overline{n} : ℕ, Γ ⊢ z = admit_{X} z′ : X and

Γ, m : ℕ, x : X ⊢ s(m, x) = admit_{X} s′(m, i_{X}x) : X.

We use Lemma 8.14, or rather its analogue with the extended rules of Section 9 in place of the \{\}β- and η-rules; the symbols \overline{x}, z′ and s′ here correspond to y, z and s there.

rec(n, z, λmx. s)
= rec(n, admit_{X} z′, λmx. admit_{X} s′(m, i_{X}x)) induction hypothesis
= admit_{X} rec(n, z′, λm \overline{x} . s′(m, \overline{x}))  Lemma 8.14
= admit_{X} rec(i_{Γ}^{∗} \overline{n} , i_{Γ}^{∗} \overline{z} , λm \overline{x} . i_{Γ}^{∗} \overline{s} (m, \overline{x}))  definition
= admit_{X} i_{Γ}^{∗}rec( \overline{n} , \overline{z} , λm \overline{x} . \overline{s} (m, \overline{x}))  substitution into rec
= admit_{X} i_{Γ}^{∗} \overline{rec(n, z, λmx. s)} : X  Notation 10.2.

Sobriety

We have now completed the proof of Theorem 10.3, that, for any term Γ ⊢ a : X in the comprehension calculus without focus,

Γ ⊢ a = admit_{X}(i_{Γ}^{∗} \overline{a}) : X and Γ ⊢ i_{X}a = i_{Γ}^{∗} \overline{a} : \overline{X} .

There are two ways of handling a term focus P : ℕ.

10.15. Remark. Lemma 8.11 says that ℕ ≅ {Σ^{2}ℕ | E_{ℕ}}, where E_{ℕ} characterises primes. This makes use of admit instead of focus. More generally, {ℕ | E} ≅ {Σ^{2}ℕ | E′}, where E′ encodes the composite inclusion. Another way of saying this is that, in Notation 9.2, we define the base case \overline{ℕ} as Σ^{2}ℕ instead of ℕ. This way we only ever deal with subspaces of injectives (cf. Corollary 5.3), and never need to use focus.

10.16. Remark. Alternatively, if Γ ⊢ P : Σ^{2}X is a prime not involving focus,

focus_{X} P = admit_{X} ( focus_{\overline{X}} (Σ^{2}i_{X}P))  Lemma 8.13
= admit_{X} ( focus_{\overline{X}} (i_{Σ^{2}X}P))  Notation 9.2
= admit_{X} ( focus_{\overline{X}} (i_{Γ}^{∗} \overline{P} ))  Theorem 10.3
= admit_{X} (i_{Γ}^{∗} force_{\overline{X}} \overline{P} )  cf. Lemma A 8.4
= admit_{X} (i_{Γ}^{∗} \overline{focus_{X} P} )  Notation 10.2.

Lemma A 8.4 actually said

u : Δ → Γ Γ ⊢ P : Σ^{2}X prime
Δ ⊢ u^{∗}P : Σ^{2}X prime
Δ ⊢ u^{∗}(focus P) = focus(u^{∗}P) : X

and we’re trying to use its converse, which is not valid. Although Γ ⊢ i_{Γ}^{∗} \overline{P} : Σ^{2} \overline{X} is prime, \overline{Γ} ⊢ \overline{P} : Σ^{2} \overline{X} need not be. This is why we write force instead of focus here.

Semantically, Γ^{}^{}\overline{Γ} is a subspace, on which the relevant equation holds, but it need not hold on the ambient space \overline{Γ}. That such a situation arises is more obvious for descriptions (Remark A 9.13): any predicate \overline{Γ} ⊢ ϕ : Σ^{ℕ} becomes a description when restricted to the locally closed subspace Γ^{}^{}\overline{Γ} defined by

(∃n. ϕ[n]) = ⊤ and (∃nm. ϕ[n] ∧ ϕ[m] ∧ n ≠ m) = ⊥.

In the terms of this paper, the equation in Definition 4.5 defining a (prime or) homomorphism on a subspace {Y_{1} | E_{1}} involves Ê_{1}, and does not imply the form without it.

Nevertheless, it is a legitimate alternative way of treating focus P to translate it into force \overline{P} . For, if Γ ⊢ ψ : Σ^{X} then

ψ[focus P] = P ψ = (admit_{Σ^{2}X} i_{Γ}^{∗} \overline{P} )(admit_{Σ^{X}} i_{Γ}^{∗} \overline{ψ}) = i_{Γ}^{∗} \overline{P ψ} = i_{Γ}^{∗} \overline{ψ} [force \overline{P} ]

using the unrestricted β-rule for force.

As we know from Sections A 8 and 11, and the work on computational effects cited there, we may obtain different terms \overline{Γ} ⊢ \overline{a} : \overline{X} by applying or reversing the β- and η-rules of the λ-calculus with force. So, for such a calculus to be defined consistently, an order of evaluation must be specified.

However, these computational terms with possibly different denotations on \overline{Γ} become equal when we apply i_{Γ}^{∗} to restrict them to the required context Γ. In other words, as we know very well from experience, there are different programs \overline{Γ} ⊢ \overline{a} : \overline{X}, possibly involving computational effects, to compute the same denotational value Γ ⊢ a : X.

Categorical equivalence

10.17. Theorem. Let C and D be the categories generated by the restricted λ-calculus (possibly with the extra structure) and the comprehension calculus. Then there is an equivalence of categories \overline{C} ≃ D whose effect on types is

[figure: \{X | E\}; \{X | E\}; \overline{C}; ≃; D; \{ \overline{X} | \overline{E_{X}} \}; X,]

where the notation \{X | E\} in \overline{C} is the categorical one in Section 4, whilst in D it is understood as the comprehension calculus in Section 8.

Proof. The previous section defined the transformation D → \overline{C} on types, and showed that the composite D → \overline{C} → D is isomorphic to the identity: Proposition 9.11 provided mutually inverse terms in the comprehension calculus that relate any type X to \{ \overline{X} | E_{X}\}. The other composite is the identity on types, so we just have to show that \overline{C} → D is full and faithful.

Let X_{1} and X_{2} be types that are defined without comprehension, and E_{1} and E_{2} nuclei on them. We shall show that there is a bijection between the \overline{C}-morphisms

Ĵ: {X_{1} | E_{1}} ⟶ {X_{2} | E_{2}}

defined in Section 4 and the terms

x : {X_{1} | E_{1}} ⊢ focus P : {X_{2} | E_{2}}

that we have just expressed in normal form. Of course \overline{\{X_{1} | E_{1}\}} = X_{1}, and we write i_{1} = i_{X_{1}}, etc.

In each of the categories, these morphisms correspond bijectively to homomorphisms

Σ^{{X_{2} | E_{2}}} ⟶ Σ^{{X_{1} | E_{1}}},

but first we consider ordinary maps, without the homomorphism requirement.

By Proposition 6.2 for \overline{C}, Σ^{\{X | E\}} ≅ \{Σ^{X} | Σ^{E}\}, which is simply a retract of the power type Σ^{X} in C (the restricted λ-calculus), so a \overline{C}-morphism J : Σ^{\{X_{2} | E_{2}\}} → Σ^{\{X_{1} | E_{1}\}} is a C-morphism J : Σ^{X_{2}} → Σ^{X_{1}} such that E_{2} ; J = J = J ; E_{1}.

[figure: Σ^{X_{2}}; J; Σ^{X_{1}}; Σ^{X_{2}}; \overline{H}; Σ^{X_{1}}]

[figure: Σ^{{X_{2} | E_{2}}}; E_{2}; E_{2}; J; Σ^{{X_{1} | E_{1}}}; E_{1}; E_{1}; Σ^{{X_{2} | E_{2}}}; i_{Σ^{X_{2}}} = I_{2}; Σ^{i_{2}}; H; Σ^{{X_{1} | E_{1}}}; I_{1}; Σ^{i_{1}} = admit_{Σ^{X_{1}}}]

The corresponding power type in D is also a retract, and Theorem 10.3 characterised its morphisms H in the same fashion. Hence H\overline{C} ≃ HD.

Now, homomorphisms are characterised equationally amongst all maps, and we have already shown that the functor is full and faithful for them, i.e. that maps and their equations agree, so the homomorphisms also agree.

In \overline{C}, the equation that defines homomorphisms is more clearly understood by means of Lemma 6.6, i.e. with reference to the subtypes {X_{i} | E_{i}}, rather than using Definition 4.5, which transfers the condition to the ambient types X_{i}. We have seen the same phenomenon in D, where the translation \overline{P} of a prime P relative to the sub-types need not be prime with respect to the translated types.

That deals with single-type contexts, but that is enough as products may be encoded as comprehension types in each category.

Therefore our first construction, adjoining formal Σ-split equalisers to the category in Sections 4–6, is equivalent to the third, the extension of the λ-calculus in Sections 8–10.

11. Sums and quotients

Paré’s theorem, that any elementary topos has the monadic property [Par74], which originally inspired abstract Stone duality, was itself motivated by the simple way that it affords for constructing colimits. So we conclude this paper with applications of the comprehension calculus to coproducts and coequalisers.

11.1. Example. The idea of Stone duality is to consider spaces in terms of the corresponding algebras. For any algebra (A, α), we have

pts(A, α) = {Σ^{A} | η_{A} · α ≡ λF ϕ. ϕ(αF)},

in which η_{A} · α is a nucleus (Definition 8.7) because of the Eilenberg–Moore equations for α. The homomorphism H : B → A corresponds to the function

x : pts(A, α) ⊢ admit (λψ. Hψ(ix)) : pts(B, β),

in which H is behaving as a continuation-transformer. (We saw in the previous section that the operators i and admit merely serve as compile-time type-annotation.) In particular, if H = Σ^{f}, where f : X → Y, this is just focus (λψ. ψ(fx)) = fx by Lemma 8.11.

The continuation-passing style is more clearly visible in a more complicated example.

11.2. Example. The coproduct X + Y of spaces corresponds to the product A = Σ^{X} × Σ^{Y} of algebras, whose structure map α = ⟨P_{0}, P_{1}⟩ was given in Lemma 5.5:

P_{0} : Σ^{2}(Σ^{X} × Σ^{Y}) → Σ^{X} by H ↦ λx. H (λϕψ. ϕx).

Then X + Y = pts(A, α) = {Σ^{Σ^{X}×Σ^{Y}} | E_{X+Y} }, where

E_{X+Y} = η_{Σ^{X}×Σ^{Y}} · α : H ↦ λH. H ⟨P_{0}H, P_{1}H⟩.

The inclusion ν_{0} : X → X + Y satisfies Σ^{ν_{0}} = π_{0}, so

ν_{0}(x) = admit(λϕψ. ϕx) and ν_{1}(y) = admit(λϕψ. ψy).

Then, for f : X → Z and g : Y → Z, the mediator X + Y → Z is

[f, g] : u ↦ focus (λθ. (iu)(λx. θ(fx))(λy. θ(gy))),

in which the continuation θ from Z is passed either as θ · f to X or as θ · g to Y. When u = ν_{0}(x) or ν_{1}(y), one of the two branches is selected and that continuation is applied to x or y.

We already know that products distribute over coproducts (Proposition A 7.11), and coproducts are disjoint and stable under pullback on the assumption that Σ is a distributive lattice and satisfies the Euclidean principle (Section C 9). In fact this extra structure is unnecessary: if (C, Σ) is monadic then C is extensive on a very much weaker assumption.

11.3. Lemma. The map 0 → 1 is a Σ-split mono iff Σ has a constant.

Proof. I : Σ^{0} = 1 → Σ = Σ^{1}.

If I = ⊤, this makes 0 a closed subspace; if I = ⊥ then it’s open (Examples 2.5). However, we shall call the constant ⋆ here to emphasise that we are not using any lattice structure. Then coproduct inclusions are also Σ-split monos:

11.4. Lemma. X ≅ {X + Y | ⟨π_{0}, ⋆⟩} and Y ≅ {X + Y | ⟨⋆, π_{1}⟩}.

Proof. These idempotents arise from the diagram

[figure: Σ^{X}; \underline{π_{0} ≡ Σ^{ν_{0}}}; ⟨id, ⋆⟩; Σ^{X} × Σ^{Y}; π_{1} ≡ Σ^{ν_{1}}; ⟨⋆, id⟩; Σ^{Y}]

We want to show that every map U → 2 arises in this way from a unique coproduct. Because of the continuation-passing behaviour, it is convenient to treat 2 as a subspace of Σ^{Σ×Σ}. Then the definable elements are π_{0} ≡ λxy. x and π_{1} ≡ λxy. y, which simply select the appropriate continuation from the pair.

11.5. Lemma. 2 ≅ {Σ^{Σ×Σ} | λFF . F (Fπ_{0}, Fπ_{1})}.

Proof. This is the primality equation, FP = P (λx. F(λϕ. ϕx)), with λx replaced by the two values 0, 1 : 2, and ϕ : Σ^{2} by a pair.

We shall abuse our language by calling the two-argument functions P : Σ^{Σ×Σ} that belong to this subspace “prime”. However, we need yet another characterisation of them.

11.6. Lemma. Γ ⊢ P : Σ^{Σ×Σ} is prime iff, for x, y, z : Σ and G : Σ^{Σ^{Σ}},

P (x, x) = x P (P (x, y), z) = P (x, z) = P (x, P (y, z))

G(λz. P (z, ⋆)) = P (Gid, G(λz. ⋆)) G(λz. P (⋆, z)) = P (G(λz. ⋆), Gid). Proof. If P is prime, so Γ, F : Σ^{2}(Σ × Σ) ⊢ FP = P (Fπ_{0}, Fπ_{1}), then

• put F ≡ λQ. x, so FP = Fπ_{0} = Fπ_{1} = x and primality says that x = P (x, x);

• put F ≡ λQ. Q(Q(x, y), z), so Fπ_{0} = x, Fπ_{1} = z and P (P (x, y), z) ≡ FP = P (x, z);

• put F ≡ λF. G(λz. F (z, ⋆)), so Fπ_{0} = Gid, Fπ_{1} = G(λz. ⋆) and primality says that G(λz. P (z, ⋆)) ≡ FP = P (Gid, G(λz. ⋆)).

Conversely, we first put G ≡ λθ. F(λxy. θP (x, y)), so G(λz. ⋆) = F(λxy. ⋆), Gid = FP,

G(λz. P (z, ⋆)) = F(λxy. P (P (x, y), ⋆)) = F(λxy. P (x, ⋆)),
G(λz. P (⋆, z)) = F(λxy. P (⋆, P (x, y))) = F(λxy. P (⋆, y)),

with which the equations involving G give

F(λxy. P (x, ⋆)) = P (FP, F(λxy. ⋆)) F(λxy. P (⋆, y)) = P (F(λxy. ⋆), FP ).

Next put G ≡ λθ. F(λxy. θx), so

G(λz. ⋆) = F(λxy. ⋆), G(λz. P (z, ⋆)) = F(λxy. P (x, ⋆)) and Gid = Fπ_{0},

with which the first G-equation gives

F(λxy. P (x, ⋆)) = P (Fπ_{0}, F(λxy. ⋆)),

and similarly G ≡ λθ. F(λxy. θy) yields F(λxy. P (⋆, y)) = P (F(λxy. ⋆), F π_{1}).

From these four consequences of the higher-type G-equations, together with the ones of base type, we deduce that P is prime:

FP = P (P (FP, F(λxy. ⋆)), P (F(λxy. ⋆), FP))
= P (F(λxy. P (x, ⋆)),  F(λxy. P (⋆, y)))
= P (P (Fπ_{0}, F(λxy. ⋆)), P (F(λxy. ⋆), Fπ_{1}))
= P (Fπ_{0}, Fπ_{1}).

11.7. Proposition. Let u : U ⊢ P u : Σ^{Σ×Σ} be prime. Then the following subspaces are well defined, their coproduct is U and the squares are pullbacks.

[figure: {U | E_{0} ≡ λϕu. P u(ϕu, ⋆)}; U; {U | E_{1} ≡ λψu. P u(⋆, ψu)}; 1; 2; u ↦ focus(P u); 1]

Proof. To show that E_{0} is a nucleus, we must show for u : U and F : Σ^{3}U that

E_{0}(λv. F(λϕ. E_{0}ϕv))u = P u(F(λϕ. P u(ϕu, ⋆)), ⋆) ≡ P u(y, ⋆)

is equal to

E_{0}(λv. F(λϕ. ϕv))u = P u(F(λϕ. ϕu), ⋆) ≡ P u(x, ⋆).

Put G ≡ λθ. F(λϕ. θ(ϕu)) in the Lemma. Then

y = F(λϕ. P u(ϕu, ⋆))
= G(λz. P u(z, ⋆))
= P u(Gid, G(λz. ⋆))
= P u(F(λϕ. ϕu), F(λϕ. ⋆))
≡ P u(x, t),

so P u(y, ⋆) = P u(P u(x, t), ⋆) = P u(x, ⋆) as required.

To test that the left hand square is a pullback, we are given Γ ⊢ v : U such that Γ ⊢ P v = π_{0}. Then

Γ, θ : Σ^{U} ⊢ E_{0}θv = P v(θv, ⋆) = π_{0}(θv, ⋆) = θv,

as is required to form the mediator Γ ⊢ admit v : {U | E_{0}}.

To show that U is the coproduct, we must show that Σ^{U} is the associated product, i.e. that θ : Σ^{U} corresponds bijectively to ⟨ϕ, ψ⟩ where ϕ = E_{0}ϕ and ψ = E_{1}ψ. In fact, P serves for the pairing operation as well as for the projections: θ = λu. P u(ϕu, ψu).

θ ↦ ⟨λu. P u(θu, ⋆), λu. P u(⋆, θu)⟩ ↦ λu. P u(P u(θu, ⋆), P u(⋆, θu)) = λu. θu

(ϕ, ψ) ↦ λu. P u(ϕu, ψu) ^{π_{0}}^{}λu. P u(P u(ϕu, ψu), ⋆) = λu. P u(ϕu, ⋆) = E_{0}ϕ.

11.8. Theorem. If (C, Σ) is monadic and Σ has a constant then C is extensive, i.e. it has stable disjoint coproducts [Tay99, Section 5.5].

[figure: X; U; Y; 1; 2; 1]

Proof. We have to show that the commutative diagram is a pair of pullbacks iff its top row is a coproduct. The map U → 2 must arise from a prime u : U ⊢ P u : Σ^{Σ×Σ}, from which Proposition 11.7 constructs subspaces forming pullbacks and a coproduct. Since pullbacks are unique up to isomorphism, if the given diagram is a pair of pullbacks then it is isomorphic to that in the Proposition.

Conversely, if we are given a coproduct U = X + Y then u : U ⊢ P u : Σ^{Σ×Σ} is defined by x : X ⊢ P x ≡ π_{0} and y : Y ⊢ P y ≡ π_{1}. Then E_{0} in the Proposition becomes

E_{0}θ = E_{0}⟨ϕ, ψ⟩ = ⟨λx. π_{0}⟨ϕ, ψ⟩x, λy. ⋆⟩ = ⟨ϕ, ⋆⟩,

which agrees with Lemma 11.4.

11.9. Corollary. Let x : X ⊢ fx, gx : Z and x : X ⊢ P x : Σ^{Σ×Σ} with P prime. Then

if (focus P) then fx else gx = focus (λθ. P x(θ(fx))(θ(gx))).

Turning from coproducts to coequalisers, of course we can only construct those that are Σ-split. We leave the reader to formulate Beck-style equations as in Section 3, concentrating instead on the analogue for quotients of the comprehension calculus for subspaces in Section 8. Beware also that the class of Σ-epis is stable under products but not necessarily pullbacks. For the topological motivation, recall that the quotient topology on a set Y induced by the function q : X → Y from a topological space has V ⊂ Y open iff q^{−1}V is open in X.

11.10. Lemma. Let X ×Q̂^{[figure: q]} Y be a Σ-split epi, and put R̂ = Q̂ · q. Then

Y ≅ {Σ^{2}X | E}, where EFF = F (λx. F(λϕ. Rϕx)),
qx = admit(λϕ. Rϕx) and Qϕ = λy. iyϕ.

Proof. Three of the four squares

[figure: Σ^{2}X; Σ^{2}q; Σ^{Q}; Σ^{2}Y; X; η_{X}; η̂_{Σ^{X}} ; ×; q; × \underline{Q̂}; Y; η_{Y}; η̂_{Σ^{Y}} ; ×]

commute by naturality, but that from Y to Σ^{2}X need not. So Ê is the composite from Σ^{2}X anticlockwise back to itself:

Ê = Σ^{2}q ; η̂_{Σ^{Y}} ; η_{Y} ; Σ^{Q} = η̂_{Σ^{X}} ; q ; η_{Y} ; Σ^{Q} = η̂_{Σ^{X}} ; η_{X} ; Σ^{Σ^{q}} ; Σ^{Q},

so EFF = η_{Σ^{X}}(Σ^{η_{X}}(Σ^{2}RF))F = F (λx. F(λϕ. Rϕx)). Next,

i(qx) = Σ^{Q}(η_{Y} (qx)) = Σ^{Q}(Σ^{2}q(η_{X}x)) = Σ^{R}(η_{X}) = λϕ. Rϕx,

whence qx = admit(λϕ. Rϕx). Finally, iyϕ = Σ^{Q}(η_{Y} y)ϕ = (λϕ. ϕy)(Qϕ) = Qϕy.

11.11. Proposition. Y ≡ X/R, qx ≡ [x] and

( let y = [x] in fx) ≡ focus (λθ. Q(θ · f)y) ≡ focus (λθ. (iy)(θ · f))

satisfy the rules

x : X ⊢ [x] : X/R  /I
Γ, x : X ⊢ fx : Z Γ, θ : Σ^{Z} ⊢ (θ · f) = R(θ · f) : Σ
Γ, y : X/R ⊢ ( let y = [x] in fx) : Z

/E

Γ, x : X ⊢ fx : Z Γ, θ : Σ^{Z} ⊢ (θ · f) = R(θ · f) : Σ
Γ, x : X ⊢ ( let[x] = [x′] in fx′) = fx

/β

y : X/R ⊢ ( let y = [x] in [x]) = y  /η,

together with those for the quotient topology (Σ^{/}I, Σ^{/}E, Σ^{/}β and Σ^{/}η),

ϕ : Σ^{X} ⊢ Qϕ : Σ^{X/R}  ϕ : Σ^{X}, x : X ⊢ (Qϕ)(qx) = Rϕx
ψ : Σ^{X/R} ⊢ Σ^{q}ψ : Σ^{X}  ψ : Σ^{X/R} ⊢ Q(Σ^{q}ψ) = ψ.

Proof. We verify the /β and /η rules:

let [x] = [x′] in fx′ = focus (λθ. i(qx)(λx′. θ(fx′)))  definition
= focus (λθ. (λϕ. Rϕx)(λx′. θ(fx′)))  Lemma 11.10
= focus (λθ. R(θ · f)x)
= focus (λθ. (θ · f)x) = fx  R(θ · f) = (θ · f)
let y = [x] in [x] = focus (λψ. (iy)(ψ · q))
= focus (λψ. Q(ψ · q)y)  Lemma 11.10
= focus (λψ. (Q · Σ^{q})ψy)
= focus(λψ. ψy) = y  Q · Σ^{q} = id.

11.12. Remark. Notice that the β-rule is not a computational reduction, but a denotational equation that is a consequence of the equation R(θ · f) = (θ · f) in its hypothesis. A compiler equipped with a proof assistant might perhaps be able know this, but otherwise we can only hope that the implementation will somehow find its way from one side of the β-rule to the other.

Let us specialise this to sets and (discrete) topological spaces, now making use of the lattice structure.

11.13. Example. Section C 10 constructs the quotient X/δ of an overt discrete object X by the open equivalence relation classified by δ : X × X → Σ. Overt discrete means that X is equipped with predicates ∃_{X} : Σ^{X} → Σ and (=_{X}) : X × X → Σ satisfying the usual properties.

The construction in Lemma C 10.8 obtains Σ^{X/δ} (which is unfortunately called Σ^{Q} = E there, for “quotient” and “equaliser”) as a retract of Σ^{X}, namely as the image of the closure operation

R ≡ Σ^{q} · ∃_{q} ≡ λϕx. ∃y. δ(x, y) ∧ ϕ(y).

The quotient space is therefore X/δ = X/R = {Σ^{2}X | E}, where

EFF ≡ F (λx. F(λϕ. ∃y. δ(x, y) ∧ ϕy))
q(x) ≡ admit (λϕ. ∃y. δ(x, y) ∧ ϕ(y)).

If f : X → Z respects the equivalence relation δ then the β-rule is

focus (λθ. ∃y. δ(x, y) ∧ θ(fy)) = fx.

In principle this computation involves a search of the equivalence class, which makes sense, given the connection between coequalisers and while programs [Tay99, Section 6.4].

11.14. Example. As explained in Remark C 10.12, there is another representation of X/δ that is more like the familiar one with equivalence classes. It arises from the factorisation

[figure: X; q; ×  \underline{ˆ∃_{q}}; X/δ; \{\}; ×; Σ^{X/δ}; Σ^{q}; ⊤; \underline{∃_{q}}; Σ^{X}]

of the transpose δ̃ of the equivalence relation. This generalises

ℕ ≅ {Σ^{ℕ} | E} by n ↦ {n}, where E = λF ϕ. ∃n. F (λm. m = n) ∧ ϕn,

cf. Section A 10. The quotient is now given by {Σ^{X} | E}, where

E = λF ϕ. ∃x. F (λy. δ(x, y)) ∧ ϕx,

with qx = admit (λy. δ(x, y)).

If f : X → Z respects the equivalence relation then the mediator X/δ → Z is

y ↦ focus (λθ. ∃x′. iyx′ ∧ θ(fx′)).

This selects an element x′ from the equivalence class y ∈ X/δ (classified by a predicate iy ∈ Σ^{X}) and applies f to it, as we would expect. Substitution of y = qx yields the same formula focus (λθ. ∃x′. δ(x, x′) ∧ θ(fx′)) as before.

11.15. Remark. Here is a summary of the comprehension types that we have used.

X ≅ {Σ^{2}X | λFF . F (λx. F(λϕ. ϕx))}  Remark 4.11
{X | E_{0}} × {Y | E_{1}} = {X × Y | E_{1}^{X} · E_{0}^{Y} }  Proposition 5.12
{X | E_{0}} + {Y | E_{1}} = {Σ^{Σ^{X}×Σ^{Y}} | E}  Example 11.2
where EHH = H⟨λx. H(λϕψ. E_{0}ϕx), λy. H(λϕψ. E_{1}ϕy)⟩
Σ^{{X | E}} = {Σ^{X} | Σ^{E}}  Proposition 6.2
{{X | E_{1}} | E_{2}} = {X | E_{2}}  Proposition 6.10
pts(A, α) = {Σ^{A} | λF ϕ. ϕ(αF)}  Example 11.1
X/R = {Σ^{2}X | λFF . F (λx. F(λϕ. Rϕx))} Proposition 11.11
U ∩ (X \ V) = {X | λϕ. U ∧ ϕ ∨ V }  Examples 2.5
X/δ = {Σ^{2}X | λFF . F (λx. F(λϕ. ∃y. δ(x, y) ∧ ϕy))}
≅ {Σ^{X} | λF ϕ. ∃x. F (λy. δ(x, y)) ∧ ϕx} Examples 11.13f.

References

[Bou66] Nicolas Bourbaki. Topologie Générale. Hermann, 1966. Chapter I, “Structures Topologiques”. English translation, “General Topology”, distributed by Springer-Verlag, 1989.

[BR98] Anna Bucalo and Giuseppe Rosolini. Repleteness and the associated sheaf. Journal of Pure and Applied Algebra, 127:147–151, 1998.

[BW85] Michael Barr and Charles Wells. Toposes, Triples, and Theories. Number 278 in Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1985.

[Eck69] Beno Eckmann, editor. Seminar on Triples and Categorical Homology Theory, number 80 in Lecture Notes in Mathematics. Springer-Verlag, 1969.

[Fak70] Sabah Fakir. Monade idempotente associée à une monade. Comptes Rendues de l’Academie des Sciences de Paris, Série A–B, 270:A99–101, 1970.

[Fef77] Solomon Feferman. Categorical foundations and foundations of category theory. In Robert Butts and Jaakko Hintikka, editors, Logic, Foundations of Mathematics and Computability Theory, pages 149–169. Reidel, 1977.

[FS90] Peter Freyd and Andre Scedrov. Categories, Allegories. Number 39 in Mathematical Library. North-Holland, 1990.

[FW90] Barry Fawcett and Richard Wood. Completely distributive lattices I. Mathematical Proceedings of the Cambridge Philosophical Society, 107:81–9, 1990.

[GHK^{+}80] Gerhard Gierz, Karl Heinrich Hoffmann, Klaus Keimel, Jimmie Lawson, Michael Mislove, and Dana Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980.

[HM81] Karl Hofmann and Michael Mislove. Local compactness and continuous lattices. In Bernhard Banaschewski and Rudolf-Eberhard Hoffmann, editors, Continuous Lattices, number 871 in Springer Lecture Notes in Mathematics, pages 209–248, 1981.

[Joh82] Peter Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[Law70] Bill Lawvere. Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In Alex Heller, editor, Applications of Categorical Algebra, number 17 in Proceedings of Symposia in Pure Mathematics, pages 1–14. American Mathematical Society, 1970.

[LR73] Joachim Lambek and Basil Rattray. Localizations at injective objects in complete categories. Proceedings of the American Mathematical Society, 41:1–9, 1973.

[LR75] Joachim Lambek and Basil Rattray. Localizations and sheaf reflectors. Transactions of the American Mathematical Society, 210:279–293, 1975.

[ML71] Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.

[ML84] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984.

[Mog91] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[MRW02] Francisco Marmolejo, Robert Rosebrugh, and Richard Wood. A basic distributive law. Journal of Pure and Applied Algebra, 168:209–226, 2002.

[Par71] Robert Paré. On absolute colimits. Journal of Algebra, 19:80–95, 1971.

[Par74] Robert Paré. Colimits in topoi. Bulletin of the American Mathematical Society, 80(3):556–561, 1974.

[RR88] Edmund Robinson and Giuseppe Rosolini. Categories of partial maps. Information and Computation, 79:95–130, 1988.

[Sco72] Dana Scott. Continuous lattices. In Bill Lawvere, editor, Toposes, Algebraic Geometry and Logic, number 274 in Lecture Notes in Mathematics, pages 97–137. Springer–Verlag, 1972.

[Sco76] Dana Scott. Data types as lattices. SIAM Journal on Computing, 5:522–587, 1976.

[Tar35] Alfred Tarski. Zur Grundlegung der Boole’schen algebra. Fundamenta Mathemematica, 24:177–198, 1935.

[Tay99] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[Thi97] Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997. Also available as technical report ECS-LFCS-97-376.

[Vic95] Steven Vickers. Locales are not pointless. In Ian Mackie and Rajagopal Nagarajan, editors, Theory and Formal Methods of Computing, 1995.

[Vic02] Steven Vickers. The double powerlocale and exponentiation. Submitted to Theory and Applications of Categories, 2002.

The papers on abstract Stone duality may be obtained from

                     http://www.di.unito.it/∼pt/ASD

[A] Paul Taylor. Sober spaces and continuations. Theory and Applications of Categories, 10(12):248–300, 2002.

[C] Paul Taylor. Geometric and higher order logic using abstract Stone duality. Theory and Applications of Categories, 7(15):284–338, 2000.

[D] Paul Taylor. Non-Artin gluing in recursion theory and lifting in abstract Stone duality, 2000.

[E] Paul Taylor. Local compactness and the Baire category theorem in abstract Sone duality, Category Theory and Computer Science, Ottawa, 2002.

[F] Paul Taylor. Scott domains in abstract Stone duality, 2002.

Email: pt@di.unito.it

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/10/13/10-13.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh,

rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

John Baez, University of California, Riverside: baez@math.ucr.edu Michael Barr, McGill University: barr@barrs.org, Associate Managing Editor Lawrence Breen, Université Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Sydney: stevel@maths.usyd.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Andrew Pitts, University of Cambridge: Andrew.Pitts@cl.cam.ac.uk Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca, Managing Editor Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca