We have seen how some of the ideas of topology can be expressed using the types and terms of a λ-calculus. In particular, compactness of a space K is expressed as a “universal quantifier” ∀KK→Σ. The main application of this idea will be to the closed interval K≡[d,u]⊂ R⊂Σ×ΣY, where we shall construct R as the subspace of those pairs of predicates on ℚ that are Dedekind cuts (Remark 2.1).

How could we obtain a map ΣK→Σ from one i:KY? We have ΣY→Σ by evaluation at some y:Y (Lemma 5.12), but nothing ΣK→ΣY, since the maps go the wrong way. However, given that we have already introduced higher types, it hardly seems to be a revolutionary step to introduce extra terms of those types. Indeed, in our brief account of interval analysis in Section 2, we have already discussed such a map, IK→ΣY. It extends open sets and functions from the real line to the interval domain, and it is intimately related to the quantifiers ∀ and ∃, indeed these are special cases of it.

In this section we shall give the type-theoretic rules that formally introduce i and I for (certain) subspaces, at least the ones that we need. This will complete our manual of the axioms of ASD. The basis of our proof of the Heine–Borel theorem is that the rules force these subspaces to carry the subspace topology. Naturally, we shall use terms of higher type (such as I) to do this, just as we have already introduced terms of lower type and equations between them in the previous section.

Definition 5.1 An inclusion i:XY is called a Σ-split subspace if there is another map IX↣ΣY such that

 Σi· I =  idΣX     or     x:X,  φ:ΣX  ⊢ Iφ(i x)  ⇔   φ x,

thereby making ΣX a retract of ΣY with inclusion I and projection Σi. The convention in the λ-calculus is that Iφ(i x) means (Iφ)(i x).

Remark 5.2 Whenever two maps compose to the identity one way round like this, they may be recovered (uniquely up to unique isomorphism) from their composite the other way, which is an idempotent (E=E· E). In this case, EI·ΣiY→ΣY determines ΣX. (We wrote E for E in Proposition 2.15 in accordance with our convention of using fancier typefaces for fancier types.) The object X itself is the equaliser

The idea is that the operator E “normalises” open subspaces of Y by restricting them to X using Σi, and then re-expanding them using I. Therefore a:Y belongs to {YE} iff its membership of any open subspace ψ of Y is unaffected by this process.

Definition 5.3 Recall that being the equaliser means that

1. the inclusion i has equal composites with the parallel pair: it sends each x:X to yi x:Y satisfying the equation (ψ yEψ y for all ψ:ΣY);
2. whenever we have another map b:Γ→ Y (which is the same as a term b:Y with parameters from Γ) that has equal composites with the parallel pair (i.e. which satisfies the equation ψ bEψ b for all ψ), then we may introduce a map a:Γ→ X (term Γ⊢ a:X) that makes the triangles commute, so b = i a, and this is unique.

Not every idempotent E on ΣY can arise in this way from a Σ-split subspace, because the surjective part Σi of its splitting must be a homomorphism for the topological structure. In particular, it must preserve the four lattice connectives, but any order-preserving surjective function between lattices preserves ⊤ and ⊥ anyway. So the crucial condition is this:

Lemma 5.4 EI·ΣiY→ΣY satisfies the equations, for φ,ψ:ΣY,

 E(φ∧ψ)  =  E(Eφ∧ Eψ)   and   E(φ∨ψ)   =  E(Eφ∨ Eψ).         ▫

Definition 5.5 A term E that satisfies the equations in the Lemma is called a nucleus. In order to avoid developing a theory of dependent types, we do not allow E to have parameters.

The word “nucleus” was appropriated from locale theory, since both kinds of nuclei play the same role, namely to define subspaces, but the definitions are different. A localic nucleus, usually called j, must satisfy idj=j· j but need not be Scott-continuous [Joh82, §II 2]. Nuclei in ASD, on the other hand, are continuous but need not be order-related to id. So the common ground is when Eid and j is continuous: ASD and locale theory therefore agree on how to form closed subspaces, but not open ones or retracts.

In Section 8 we shall use E to define R as a subspace of the interval domain IR, and in this case E is a nucleus in both senses. If we view R instead as a subspace of Σ×Σ, but still defined by E, this is a nucleus only in the sense of ASD, not that of locale theory.

Notation 5.6 We write {YE} for the subspace XY that is defined by any nucleus E on Y. Beware, however, that this has very few of the properties of subset-formation in set theory.

Definition 5.7 A term a:Y (which may now involve parameters from a context Γ) of the larger space Y is called admissible with respect to the nucleus E if

 Γ,  ψ:ΣY ⊢ ψ a  ⇔  Eψ a.

This is the same as saying that the map a:Γ→ Y has equal composites with the parallel pair in the diagram in Remark 5.2, so it factors through the equaliser.

Since this equaliser is the subtype XY, we may then regard a as a term of type X or  {YE}. However, when we need to discuss the calculus in a formal way, we shall write admitY,E a for it, in order to disambiguate its type.

Remark 5.8 The simplest (and first, Section C 3) application of this calculus is to the construction of open and closed subspaces. This will formalise Remark 4.11.

Let θ:ΣY be a closed term (i.e. without parameters), which we think of as a continuous function θ:Y→Σ. The open and closed subspaces that θ (co)classifies are the inverse images U≡θ−1(⊤) and C≡θ−1(⊥) of the two points of the Sierpiński space (Remark 3.2).

Classically, any open subspace of U is already one of Y, whilst an open subspace of C becomes open in Y when we add U to it. This means that

 ΣU  ≅  ΣY↓θ  ≡  {ψ ∣ ψ⊑θ}   and   ΣC  ≅  θ↓ΣY  ≡  {ψ ∣ ψ⊒θ},

i.e. the parts of the lattice ΣY that lie respectively below and above θ. (The ↓ notation is used in category theory for “slice” or “comma” categories.)

From this we see what the Σ-splittings and nuclei for U and C must be. The construction of the interval domain IR⊂Σ×Σ in Section 7 will involve an open subspace, a closed one and a retract.

Lemma 5.9 Let e:YY be an idempotent and θ:Y→Σ any map. Then

 Σe,     θ∧(−)     and     θ∨(−)

are nuclei on Y, with respect to which a:Y is admissible iff respectively

 e a=a,       θ a⇔⊤     and     θ a⇔⊥.         ▫

Notation 5.10 As we shall need to name the Σ-splittings of j:U,CY, we write

 ∃j:ΣU↣ΣY     and     ∀j:ΣC↣ΣY,

where ∃jjψ)=ψ∧θ and ∀jjψ)=ψ∨θ. See [C] for the reasons for these names.

In Sections 7 and 8 we shall need to combine several nuclei. However, the intersection of two Σ-split subspaces need not exist, in general, and even if it does, it need not be Σ-split. Everything works if the nuclei commute, but this does not often happen. In fact, there are many situations in which E1· E2· E1=E1· E2, and that is sufficient to justify forming the intersection.

Lemma 5.11 Let E1 and E2 be nuclei on a type Y such that either E1· E2=E2· E1 or E1· E2· E1=E1· E2. Then E1· E2 is also a nucleus, and defines the intersection (pullback)

in which all five inclusions (including the composite) are Σ-split. Regarding {YE1}⊂ Y as the subset of admissible elements, and Σ{YE1} as the subset {ψ:ΣYE1ψ=ψ}, we see E1· E2 as a nucleus on {YE1} but not necessarily on {YE2}.         ▫

We have already said that nuclei and Σ-splittings are intimately related to the quantifiers that define compactness and overtness. The following two lemmas will provide the key to defining ∃ and ∀ from I in Section 10. There we shall use the slices Σ×Σ↓(δud) and (δdu)↓Σ×Σ, which we shall call lattices in this very specific context.

Lemma 5.12 Any lattice L is overt and compact, with ∃Φ≡Φ(⊤) and ∀Φ≡Φ(⊥).

Proof    By monotonicity, Φ(⊥)⇒Φ(x)⇒Φ(⊤) for any x:L.         ▫

Lemma 5.13 Let i:XL and IX↣ΣL with Σi· I=id. Then2

1. if I preserves ⊥ and L is overt then so is X, with ∃ x:Xx ≡ ∃ y:L.Iφ y, whilst
2. if I preserves ⊤ and L is compact then so is X, with ∀ x:Xx ≡ ∀ y:L.Iφ y.

Proof    In each column we deduce in both directions,

 Γ,  x:X ⊢ φ x ⇒ σ Γ,  x:X ⊢ σ ⇒ φ x Γ,  σ⇔⊥ ⊢ Σi(Iφ)  ≡  φ  =  ⊥:ΣX Γ,  σ⇔⊤ ⊢ ⊤  =  φ  ≡  Σi(Iφ):ΣX Γ,  σ⇔⊥ ⊢ Iφ  =  ⊥:ΣL Γ,  σ⇔⊤ ⊢ ⊤  =  Iφ:ΣL Γ,  σ⇔⊥ ⊢ ∃L(Iφ)  ⇒  ⊥ Γ,  σ⇔⊤ ⊢ ⊤  ⇒  ∀L(Iφ) Γ ⊢ ∃L(Iφ)  ⇒  σ Γ ⊢ σ ⇒ ∀L(Iφ)

using Axiom 4.7 and Definition 4.14.         ▫

It is high time we gave the actual rules that define subtypes and their admissible terms. These formally adjoin Σ-split subspaces to the calculus just as number theorists formally adjoin roots of particular polynomials to a field, or set theorists construct “equiconsistent” models that have altered properties. Theorem 15.8 describes the corresponding categorical construction.

As in type theory, we name the rules after the connective that they introduce or eliminate. Our connectives are called {} and Σ{}.

Axiom 5.14 The {}-rules of the monadic λ-calculus define the subspace itself:

These rules say that {YE} is the equaliser in Remark 5.2.

Axiom 5.15 The following Σ{}-rules say that {YE} has the subspace topology, where IY,E expands open subsets of the subspace to the whole space.

φ:Σ{Y ∣ E} ⊢ IY,Eφ:ΣY.          Σ
 ⎧ ⎨ ⎩ ⎫ ⎬ ⎭

E

The Σ{}I rule is derived from {}E0:

ψ:ΣY  ⊢      Σiψ  ≡  λ x:{Y ∣ E}.ψ(iY,E x):Σ{Y ∣ E}.          Σ
 ⎧ ⎨ ⎩ ⎫ ⎬ ⎭

I

The β-rule says that the composite Σi;IY↠Σ{YE}↣ΣY is E:

y:Y,  ψ:ΣY   ⊢   IY,E(λ x:{Y ∣ E}.ψ(iY,E x))y  ⇔  Eψ y.          Σ
 ⎧ ⎨ ⎩ ⎫ ⎬ ⎭

β

The η-rule says that the other composite Σ↠ΣY↠Σ{YE} is the identity:

φ:Σ{Y ∣ E},  x:{Y ∣ E}   ⊢   φ x   ⇔  IY,Eφ(iY,E x).           Σ
 ⎧ ⎨ ⎩ ⎫ ⎬ ⎭

η

This equation is the one in Definition 5.1 for a Σ-split subspace.

Remark 5.16 Notice that the Σ{}β-rule is the only one that introduces E into terms. This is something that we want to avoid if at all possible, given that the expressions for nuclei, such as E, which we intend to use to construct R, are usually very complicated. The normalisation theorem that eliminates unnecessary Es is proved in Section B 910.

When E does find its way into a program, it will give rise to a substantial computation. But this is what we would expect, considering the relationship to the quantifiers, and their computational meaning as optimisation and search (Section 2).

Warning 5.17 It is important to understand that, for another structure to admit a valid interpretation of this calculus, not only must the equaliser in Remark 5.2 exist, but there must also be a map I in the structure that satisfies the equations Σi· I=idΣX and I·Σi=E, cf. Remark 2.18.

Proposition 5.18

1. If Y is sober then so is {YE}, with focus{YE} Q = admitY,E(focusY2 iY,E Q)).
2. If X is also sober and has maps f:XY and FX→ΣY with Σf· F=idΣX and F·Σf=E then X≅{YE}, where
 x:X ⊢ x′≡admitY,E(f x):{Y ∣ E} x′:{Y ∣ E} ⊢ x≡focusX(λφ:ΣX.Fφ(i x′)):X.
In particular, f is the equaliser in Remark 5.2.         ▫

Remark 5.19 If this paper is the first one about ASD that you have seen, you may reasonably imagine that we have cooked up the rules from the observations in Section 2, based on little more than the properties of the real line that first year undergraduates learn. Can this theory of topology even be generalised to ℝn? Is it of any use in proving theorems in mathematics other than those that we have mentioned?

Actually, we have told the story so far in reverse historical order. The calculus above was derived from a categorical intuition, and when it was formulated [B], it was a solution in search of a problem. There were no clear ideas of how the real line might be constructed, and certainly no inkling that it might behave in ASD in a radically different way from the established theory of Recursive Analysis (Section 15). That it turned out to do so is a tribute to category theory as a source of, or rather as a way of communicating, mathematical intuitions.

For reference we give a summary of some of the constructions that have been performed using nuclei in the infrastructure of ASD.

Theorem 5.20 Σ-split subspaces interact with the underlying structure of products and exponentials as follows, and also provide stable disjoint unions Section B 11.

 X ≅ {ΣΣX ∣ λF F.F(λ x.F(λφ.φ x))} {X ∣ E0} × {Y ∣ E1} ≅ {X× Y ∣ E1X· E0Y} Σ{X ∣ E} ≅ {ΣX ∣ ΣE} {{X ∣ E1} ∣ E2} ≅ {X ∣ E2} {X ∣ E0}+{Y ∣ E1} ≅ {ΣΣX×ΣY ∣ E} where   EH H ≡ H<λ x.H(λφψ.E0φ x), λ y.H(λφψ.E1ψ y)>.         ▫

In Section 8, we shall need to perform some combinatorial arguments using lists of rational numbers. However, since ASD is a direct axiomatisation of topology, without using set theory, we have to recover some kind of “naïve set theory” within our category of spaces. Our “sets” are the overt discrete objects.

Theorem 5.21 The full subcategory consisting of the overt discrete objects has

1. finite products (1 and ×);
2. equalisers;
3. stable disjoint coproducts (0 and +);
4. stable effective quotients of open equivalence relations [C]; and
5. free monoids or “sets of lists”, List (X) [E].

This categorical structure is called an arithmetic universe.         ▫

Remark 5.22 We shall rely on this result to provide the “discrete mathematics” that we need, namely

1. the usual arithmetic operations on ℕ, ℤ and ℚ;
2. the operations of naïve set theory over these types, including, for example, the use of lists and (Kuratowski-) finite sets; and
3. both quantifiers over finite sets, i.e. finite conjunctions and disjunctions, which have well known definitions using primitive recursion.

The infinite objects that are generated in this way are countable in the strict sense of being bijective with a decidable subset of ℕ in the calculus; since our isomorphisms are homeomorphisms, such objects inherit =, ∃, and in some cases ≠, from ℕ.

These “sets” do not admit a full powerset on the basis of the axioms that we have given here, and therefore they do not form an elementary topos or model of set theory. However, it is possible to add another (much more powerful, and certainly non-computational) axiom to ASD that does make the full subcategory of overt discrete objects into a topos. This axiom asserts that this subcategory is co-reflective, i.e. that the inclusion has a right adjoint, which formally assigns an overt discrete object to any space, and we call this object the “underlying set” of the space [H]. We do not use this axiom in this paper.

Remark 5.23 In order to formulate the definition of Σ-split subspace we only need powers Σ(−), not the lattice structure on Σ or the quantifiers. The category-theoretic summary of this section is that we require the adjunction Σ(−)⊣Σ(−) to be monadic.

The notions of sobriety and Σ-split subspaces in ASD come from the two conditions in the theorem of Jon Beck (1966) that characterise monadic adjunctions [Tay99, Theorem 7.5.9]. Sobriety says that Σ(−) reflects invertibility (Proposition 4.23). Nuclei are essentially the same as Σ(−)-contractible equalisers; Axiom 5.14 says that such equalisers exist, and Axiom 5.15 that Σ(−) takes them to coequalisers. These conditions are given as equations between higher-order λ-terms in [A][B].

In the presence of the other topological structure in the previous section, in particular Scott continuity, the equations that define a nucleus are equivalent to the much simpler ones involving finitary ∧ and ∨ that we gave in Lemma 5.4 and Definition 4.22 [Section G 10]. In this setting, any definable object X of ASD can be expressed as a Σ-split subspace, i:X↣Σ, where i and I correspond directly to a basis of open subspaces and related compact subspaces. Locally compact spaces and computably continuous functions between them can then be understood directly in ASD [G]. This calculus is how we implement the foundations of recursive analysis and topology based on open sets instead of points.

However, the introduction of nuclei with this definition after the lattice theory in the previous section is the reason why our discussion of open and closed subspaces and the Phoa principle in Remark 4.11 was deductively unsatisfactory. From a foundational point of view, the monadic structure should really come first. Then the Euclidean principle (σ∧ Fσ⇔σ∧ F⊤), which is the part of the Phoa principle that applies to intuitionistic set theory or the subobject classifier in an elementary topos, is exactly what is required to make Eφ≡φ∧θ a nucleus in the abstract sense, or equivalently to justify the first of the two Gentzen-style rules. This is essentially how this principle was discovered [Section C 3].

The results that we have sketched here are treated in greater detail in the earlier papers that developed ASD. The foundations of the theory, together with the methodology and motivations behind it, are surveyed in [O].