Theory and Applications of Categories, Vol. 28, No. 32, 2013, pp. 1139–1152.

THE GLEASON COVER OF A REALIZABILITY TOPOS

PETER JOHNSTONE

Abstract. Recently Benno van den Berg [1] introduced a new class of realizability toposes which he christened Herbrand toposes. These toposes have strikingly different properties from ordinary realizability toposes, notably the (related) properties that the ‘constant object’ functor from the topos of sets preserves finite coproducts, and that De Morgan’s law is satisfied. In this paper we show that these properties are no accident: for any Schönfinkel algebra Λ, the Herbrand realizability topos over Λ may be obtained as the Gleason cover (in the sense of [8]) of the ordinary realizability topos over Λ. As a corollary, we obtain the functoriality of the Herbrand realizability construction on the category of Schönfinkel algebras and computationally dense applicative morphisms.

1. Introduction

Realizability toposes were first introduced by Martin Hyland in the late 1970s [7, 6] and many particular examples have now been extensively studied (see for example [16]). However, whilst the 2-category of Grothendieck toposes, geometric morphisms and natural transformations between them has long been well understood, there has been relatively little progress until recently on understanding the structure of geometric morphisms between realizability toposes. Indeed, such results as have been established have tended to be negative in character (e.g., if E is a realizability topos and F is a Grothendieck topos then there are no geometric morphisms E → F, and (up to isomorphism) only one morphism F → E, namely that which factors through Set), and have tended to raise doubts about whether the well-developed techniques for studying geometric morphisms actually have any utility in the world of realizability. The present paper is perhaps the first to show that a nontrivial geometric construction developed for Grothendieck toposes (specifically, the Gleason cover, introduced — at about the same time as realizability toposes — by the present author [8]) does have a significant rôle to play in this world.

As in [11], we use the term Schönfinkel algebra for what most people call a partial combinatory algebra: that is, a set Λ equipped with a partial binary operation (denoted by juxtaposition) and constants K and S such that Kλμ = λ for all λ and μ, and Sλμν = λν(μν) whenever λν(μν) is defined. For simplicity, we shall assume that all Schönfinkel algebras we consider are proper in the sense that Sλμ is always defined; but we shall not require them to be strict in the sense that Sλμν is defined only when λν(μν) is defined.

Received by the editors 2013-09-26 and, in revised form, 2013-12-03.

Transmitted by Ieke Moerdijk. Published on 2013-12-12.

2010 Mathematics Subject Classification: Primary 18B25. Secondary 03G30.

Key words and phrases: realizability topos, De Morgan topos, Gleason cover.

\begin{matrix}c \\ ◯ \end{matrix} Peter Johnstone, 2013. Permission to copy for private use granted.

We shall make free use of the combinators I, B, E which respectively correspond to the closed λ-terms λx.x, λxyz.x(yz) and λxy.yx; of the pairing combinator D corresponding to λxyz.zyx and the unpairing combinators P_{1} = E(KI) and P_{2} = EK (note that P_{1}(Dλμ) = λ and P_{2}(Dλμ) = μ for all λ and μ); and of the Church numerals C_{n} corresponding to λxy.x(x(⋯ (xy) ⋯)) where x appears n times in the body of the term.

We recall briefly the construction of a topos from a tripos, which is described in greater detail in [7] and in [16]. By a tripos on Set, we mean a Set-indexed preorder 𝕋 = (A ↦ T^{A}), such that (a) each preorder T^{A} is a Heyting prealgebra (i.e., its poset reflection is a Heyting algebra), and the transition functors u^{∗}: T^{A} → T^{B} induced by morphisms u: B → A in Set preserve this structure; (b) 𝕋 is complete and cocomplete (i.e., the functors u^{∗} have left and right adjoints ∃_{u} and ∀_{u} satisfying the Beck–Chevalley conditions); and (c) 𝕋 has an exemplary element, i.e. an element σ ∈ T^{Σ} for some set Σ, such that every element of T^{A} (for any A) is isomorphic to u^{∗}(σ) for some (not necessarily unique) u: A → Σ. In all the examples we consider, the elements of T^{A} will be actual functions from A to a fixed set T, the functors u^{∗} will be induced by composition (so that the exemplary element may be taken to be 1_{T}), the Heyting prealgebra structure will be induced by suitable operations on T, and the quantifiers will be defined ‘pointwise’ in the sense that ∃_{u}f(a) and ∀_{u}f(a) depend only on the set {f(b) | u(b) = a} (so that the Beck–Chevalley conditions are automatic). (In fact there is no loss of generality in assuming that these conditions on 𝕋 are always satisfied, see [7].)

Such a structure gives rise to an allegory (in the sense of [3]) whose objects are sets, and whose morphisms A ↬ B are isomorphism classes of elements of T^{A×B}, the composition of [ϕ: A ↬ B] and [ψ: B ↬ C] being given by [ψ ∘ ϕ], where

(ψ ∘ ϕ)(a, c) = ∃_{b}(ϕ(a, b) ∧ ψ(b, c)) .

The topos Set⟨𝕋⟩ is obtained from this allegory by splitting all symmetric idempotents and then cutting down to the subcategory of maps: more specifically,

1.1. Definition.

(i) An object of Set⟨𝕋⟩ is a pair (A, δ) where A is a set and δ: A × A → T is ‘symmetric and transitive in the logic of 𝕋’, i.e. the inequalities δ(a, a′) ≤ δ(a′, a) and (δ(a, a′) ∧ δ(a′, a′′)) ≤ δ(a, a′′) hold in T^{A×A} and T^{A×A×A} respectively.

(ii) Morphisms (A, δ) → (B, ϵ) are named by functions F: A × B → T which are extensional, strict, single-valued and total in the sense that the inequalities

(δ(a′, a) ∧ F (a, b) ∧ ϵ(b, b′)) ≤ F (a′, b′) ,
F (a, b) ≤ (δ(a, a) ∧ ϵ(b, b)) ,
(F (a, b) ∧ F (a, b′)) ≤ ϵ(b, b′) and
δ(a, a) ≤ ∃_{b}F (a, b)

hold; and two such functions name the same morphism iff they are isomorphic as elements of T^{A×B}.

We omit the detailed verification that Set⟨𝕋⟩ is indeed a topos (the reader may find it in [7] or [16]), but we note for future reference that its subobject classifier Ω is the object (T,⇔) where ⇔ denotes the Heyting bi-implication.

1.2. Examples.

(a) The tripos corresponding to ordinary realizability, over a Schönfinkel algebra Λ, is obtained by taking T to be the power-set P Λ, with Heyting operations given by

(p⇒q) = {λ ∈ Λ | for all μ ∈ p, λμ is defined and λμ ∈ q} ,
(p ∧ q) = {Dλμ | λ ∈ p and μ ∈ q} and
(p ∨ q) = {DKλ | λ ∈ p} ∪ {D(KI)μ | μ ∈ q} .

The preorder on P Λ^{A} is the ‘uniform’ ordering given by f ≤ g iff ⋂{(f(a)⇒g(a)) | a ∈ A} is inhabited; and the quantifiers are given by ∃_{u}f(a) = ⋃{f(b) | u(b) = a} and ∀_{u}f(a) = ⋂{(Λ⇒f(b)) | u(b) = a}. We denote this tripos by ℙΛ.

(b) Given a frame (i.e., a complete Heyting algebra) L, we write 𝕃 for the tripos in which L^{A} is the set of all maps A → L, with pointwise ordering. The topos Set⟨𝕃⟩ is simply the topos of L-valued sets (equivalently, of sheaves on L for the canonical coverage; cf. [10], C1.3.11). In particular, it is a Grothendieck topos.

By a geometric morphism f: 𝕋 → 𝕊 of triposes, we mean an adjoint pair of indexed functors (f^{∗}: 𝕊 → 𝕋 ⊣ f_{∗}: 𝕋 → 𝕊), of which the left adjoint f^{∗} additionally preserves finite meets. Given such an adjunction, it is easy to see that the mapping ((A, δ) ↦ (A, f^{∗}δ)) defines the object-map of a functor (also denoted f^{∗}) from Set⟨𝕊⟩ to Set⟨𝕋⟩, whose effect on morphisms is similarly given by ([F] ↦ [f^{∗}F]); and this functor preserves finite limits. In general, f_{∗} does not induce a functor in the same simple-minded way, since it need not commute with existential quantification; thus, although (A, f_{∗}δ) is an object of Set⟨𝕊⟩ whenever (A, δ) is an object of Set⟨𝕋⟩, and f_{∗}F is extensional, strict and singlevalued whenever F represents a morphism of Set⟨𝕋⟩, it may fail to be total since the definition of totality involves an existential quantifier. Fortunately, however, there is a ‘weak completion’ process for objects of Set⟨𝕋⟩, such that every object is isomorphic to its weak completion, and f_{∗} does preserve totality of functions representing morphisms whose codomain is weakly complete. Specifically, we say (B, ϵ) is weakly complete if, for any (A, δ) and any F: A × B → T representing a morphism (A, δ) → (B, ϵ), there exists a function f: A → B in Set for which ∃_{b}F (a, b) ≅ F (a, f(a)) in T^{A}. (The word ‘weakly’ is a reminder that we do not, and cannot reasonably, demand that the function f should be unique.) The following result is well known, but does not seem to be in the literature.

1.3. Lemma. The object Ω is weakly complete.

Proof. Recall that Ω = (T,⇔). If F: A × T → T represents a morphism (A, δ) → Ω, then from the fact that it is extensional and single-valued we deduce

F (a, t) ≤ (F (a, ⊤)⇔(t⇔⊤)) ;

but (t ⇔ ⊤) is isomorphic to t, and hence we have F (a, t) ≤ F (a, F (a, ⊤)) by a further application of extensionality. So we may take f(a) to be F (a, ⊤).

We define f_{∗}: Set⟨𝕋⟩ → Set⟨𝕊⟩ by setting f_{∗}(A, δ) = (Ã, f_{∗}δ̃) where (Ã, δ̃) is a weak completion of (A, δ); it is then straightforward to verify that this yields a right adjoint for f^{∗} at the topos level. In other words, every geometric morphism of triposes 𝕋 → 𝕊 induces a geometric morphism of toposes Set⟨𝕋⟩ → Set⟨𝕊⟩. We do not assert that every geometric morphism between toposes of the form Set⟨𝕋⟩ arises in this way — although that is the case if both triposes are induced by frames as in 1.2(b), and it was recently shown [11] that the same is true if they are both induced by Schönfinkel algebras as in 1.2(a).

For future reference, we note also that if f: 𝕋 → 𝕊 is a reflection (i.e., the counit of (f^{∗} ⊣ f_{∗}) is an isomorphism), then the counit of the induced geometric morphism of toposes is also an isomorphism, i.e. the latter is an inclusion. If the morphism of triposes is a coreflection, we cannot conclude the same condition for the induced morphism of toposes (unless f_{∗} happens to commute with existential quantification, so that its extension to Set⟨𝕋⟩ may be defined in the ‘simple-minded’ way); but we can say that f^{∗}: Set⟨𝕊⟩ → Set⟨𝕋⟩ is faithful, since it reflects isomorphisms between the functions representing morphisms of Set⟨𝕊⟩ — in other words, the induced geometric morphism of toposes is a surjection.

Given a tripos 𝕋, we write L_{T} (or simply L) for the Heyting algebra obtained from T^{1} by identifying isomorphic elements, and q: T → L_{T} for the quotient map. If e: L_{T} → T denotes ∃_{q}(1_{T}), we say that 𝕋 has standard existential quantification (briefly, 𝕋 is ∃- standard) if qe = 1_{L}. (If existential quantification is pointwise, so that it is in effect induced by a join map ⋁: P T → T, this is equivalent to saying that the join of each isomorphism class is a member of the class.) It is shown in [7] that if this condition holds, then L is a frame, and the pair (q, e) induces a geometric morphism of triposes 𝕃 → 𝕋. So we obtain a geometric morphism (in fact an inclusion) Set⟨𝕃⟩ → Set⟨𝕋⟩. If in addition 𝕋 is two-valued (that is, L_{T} has only two isomorphism classes [⊤] and [⊥]), this becomes a geometric inclusion Set → Set⟨𝕋⟩; since it is clearly dense (i.e., its direct image preserves the initial object) and Set is Boolean, it identifies Set with the subtopos sh_{¬¬}(Set⟨𝕋⟩). Given a set A, we write ∇A for A considered as a ¬¬-sheaf in Set⟨𝕋⟩; it may be identified with (A, Δ) where Δ(a, a) = e([⊤]) for all a ∈ A, and Δ(a, a′) = e([⊥]) if a ≠ a′. (The reader should be warned that this functor does not always coincide with the functor Set → Set⟨𝕋⟩ which is denoted ∇ in [16]: it does so for an ordinary realizability topos, but not for a Herbrand realizability topos.) All the triposes that we consider in this paper are ∃-standard, and the majority of them (including ℙΛ) are two-valued.

Ordinary realizability toposes are decidedly non-classical. It has been known for some time that an ordinary realizability topos does not admit any geometric morphism to a Boolean topos, but the following stronger result has not been published before. Recall that a geometric morphism f: F → E is said to be skeletal [9] if f_{∗} maps ¬¬-sheaves to ¬¬- sheaves; of course, any morphism with Boolean codomain is skeletal, and it was shown in [11] that any geometric morphism between ordinary realizability toposes is skeletal. More generally, if 𝕊 and 𝕋 are two-valued ∃-standard triposes, then any geometric morphism Set⟨𝕋⟩ → Set⟨𝕊⟩ which is induced by a geometric morphism of triposes is skeletal, since the triangle

\xymatrix{2 \ar[r] \ar[dr] & 𝕋 \ar[d] \\  & 𝕊}

clearly commutes.

1.4. Lemma. Let Λ be a Schönfinkel algebra. Then there is no skeletal geometric morphism f: Set⟨ℙΛ⟩ → E where E satisfies De Morgan’s law.

Proof. Suppose given such a morphism f; then since f_{∗}(0) is a ¬¬-sheaf and hence a complemented subterminal object of E, we see that the image of f is dense in a clopen subtopos of E, and hence also satisfies De Morgan’s law. And the surjective part of the image factorization of f is still skeletal ([9], 3.5(i)); thus we may reduce to the case when f itself is surjective. For any set A, f_{∗}(∇A) is a ¬¬-sheaf and hence decidable in E ([10], D4.6.2(v)), so that f^{∗}f_{∗}(∇A) is decidable in Set⟨ℙΛ⟩ and hence a modest assembly ([16], p. 153). Now E (1, f_{∗}(∇A)) injects into Set⟨ℙΛ⟩ (1, f^{∗}f_{∗}(∇A)), and thus has cardinality bounded by that of Λ, since distinct morphisms into a modest assembly must be tracked by distinct elements of Λ. But we also have E (1, f_{∗}(∇A)) ≅ Set⟨ℙΛ⟩ (1, ∇A) ≅ A; taking A to be the power-set of Λ, we obtain a contradiction.

2. Herbrand Realizability

Herbrand realizability, introduced by Benno van den Berg in [1], may be viewed as a further modification of modified realizability (for which see [14]); it resembles the latter in that propositions come equipped with two sets p and a of ‘potential’ and ‘actual’ realizers, but differs in that the actual realizers are not individual members of p but are (in effect) finite subsets of p. To this end, we need to suppose that our Schönfinkel algebra is equipped with a notion of coding, not just for pairs, but for arbitrary finite sequences; of course, the latter may easily be constructed from the D-combinator and the Church numerals, but in particular cases there may be simpler ways of achieving it — for example, if Λ has underlying set ℕ, we may code a finite sequence (n_{1}, …, n_{k}) by the number 2^{n_{1}+1}3^{n_{2}+1} ⋯ p_{k}^{n_{k}+1}, where p_{k} denotes the kth prime. We write ⟨λ_{1}, …, λ_{k}⟩ for the element coding the sequence (λ_{1}, …, λ_{k}) (and ⟨⟩ for the element coding the empty sequence), and if λ codes a sequence we shall write |λ| for the length of this sequence and λ_{i} for its ith term (it being understood that λ_{i} may be undefined if i > |λ|). We shall also write λ ∗ μ for the element coding the concatenated sequence (λ_{1}, …, λ_{|λ|}, μ_{1}, …, μ_{|μ|}). We assume that the coding function (λ_{1}, …, λ_{k}) ↦ ⟨λ_{1}, …, λ_{k}⟩, the projection functions (−)_{i}, the function λ ↦ C_{|λ|}, and the function (λ, μ) ↦ λ ∗ μ are all recursive — that is, they are ‘tracked’ by suitable elements of Λ.

Given a set p ⊆ Λ, we shall write !p for the set of codes for finite sequences (of arbitrary length) whose members all belong to p. Note that ⟨⟩ ∈!p for any p; we shall also write !^{+}p for the set of codes for nonempty sequences of members of p. We preorder !p by setting λ ⪯ μ if every term in the sequence coded by λ also occurs in that coded by μ (but not necessarily in the same order). (The partial order reflection of !p is of course isomorphic to the free join-semilattice Kp, i.e. the set of finite subsets of p.) A realizer λ for (p⇒q) easily yields a realizer !λ for (!p ⇒!q), given by (!λ)μ = ⟨λμ_{1}, …, λμ_{|μ|}⟩. In fact the mapping p ↦!p defines an indexed monad on the indexed preorder ℙΛ; we shall not make explicit use of this structure, but we reserve the letters ι and υ for elements of Λ coding the recursive functions Λ →!Λ and !!Λ →!Λ which yield the unit and multiplication of this monad, namely λ ↦ ⟨λ⟩ and

⟨μ_{1}, μ_{2}, …, μ_{n}⟩ ↦ μ_{1} ∗ μ_{2} ∗ ⋯ ∗ μ_{n} .

Note also that ι and (−)_{1} are uniform realizers for the implications (p⇒!^{+}p) and (!^{+}p⇒p) respectively.

We shall use the ‘exponential isomorphism’ linking !(−) to the join and meet operations of ℙΛ:

2.1. Lemma. The implications !(p ∨ q) ⇒ (!p ∧!q) and (!p ∧!q) ⇒!(p ∨ q) are uniformly realizable.

Proof. Given an element λ of !(p ∨ q), we map it to Dμν, where μ codes the sequence of those elements P_{2}λ_{i} (i ≤ |λ|) for which P_{1}λ_{i} = K, and ν similarly codes the sequence of those P_{2}λ_{i} for which P_{1}λ_{i} = KI. In the opposite direction, given an element Dμν of (!p ∧!q), we map it to (!(DK)μ) ∗ (!(D(KI))ν). It is easy to see that both these mappings are recursive — that is, they may be ‘tracked’ by elements of Λ.

The mappings constructed above are not literally inverse to each other, but they are inverse modulo the equivalence relation induced by the preorder ⪯; so in what follows — where we are primarily interested in (upwards-closed, and hence) equivalence-closed subsets of sets of the form !p — we shall regard them as entitling us to identify !(p ∨ q) with !p ∧!q.

We now define HΛ to be the set of pairs (p, a) where p ⊆ Λ and a is an upwards-closed subset of !p. (The idea is that, if we have specified enough potential realizers to give an actual realization of some proposition, we cannot destroy it by adding more potential realizers.) For any set A, we preorder the set HΛ^{A} by setting f ≤ g if the implications (!f_{1}(a) ⇒!g_{1}(a)) and (f_{2}(a) ⇒ g_{2}(a)) are simultaneously realized, uniformly in a (where we write f_{1}(a) and f_{2}(a) for the first and second components of f(a)).

We define meet and join operations on HΛ by setting

\begin{aligned}((p, a) ∧ (q, b)) & = & ((p ∨ q), (a ∧ b)) and \\ ((p, a) ∨ (q, b)) & = & ((p ∨ q), (a∧!q) ∪ (!p ∧ b)) \end{aligned}

(note the use we have made of the exponential isomorphism); and the implication is given by

((p, a)⇒(q, b)) = ((!p⇒!q), c) ,

where c the set of codes for sequences which contain at least one term in (a⇒b).

2.2. Proposition. The above definitions make HΛ^{A} into a Heyting prealgebra for any set A, and the indexed preorder ℍΛ = (A ↦ HΛ^{A}) into a tripos.

We omit the proof, whose details may be found in [1]. However, we note that existential quantification in ℍΛ is given by taking ∃_{u}f(a) to have as its first component ⋃{!f_{1}(b) | u(b) = a}, and as its second component the set of codes for sequences which contain an element of f_{2}(b) for some b with u(b) = a. It follows that ℍΛ is ∃-standard as well as twovalued (the two isomorphism classes in HΛ^{1} consist of those pairs (p, a) with a inhabited, and those with a = ∅), so as usual we have a geometric inclusion Set → Set⟨ℍΛ⟩, representing the former as the subcategory of ¬¬-sheaves in the latter. However, the most striking difference between Herbrand and ordinary (or modified) realizability lies in the fact that the direct image functor ∇ preserves finite coproducts; hence, by [10], D4.6.2(xiii), Set⟨ℍΛ⟩ satisfies De Morgan’s law. (Once again, we refer to [1] for the proof.)

3. A Tale of Three Triposes

In [14], Jaap van Oosten showed that, at least when Λ is the Kleene algebra, the modified realizability topos over Λ may be identified with a closed subtopos of an ordinary realizability topos over the Sierpiński topos [2, Set], whose open complement is the ordinary realizability topos Set⟨ℙΛ⟩. Fortunately, thanks to the theorem of A.M. Pitts on iterated tripos extensions (see [16], 2.7.1), we do not have to concern ourselves here with internal Schönfinkel algebras in [2, Set], since the ordinary realizability topos which we need can also be presented as Set⟨ℙ_{1}Λ⟩ for a suitable tripos ℙ_{1}Λ on Set. Specifically, P_{1}Λ is the set {(p, q) ∈ P Λ × P Λ | q ⊆ p}, with Heyting operations defined by

\begin{aligned}(p, q) ∧ (p′, q′) & = & (p ∧ p′, q ∧ q′) , \\ (p, q) ∨ (p′, q′) & = & (p ∨ p′, q ∨ q′) and \\ (p, q)⇒(p′, q′) & = & ((p⇒p′), (p⇒p′) ∩ (q ⇒q′)) \end{aligned}

and preordering on P_{1}Λ^{A} defined by f ≤ g iff ⋂{(f(a) ⇒ g(a))_{2} | a ∈ A} is inhabited. The verification that this yields a tripos (with quantifiers, like join and meet, defined ‘componentwise’) is straightforward. We note in passing that ℙ_{1}Λ, though ∃-standard, is not two-valued: in addition to [⊤] and [⊥], there is a third isomorphism class in P_{1}Λ^{1}, consisting of those pairs (p, ∅) with p ≠ ∅.

Between ℙΛ and ℙ_{1}Λ, we have a string of five indexed adjoint functors (f_{1} ⊣ f_{2} ⊣ f_{3} ⊣ f_{4} ⊣ f_{5}), induced respectively by composition with (p ↦ (p, ∅)), ((p, q) ↦ p), (p ↦ (p, p)), ((p, q) ↦ q) and (p ↦ (Λ, (Λ ⇒ p))). (The adjunctions are all trivial to verify except for the last: if λ realizes (q ⇒r), then B(Bλ)K realizes ((p, q)⇒(Λ, (Λ⇒r))), and if μ realizes ((p, q) ⇒ (Λ, (Λ ⇒ r))), then B(EK)μ realizes (q ⇒ r).) Although f_{1} does not preserve the top element, it does preserve binary meets, and hence composition with it defines a full embedding Set⟨ℙΛ⟩ → Set⟨ℙ_{1}Λ⟩, whose image consists of those objects (A, δ) such that the second component of δ(a, a′) is empty for all a, a′. But these are exactly the objects admitting a morphism to the unique nontrivial subterminal object U of Set⟨ℙ_{1}Λ⟩ (which may be taken to be ({∗}, δ) where δ(∗, ∗) = (p, ∅) for some inhabited p); so we may identify Set⟨ℙΛ⟩ with Set⟨ℙ_{1}Λ⟩/U, in such a way that the functor induced by f_{1} is identified with Σ_{U} — and hence the functors induced by f_{2} and f_{3} are identified with U^{∗} and Π_{U} respectively, i.e. they form an open geometric inclusion u: Set⟨ℙΛ⟩ → Set(ℙ_{1}Λ⟩.

The open inclusion u has a left adjoint g: Set(ℙ_{1}Λ⟩ → Set⟨ℙΛ⟩ induced by f_{3} and f_{4}, and this in turn has a left adjoint v: Set⟨ℙΛ⟩ → Set(ℙ_{1}Λ⟩ induced by f_{4} and f_{5}. Since v is an inclusion (equivalently, g is connected), g is a local geometric morphism in the sense of [12].

3.1. Lemma. The inclusions u and v define disjoint subtoposes of Set⟨ℙ_{1}Λ⟩.

Proof. The local operators j and k on ℙ_{1}Λ corresponding to u and v are respectively given by (p, q) ↦ (p, p) and (p, q) ↦ (Λ, (Λ ⇒ q)); we have to show that the join (m, say) of these two operators is isomorphic to (p, q) ↦ (Λ, Λ). But this is easy, since the idempotency of m yields jk ≤ m, and the composite jk is exactly (p, q) ↦ (Λ, Λ).

An alternative proof of 3.1 could be given by observing that v_{∗}(0) is the subterminal object U; recall that, for any geometric morphism f, f_{∗}(0) is the open complement of the closure of the image of f.

As we remarked above, in [14] Jaap van Oosten identified the closed complement of the open subtopos u as the modified realizability topos Set⟨𝕄Λ⟩ over Λ, at least in the case when Λ is the (first) Kleene algebra. Moreover, by 3.1 the non-open inclusion v factors through this closed subtopos; hence the composite Set⟨𝕄Λ⟩ → Set⟨ℙ_{1}Λ⟩ → Set⟨ℙΛ⟩ is still local.

More recently, van Oosten [private communication] observed:

3.2. Lemma. There is a geometric inclusion w: Set⟨ℍΛ⟩ → Set⟨ℙ_{1}Λ⟩. Moreover, this subtopos is disjoint from u.

Proof. w is induced by a geometric morphism of triposes whose direct image is ((p, a) ↦ (!p, a)) and whose inverse image is ((p, q) ↦ (p, s(p, q))) where s(p, q) ⊆!p is the set of codes for sequences containing at least one term in q. It is easy to see that both these maps are order-preserving. If λ realizes ((p, s(p, q))⇒(r, a)), then Bλι realizes ((p, q)⇒(!r, a)); and conversely if μ realizes ((p, q) ⇒ (!r, a)) then Bυ(!μ) realizes ((p, s(p, q)) ⇒ (r, a)). A realizer for the fact that w^{∗} preserves binary meets is given by a code for the function sending Dλμ (where λ and μ code sequences of lengths m and n respectively) to the code for the sequence of length mn whose (rn + s)th term is Dλ_{r+1}μ_{s}. And ι realizes (1 ≤ w^{∗}w_{∗}), so the adjunction is a reflection.

For the second assertion, we again consider the composite jl, where l is the local operator ((p, q) ↦ (!p,!^{+}p)) corresponding to w. We have jl(p, q) = (!p,!p) for all (p, q); and since ⟨⟩ ∈!p for all p this is isomorphic to the constant function with value (Λ, Λ).

The composite h = gw is not a local morphism: the left adjoint v of g cannot factor through w by 1.4, since such a factorization would be (a dense inclusion, and hence) skeletal. But it is surjective, since it corresponds to the geometric morphism of triposes given by ((p, a) ↦ a) and (p ↦ (p,!^{+}p)), and as we observed earlier the inequality h_{∗}h^{∗}(p) ≤ p is realized by (−)_{1}.

3.3. Lemma. h: Set⟨ℍΛ⟩ → Set⟨ℙΛ⟩ is a closed map.

Proof. By the tripos version of [10], C3.2.1, it suffices to verify the ‘co-Frobenius’ condition

(h_{∗}((p, a) ∨ h^{∗}(q))⇔(h_{∗}(p, a) ∨ q)) .

But the two sides reduce to (a ∧!q) ∪ (!p ∧!^{+}q) and to (a ∨ q) respectively; so a realizer for the left-to-right implication is given by a code for the function sending Dλμ to DKλ if μ = ⟨⟩ and to D(KI)μ_{1} otherwise, and the right-to-left implication is realized by a code for the function sending Dλμ to Dμ⟨⟩ if λ = K, and to D⟨⟩(ιμ) if λ = KI.

4. Herbrand Realizability as a Gleason Cover

The Gleason cover construction takes its name from a paper by A.M. Gleason [4], in which he showed how to construct a ‘best possible’ covering of an arbitrary compact Hausdorff space by an extremally disconnected one. This construction was subsequently extended to larger classes of spaces by various authors, and in [8] the present author showed that it may be extended to arbitrary toposes. Given a topos E, its Gleason cover γE is defined to be the topos of E-valued sheaves on the internal frame Idl(Ω_{¬¬}) of ideals of the complete Boolean algebra Ω_{¬¬} in E. γE always satisfies De Morgan’s law, and it comes equipped with a geometric morphism f: γE → E which is a proper separated map and a minimal localic surjection; moreover, γE is characterized up to equivalence in Top/E by these properties (see [10], D4.6.8). The morphism f is also skeletal (indeed, it restricts to an equivalence between categories of ¬¬-sheaves), and the construction E ↦ γE may be viewed as a right adjoint to the inclusion, in the 2-category of toposes and skeletal geometric morphisms, of the full sub-2-category of toposes satisfying De Morgan’s law ([10], D4.6.12).

In our present context, the domain of h: Set⟨ℍΛ⟩ → Set⟨ℙΛ⟩ satisfies De Morgan’s law; h is skeletal (either by direct computation, or by the argument of Lemma 2.1 in [11]) and localic (as are all morphisms induced by geometric morphisms of triposes), and it is minimal surjective since the only proper closed subtopos of its domain is the degenerate topos. So, in order to identify it with the Gleason cover of Set⟨ℙΛ⟩, it would suffice to show that it is proper and separated. As we saw in 3.3, it is a closed map, which is one part of propriety; the other is preservation of filtered Set⟨ℙΛ⟩-indexed colimits by its direct image. Although filtered colimits in realizability toposes were studied by van Oosten in [15], we have chosen not to follow this route, but instead to argue directly to show that the internal frame in Set⟨ℙΛ⟩ which corresponds to h is isomorphic to the frame of ideals of Ω_{¬¬} = ∇2.

Since Ω is weakly complete in Set⟨ℍΛ⟩ by 1.3, we may compute h_{∗}(Ω) in the ‘simpleminded’ way: that is, its underlying set is simply HΛ, with P Λ-valued equality predicate obtained by applying h_{∗} to the HΛ-valued predicate ⇔ (that is, by forgetting the first coordinate of the latter). We have to show that this object is isomorphic to Idl(∇2) in Set⟨ℙΛ⟩.

Of course, an ideal I ↣ ∇2 is completely determined by a pair of truth-values (= subsets of Λ) p = [[0 ∈ I]] and q = [[1 ∈ I]]; but the assertion that these truth-values define an ideal involves realizers for the assertions that I is downwards closed and closed under finite joins — i.e., we must be given specified realizers α ∈ [[0 ∈ I]] = p,

β ∈ ⋂{([[i ∈ I]]⇒[[j ∈ I]]) | i ≥ j} = (p⇒p) ∩ (q ⇒p) ∩ (q ⇒q) , and
γ ∈ ⋂{(([[i ∈ I]] ∧ [[j ∈ I]])⇒[[i ∨ j ∈ I]]) | i, j ∈ 2}
= ((p ∧ p)⇒p) ∩ (p ∧ q)⇒q) ∩ ((q ∧ p)⇒q) ∩ ((q ∧ q)⇒q) .

We note that if (p, a) is any element of HΛ then the pair (!p, a) carries this structure, with α = ⟨⟩, β = I and γ taken to be a code for the mapping (Dλμ ↦ λ ∗ μ). In showing that any ideal is isomorphic to one of this form, we proceed in two steps:

4.1. Lemma.

(i) Given any ideal (p, q) (with realizers α, β, γ), we may uniformly construct an isomorphic ideal (p′, q′) for which q′ ⊆ p′ and β′ = I.

(ii) Given an ideal (p, q) with q ⊆ p (and realizers α, I, γ), we may uniformly construct an isomorphic ideal (!p′, a) where a is an upwards-closed subset of !p′.

Proof. (i) We define p′ = p and q′ = p∩q; clearly this is an ideal, with the same realizers α and γ as (p, q) and with β′ = I. Moreover, β realizes the inequality (p, q) ≤ (p′, q′), and I realizes the converse.

(ii) Again, we take p′ = p, and we take a to be the set of codes for sequences including at least one term in q. The inequality (p, q) ≤ (!p, a) is realized by ι; to realize the converse, we take a code for the function f: !p → p recursively defined by

\begin{aligned}f(λ) & = & α & if λ = ⟨⟩ \\ & = & γ(D(f(⟨λ_{1}, …, λ_{|λ|−1}⟩))λ_{|λ|}) & if |λ| > 0 . \end{aligned}

It is clear that if λ codes a sequence including a member of q then f(λ) ∈ q.

4.2. Theorem. For any Schönfinkel algebra Λ, the internal frames h_{∗}(Ω) and Idl(∇2) are isomorphic in Set⟨ℙΛ⟩. Hence Set⟨ℍΛ⟩ is equivalent to the Gleason cover of Set⟨ℙΛ⟩.

Proof. We may take Idl(∇2) to be the set of pairs (p, q) of subsets of Λ for which there exist realizers α, β, γ as above, with [[(p, q) ∈ Idl(∇2)]] taken to be the set of coded triples ⟨α, β, γ⟩ which satisfy the conditions for p and q, and equality predicate δ given by

δ((p, q), (p′, q′))

= [[(p, q) ∈ Idl(∇2)]] ∧ [[(p′, q′) ∈ Idl(∇2)]] ∧ ((p, q) ≤ (p′, q′)) ∧ ((p′, q′) ≤ (p, q)) ,

where ((p, q) ≤ (p′, q′)) denotes (p ⇒ p′) ∩ (q ⇒ q′). As already mentioned, h_{∗}(Ω) is the set of elements (p, a) ∈ HΛ, with equality predicate ϵ((p, a), (p′, a′)) = (((p, a) ≤ (p′, a′)) ∧ ((p′, a′) ≤ (p, a))), where ((p, a) ≤ (p′, a′)) is the set of codes for sequences of elements of (!p ⇒!p′) which contain at least one term in (a ⇒ a′). Note that, given such a code λ, we may uniformly construct an element of ((!p ⇒!p′) ∩ (a ⇒ a′)), coding the function which applies each of the λ_{i} for i ≤ |λ| to an element of !p and then concatenates the results.

It is now straightforward to verify that, if we define F: Idl(∇2) × HΛ → P Λ by

F ((p, q), (r, a)) = δ((p, q), (!r, a)) ,

then F represents a bijection f: Idl(∇2) → h_{∗}(Ω) in Set⟨ℙΛ⟩. Strictness is easy, as is extensionality in the first variable (p, q); extensionality in the second variable follows from the last sentence of the previous paragraph; single-valuedness in either direction is again easy; totality is the left-to-right direction follows from 4.1, and totality from right to left follows from the fact which we noted earlier that [[(!r, a) ∈ Idl(∇2)]] has a uniform realizer.

Moreover, f is an isomorphism of ordered sets (and hence of frames), since the order relation on each of the two objects is induced in the obvious way by the relations on their elements which we denoted ≤, and F is clearly compatible (in either direction) with these relations. But we have Set⟨ℍΛ⟩ ≃ Sh(h_{∗}(Ω)) since h is localic, so

Set⟨ℍΛ⟩ ≃ Sh(Idl(∇2)) ≃ γ(Set⟨ℙΛ⟩) .

5. Functoriality of Herbrand Realizability

The functoriality of the construction Λ ↦ Set⟨ℙΛ⟩ has been extensively studied, first by John Longley [13] and more recently by Hofstra and van Oosten [5] and by the present author [11]. The conclusion of these researches can be summarized as follows:

5.1. Theorem. The assignment Λ ↦ Set⟨ℙΛ⟩ is a full embedding of 2-categories Schön_{qs}^{op} → Top, where Schön denotes the 2-category of Schönfinkel algebras and applicative morphisms, Schön_{qs} is its subcategory whose 1-arrows are quasi-surjective morphisms, and Top is the 2-category of toposes and geometric morphisms.

We recall that Longley defined an applicative morphism θ: Λ ↬ M of Schönfinkel algebras to be an entire relation (i.e. one relating each element of Λ to at least one element of M) which has a witness τ ∈ M such that, if θ(λ, μ) and θ(λ′, μ′) hold and λλ′ is defined in Λ, then τμμ′ is defined in M and θ(λλ′, τμμ′) holds. Such a morphism is said to be quasi-surjective if there exists a function r: M → Λ and an element ρ ∈ M such that for all μ, μ′ ∈ M, if θ(r(μ), μ′) holds, then ρμ′ = μ. In [11], this was shown to be equivalent to the notion of computational density introduced by Hofstra and van Oosten in [5], which is in turn equivalent to the assertion that the indexed functor ℙΛ → ℙM induced by composition with θ has a right adjoint (and is thus the inverse image of a geometric morphism of triposes).

We have already observed that the 2-full embedding of 5.1 takes values in the sub-2-category Top_{sk} of toposes and skeletal geometric morphisms. But the Gleason cover construction is 2-functorial on this 2-category; in fact, as shown in [10], D4.6.12, it is right adjoint to the inclusion DMTop_{sk} → Top_{sk}, where DMTop_{sk} is the full sub-2-category of toposes satisfying De Morgan’s law. Thus we may immediately conclude:

5.2. Corollary. The assignment Λ ↦ Set⟨ℍΛ⟩ is a 2-functor Schön_{qs}^{op} → Top.

No doubt it would be possible to give a direct proof of Corollary 5.2, by showing that a quasi-surjective morphism of Schönfinkel algebras induces a geometric morphism between the corresponding Herbrand triposes. We leave this as an exercise for the reader! (Note, however, that we do not make any fullness claim for the 2-functor of 5.2: we do not even know whether every geometric morphism Set⟨ℍΛ⟩ → Set⟨ℍM⟩ is induced by a geometric morphism of triposes ℍΛ → ℍM.)

We conclude with an open problem. In [2], Olivia Caramello showed that every topos E contains a largest dense subtopos which satisfies De Morgan’s law; if E is two-valued, so that its only proper closed subtopos is degenerate, then the word ‘dense’ may be omitted from this characterization. We have seen that, at least when Λ is the Kleene algebra, Set⟨ℍΛ⟩ is a dense subtopos of the modified realizability topos Set⟨𝕄Λ⟩; indeed, the latter is the closure of the former as a subtopos of Set⟨ℙ_{1}Λ⟩. It would therefore be of interest to know whether the Herbrand realizability topos could also be obtained by applying Caramello’s construction to the modified realizability topos. It seems highly likely that this is true; for if E is any subtopos of Set⟨𝕄Λ⟩ satisfying De Morgan’s law, then the composite E → Set⟨𝕄Λ⟩ → Set⟨ℙΛ⟩ is skeletal, and hence factors uniquely through the Gleason cover Set⟨ℍΛ⟩ by [10], D4.6.12. However, this argument does not suffice to show that the triangle

\xymatrix{E \ar[r] \ar[dr] & Set⟨ℍΛ⟩ \ar[d] \\  & Set⟨𝕄Λ⟩}

commutes.

References

[1] B. van den Berg, The Herbrand topos, Math. Proc. Cambridge Philos. Soc. 155 (2013), 361–374.

[2] O. Caramello, De Morgan classifying toposes, Adv. Math. 222 (2009), 2117–2144.

[3] P.J. Freyd and A. Scedrov, Categories, Allegories (North–Holland, 1990).

[4] A.M. Gleason, Projective topological spaces, Ill. J. Math. 2 (1958), 482–489.

[5] P.J.W. Hofstra and J. van Oosten, Ordered partial combinatory algebras, Math. Proc. Cambridge Philos. Soc. 134 (2003), 445–463.

[6] J.M.E. Hyland, The effective topos, in The L.E.J. Brouwer Centenary Symposium, Studies in Logic and the Foundations of Mathematics vol. 110 (North–Holland, 1982), 165–216.

[7] J.M.E. Hyland, P.T. Johnstone and A.M. Pitts, Tripos theory, Math. Proc. Cambridge Philos. Soc. 88 (1980), 205–232.

[8] P.T. Johnstone, The Gleason cover of a topos, I, J. Pure Appl. Algebra 19 (1980), 171–192.

[9] P.T. Johnstone, Factorization theorems for geometric morphisms, II, in Categorical Aspects of Topology and Analysis, Lecture Notes in Math. vol. 915 (Springer–Verlag, 1982), 216–233.

[10] P.T. Johnstone, Sketches of an Elephant: a Topos Theory Compendium, Oxford Logic Guides 43–44 (Oxford University Press, 2002).

[11] P.T. Johnstone, Geometric morphisms of realizability toposes, Theory Appl. Categories 28 (2013), 241–249.

[12] P.T. Johnstone and I. Moerdijk, Local maps of toposes, Proc. London Math. Soc. (3) 58 (1989), 281–305.

[13] J.R. Longley, Realizability toposes and language semantics, Ph.D. thesis, University of Edinburgh (1994).

[14] J. van Oosten, The modified realizability topos, J. Pure Appl. Algebra 116 (1997), 273–289.

[15] J. van Oosten, Filtered colimits in the effective topos, J. Pure Appl. Algebra 205 (2006), 446–451.

[16] J. van Oosten, Realizability: An Introduction to its Categorical Side, Studies in Logic and the Foundations of Mathematics vol. 152 (Elsevier, 2008).

Department of Pure Mathematics, University of Cambridge, England

Email: P.T.Johnstone@dpmms.cam.ac.uk

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/28/32/28-32.{dvi,ps,pdf}

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. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. 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}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com

Valeria de Paiva: valeria.depaiva@gmail.com

Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Radboud University Nijmegen: i.moerdijk@math.ru.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Edinburgh: Alex.Simpson@ed.ac.uk James Stasheff, University of North Carolina: jds@math.upenn.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