The Sierpinski Object in the Scott Realizability Topos

TL;DR

This paper investigates the properties of the Sierpinski object within the Scott realizability topos, revealing its structure, the nature of order-discrete objects, and constructing a homotopy model where these objects have only constant paths.

Contribution

It introduces the concept of order-discrete objects in the Scott realizability topos, characterizes the Sierpinski object as a dominance, and constructs a homotopy model based on these findings.

Findings

Order-discrete objects form a reflective subcategory.

The Sierpinski object is not closed under unions.

A homotopy model with constant paths is constructed.

Abstract

We study the Sierpinski object $\Sigma$ in the realizability topos based on Scott's graph model of the $\lambda$-calculus. Our starting observation is that the object of realizers in this topos is the exponential $\Sigma ^N$, where $N$ is the natural numbers object. We define order-discrete objects by orthogonality to $\Sigma$. We show that the order-discrete objects form a reflective subcategory of the topos, and that many fundamental objects in higher-type arithmetic are order-discrete. Building on work by Lietz, we give some new results regarding the internal logic of the topos. Then we consider $\Sigma$ as a dominance; we explicitly construct the lift functor and characterize $\Sigma$-subobjects. Contrary to our expectations the dominance $\Sigma$ is not closed under unions. In the last section we build a model for homotopy theory, where the order-discrete objects are exactly those objects which only have constant paths.

Equations

$${\mathcal{U}}_p=\{U\subseteq \mathbb{N}|p\subseteq U\}$$

$$n\in F(U)\text{ if and only if for some finite p⊆U, }n\in F(p).$$

$$e_n=\{k_1,\dots ,k_m\}\text{ if and only if }n=2^{k_1}+\cdots +2^{k_m}.$$

$$UV=\{n|\text{ for some }m,e_m\subseteq V\text{ and }⟨m,n⟩\in U\}$$

$$\mathsf{graph}(F)=\{⟨m,n⟩|n\in F(e_m)\}$$

$$\mathsf{graph}(F)=\{⟨m_1,⟨m_2,⟨\cdots m_n,k⟩\cdots ⟩⟩|k\in F(e_{m_1},\dots ,,e_{m_n})\}$$

$$\{⟨2^n,⟨0,2n⟩⟩|n\in \mathbb{N}\}\cup \{⟨0,⟨2^n,2n+1⟩⟩|n\in \mathbb{N}\}$$

$$\mathsf{p}U=\{⟨0,2n⟩|n\in U\}\cup \{⟨2^n,2n+1⟩|n\in \mathbb{N}\}$$

$$\mathsf{p}UV=\{2n|n\in U\}\cup \{2n+1|n\in V\}.$$

$$E((x_n{)}_n)=\{U|U\overline{n}\in E_n(x_n)\text{ for all }n\}.$$

$$\mathrm{Set}\stackrel{\nabla }{\to }\mathsf{Ass}(\mathcal{S});\mathsf{Ass}(\mathcal{S})\stackrel{\Gamma }{\to }\mathrm{Set};\Gamma ⊣\nabla$$

$$e(x)=\{n|x\in S_n\}$$

$$[x\sim y]\;=\;\left\{\begin{array}[]{cl}E(x)&\text{if }x=y\\ \emptyset&\text{otherwise}\end{array}\right.$$

$$f\approx g=[\forall p(E_P(p)\to f(p){\sim }_{X}g(p))].$$

$$E_{\Sigma }(0)=\{\varnothing \}\text{ and }E(1)=\{\{1\}\}.$$

$$\overline{n}\mapsto \{\begin{array}{ll}\overline{1}& \text{if }f(n)=1;\\ \varnothing & \text{if }f(n)=0.\end{array}$$

$$\chi :\mathcal{S}\to \{0,1{\}}^{\mathbb{N}},U\mapsto {\chi }_U$$

$${\chi }^{-1}:\{0,1{\}}^{\mathbb{N}}\to \mathcal{S},f\mapsto f^{-1}(\{1\}).$$

$$(W,W^{\prime })\mapsto \{⟨0,n⟩\mid n\in W\}\cup \{⟨2,n⟩\mid n\in W^{\prime }\}$$

$$\lambda uv.t(\mathsf{p}(s(R(Guv)\varnothing ))(R(Guv)\overline{1}))$$

$$\varnothing \mapsto A(F\varnothing )(F\varnothing ),W\ne \varnothing \mapsto A(F\varnothing )(F\overline{1})$$

$$\forall x:X\exists y:Y\varphi (x,y)\to \exists f:Y^X\forall x:X\varphi (x,f(x)).$$

$$\forall f:N^N\exists x:N\varphi (f,x)\to \forall f:N^N\exists xy:N\forall g:N^N(\overline{f}y=\overline{g}y\to \varphi (g,x)),$$

$$\overline{f}y=\overline{g}y$$

$$\forall F:N^{(N^N)}\forall f:N^N\exists x:N\forall g:N^N(\overline{f}x=\overline{g}x\to F(f)=F(g))$$

$$P=\{\varphi :\mathbb{N}\to \mathcal{P}(A)\mid \text{for all n∈N, if a∈ϕ(n), then p1a=n}\}$$

$$\psi \approx \psi =[\forall n(\varphi (n)\leftrightarrow \psi (n))].$$

$$\forall x(\neg \neg (x\in X)\to x\in X)$$

$$f_{\alpha }(n)\in \{\begin{array}{ll}[n\in \alpha ]& \text{if }[n\in \alpha ]\ne \varnothing ;\\ \{\varnothing \}& \text{else}.\end{array}$$

$$R\in \bigcap _{\alpha \in P}\bigcup _{\beta \in P}[[\text{Stab}(\beta )\wedge \forall x(x\in \alpha \leftrightarrow \exists y⟨y,x⟩\in \beta )]].$$

$${\alpha }_a(0)=\{\mathsf{p}a\overline{0}\}\text{and}{\alpha }_a(n+1)=\varnothing \text{for any }n\in \mathbb{N}.$$

Full text

Corresponding author: Jaap van Oosten

1. Introduction

In this paper, we aim to revive interest in what we call the Sierpinski object in the Scott realizability topos. We show that it is of fundamental importance in studying the subcategory of order-discrete objects (section 3), arithmetic in the topos (section 4), the Sierpinski object as a dominance (section 5) and a notion of homotopy based on it (section 6). Section 2 deals with preliminaries and establishes notation.

2. Preliminaries

Independently observed by G. Plotkin and D.S. Scott ([11, 12, 10]), there is a combinatory algebra structure (in fact, a $\lambda$-model structure) on the power set ${\mathcal{P}}(\mathbb{N})$ of the natural numbers.

Identifying ${\mathcal{P}}(\mathbb{N})$ with $\prod_{n\in\mathbb{N}}\{0,1\}$ and giving $\{0,1\}$ the Sierpinski topology (with $\{1\}$ the only nontrivial open set), we endow ${\mathcal{P}}(\mathbb{N})$ with the product topology. Concretely, basic opens of ${\mathcal{P}}(\mathbb{N})$ are of the form

[TABLE]

for $p$ a finite subset of $\mathbb{N}$. A function $F:{\mathcal{P}}(\mathbb{N})\to{\mathcal{P}}(\mathbb{N})$ is continuous for this topology if and only if it has the property that

[TABLE]

Note, that every continuous function automatically preserves the inclusion $\subseteq$.

Such continuous maps are encoded by elements of ${\mathcal{P}}(\mathbb{N})$ in the following way. Consider the following coding of finite subsets of $\mathbb{N}$:

[TABLE]

By convention, $e_{0}=\emptyset$. So: $e_{1}=\{0\}$, $e_{2}=\{1\}$, $e_{3}=\{0,1\}$, $e_{2^{n}}=\{n\}$, etc.

Consider also a bijection $\langle{\cdot},{\cdot}\rangle:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$, which we don’t specify.

Now we define a binary operation (written as juxtaposition) on ${\mathcal{P}}(\mathbb{N})$:

[TABLE]

For every function $F:{\mathcal{P}}(\mathbb{N})\to{\mathcal{P}}(\mathbb{N})$ we have

[TABLE]

so that, when $F$ is continuous, ${\sf graph}(F)V=F(V)$ for all $V\in{\mathcal{P}}(\mathbb{N})$. Note that the operation $U,V\mapsto UV$ is a continuous map of two variables.

We think of the operation $U,V\mapsto UV$ as an application operation: apply the continuous function coded by $U$ to the argument $V$.

The structure ${\mathcal{P}}(\mathbb{N})$ together with this application function is denoted $\mathcal{S}$. The fact that $\mathcal{S}$ is a $\lambda$-model is worked out in detail in [12]. We shall use $\lambda$-terms to denote elements of $\mathcal{S}$ according to this interpretation. We use repeated juxtaposition and associate to the left when discussing iterated application: $VU_{1}\cdots U_{n}$ means $(\cdots((VU_{1})U_{2})\cdots)U_{n}$. For continuous functions of several variables $F:{\mathcal{P}}(\mathbb{N})^{n}\to{\mathcal{P}}(\mathbb{N})$ we let

[TABLE]

So with these conventions, ${\sf graph}(F)U_{1}\cdots U_{n}=F(U_{1},\ldots,U_{n})$.

In $\mathcal{S}$, special combinators for important operations are available:

**Pairing and unpairing combinators: **

${\sf p},{\sf p}_{0},{\sf p}_{1}\in{\mathcal{S}}$ satisfying ${\sf p}_{0}({\sf p}UV)=U$, ${\sf p}_{1}({\sf p}UV)=V$. In fact we can take

[TABLE]

for $\sf p$, so that

[TABLE]

and

[TABLE]

**Booleans: **

${\sf t}=\{1\}$, ${\sf f}=\{0\}$. We have an “if … then …, else…” operator $\sf q$, satisfying ${\sf qt}UV=U$ and ${\sf qf}UV=V$.

**Natural numbers: **

we write $\overline{n}$ for the element $\{n\}$.

**Coding of tuples: **

we write $[U_{0},\ldots,U_{n}]$ for a standard coding of $n+1$-tuples in $\mathcal{S}$. This coding has the usual properties as given in [15]: there are elements of $\mathcal{S}$ which give the length of a coded tuple, the $i$’th element (for appropriate $i$), and the code of the concatenation of two tuples.

As usual we have a category of assemblies over $\mathcal{S}$, denoted ${\sf Ass}({\mathcal{S}})$ and the realizability topos ${\sf RT}({\mathcal{S}})$, which we call the Scott realizability topos (unfortunately, the term “Scott topos” is already in use). We briefly introduce these categories.

An assembly over $\mathcal{S}$ is a pair $X=(|X|,E_{X})$ where $|X|$ is a set and $E_{X}$ gives, for each $x\in|X|$, a nonempty subset $E_{X}(x)$ of $\mathcal{S}$. A morphism of assemblies $(|X|,E_{X})\to(|Y|,E_{Y})$ is a function $f:|X|\to|Y|$ for which there is some element $U$ of $\mathcal{S}$ which tracks $f$, meaning that for all $x\in|X|$ and all $V\in E_{X}(x)$ we have $UV\in E_{Y}(f(x))$.

The category ${\sf Ass}({\mathcal{S}})$ is a quasitopos. By way of example, let us construct exponentials explicitly: the exponent $(Y,E_{Y})^{(X,E_{X})}$ can be given as $(Z,E_{Z})$ where $Z$ is the set of morphisms from $(X,E_{X})$ to $(Y,E_{Y})$ and $E_{Z}(f)$ is the set of those elements of $\mathcal{S}$ which track the morphism $f$.

Actually, ${\sf Ass}({\mathcal{S}})$ has countable products: given a countable family $((X_{n}),E_{n})_{n\in\mathbb{N}}$ of assemblies over $\mathcal{S}$, one has the assembly $(\prod_{n}X_{n},E)$ where

[TABLE]

The category ${\sf Ass}({\mathcal{S}})$ has several subcategories of interest. First we recall that there is an adjunction

[TABLE]

where $\Gamma(|X|,E_{X})=|X|$, $\nabla(Y)=(Y,E)$ with $E(y)={\mathcal{S}}$ for all $y$.

An assembly $X$ is partitioned if $E_{X}(x)$ is always a singleton. It is not hard to see that the object $\nabla(Y)$ is isomorphic to $(Y,E)$ where $E(y)=\{\emptyset\}$ for all $y$, so all objects $\nabla(Y)$ are isomorphic to partitioned assemblies. Up to isomorphism, the partitioned assemblies are exactly the regular projective objects (the objects for which the representable functor into Sets preserves regular epimorphisms), which, in the topos ${\sf RT}({\mathcal{S}})$, coincide with the internally projective objects (the objects $X$ for which the endofuctor $(-)^{X}$ preserves epimorphisms); see 2 below.

An assembly $X$ is modest if $E_{X}(x)\cap E_{X}(y)=\emptyset$ whenever $x\neq y$. The modest assemblies are, up to isomorphism, the ones for which the diagonal map $X\to X^{\nabla(2)}$ is an isomorphism (here, 2 denotes any two-element set); such objects are called discrete in [4].

A special object of ${\sf Ass}({\mathcal{S}})$ is the object of realizers $S=({\mathcal{S}},E)$ where $E(U)=\{U\}$; one sees that $S$ is both partitioned and modest. Every object which is both partitioned and modest is a regular subobject of $S$: that is, isomorphic to an object $({\mathcal{A}},E)$ where ${\mathcal{A}}\subseteq{\mathcal{S}}$ and $E$ is the restriction to $\mathcal{A}$ of the map defining $S$.

Another partitioned and modest object is the natural numbers object $N=(\mathbb{N},E_{N})$, where $E_{N}(n)=\{\overline{n}\}$.

As Andrej Bauer observed in his thesis ([1]), one can embed the category $T_{0}^{\rm cb}$ of countably based $T_{0}$-spaces into the subcategory of partitioned and modest assemblies over $\mathcal{S}$. To be precise, by “countably based $T_{0}$-space” we mean a $T_{0}$-space together with a chosen enumeration of a subbasis. If $(X,\{S_{n}\,|\,n\in\mathbb{N}\})$ is such, then the map $e:X\to{\mathcal{S}}$ given by

[TABLE]

defines an embedding of $X$ into $\mathcal{S}$. Moreover, given countably based spaces $X$ and $Y$ with associated embeddings $e:X\to{\mathcal{S}},d:Y\to{\mathcal{S}}$, there is for every continuous map $f:X\to Y$ a continuous extension $F_{f}:{\mathcal{S}}\to{\mathcal{S}}$ satisfying $F_{f}{\circ}e=d{\circ}f$. This means that if we see the space $X$ with embedding $e:X\to{\mathcal{S}}$ as assembly $(X,E_{X})$ where $E_{X}(x)=\{e(x)\}$, then every continuous map $f:X\to Y$ is tracked (as a morphism of assemblies $(X,E_{X})\to(Y,E_{Y})$) by ${\sf graph}(F_{f})$.

Finally, we have the Scott realizability topos, the realizability topos over $\mathcal{S}$, denoted ${\sf RT}({\mathcal{S}})$. Its objects are pairs $(X,\sim)$ where $X$ is a set and for $x,y\in X$, $[x\sim y]$ is a subset of $\mathcal{S}$ (so $\sim$ is a ${\mathcal{P}}({\mathcal{S}})$-valued relation on $X$), which satisfies certain conditions (we refer to [15] for details). Every assembly $(X,E)$ is an object of ${\sf RT}({\mathcal{S}})$ if we define

[TABLE]

As subcategory of ${\sf RT}({\mathcal{S}})$, the category ${\sf Ass}({\mathcal{S}})$ is equivalent to the category of $\neg\neg$-stable objects of ${\sf RT}({\mathcal{S}})$, that is: the objects $(X,\sim)$ satisfying $\forall x,x^{\prime}:X.\neg\neg(x\sim x^{\prime})\to x\sim x^{\prime}$. We shall not rehearse the structure of ${\sf RT}({\mathcal{S}})$ or its internal logic, based on realizability over $\mathcal{S}$, any further, as for this theory now standard texts are available. We only recall the following facts from [15], pp.135–7 (the proofs generalize to arbitrary pcas):

Lemma 1**.**

If $P$ is a partitioned assembly and $X$ is any object, then the exponential $X^{P}$ is isomorphic to the object $(|X|^{|P|},\approx)$ where

[TABLE]

Lemma 2**.**

An object is internally projective in ${\sf RT}({\mathcal{S}})$ if and only if it is isomorphic to a partitioned assembly.

The following small proposition will be of use later on. Given an assembly $(X,E)$ let ${\int}(X,E)$ be $(X^{\prime},E^{\prime})$ where $X^{\prime}=\{(x,U)\,|\,U\in E(x)\}$ and $E^{\prime}(x,U)=\{U\}$. Consider also ${\int\!\!\!\int}(X,E)=(X^{\prime\prime},E^{\prime\prime})$ where $X^{\prime\prime}=\{(x,U,V)\,|\,U,V\in E(x)\}$ and $E^{\prime\prime}(x,U,V)=\{{\sf p}UV\}$. Clearly, we have a projection ${\int}(X,E)\to(X,E)$ and two projections ${\int\!\!\!\int}(X,E)\to{\int}(X,E)$, and these maps form a coequalizer diagram in ${\sf Ass}({\mathcal{S}})$.

Proposition 3**.**

Let $(Y,\sim)$ be an arbitrary object of ${\sf RT}({\mathcal{S}})$ and let $(X,E)$ be an assembly over $\mathcal{S}$. The exponential $(Y,\sim)^{(X,E)}$ can be presented as follows: its underlying set is the set of functions from $\{(x,U)\,|\,U\in E(x)\}$ to $Y$. Given two such functions $f,g$, the set $[f\approx g]$ consists of those coded triples $[P,Q,R]$ (coded in the sense of $\mathcal{S}$) of elements of $\mathcal{S}$, which satisfy the following three conditions:

1. (1)

for $U\in E(x)$, $PU\in[f(x,U)\sim f(x,U)]$; 2. (2)

for $U,U^{\prime}\in E(x)$, $QUU^{\prime}\in[f(x,U)\sim f(x,U^{\prime})]$; 3. (3)

for $U\in E(x)$, $RU\in[f(x,U)\sim g(x,U)]$.

Proof 2.1**.**

Observe that the objects ${\int}(X,E)$ and ${\int\!\!\!\int}(X,E)$ are partitioned assemblies, hence projective objects in ${\sf RT}({\mathcal{S}})$. Also note that the contravariant functor $(Y,\sim)^{(-)}$ sends coequalizers to equalizers. Finally, use Lemma 1.

3. The Sierpiński object and order-discrete objects

{defi}

The Sierpiński object $\Sigma$ is the image of Sierpiński space under the embedding $T_{0}^{\text{cb}}\to\mathsf{RT}(\mathcal{S})$. Concretely, $\Sigma$ is the modest set $(\{0,1\},E_{\Sigma})$ with

[TABLE]

{defi}

The object of realizers $S$ is the modest set $(\mathcal{S},\{-\})$.

The two objects above are related, as follows.

Proposition 4**.**

The object of realizers is isomorphic to the exponential $\Sigma^{N}$, where $N$ is the natural numbers object of $\mathsf{RT}(\mathcal{S})$.

Proof 3.1**.**

We prove that the underlying set of $\Sigma^{N}$ is $\{0,1\}^{\mathbb{N}}$. Since any morphism from $N$ to $\Sigma$ is in particular a function from $\mathbb{N}$ to $\{0,1\}$, one inclusion is clear. Conversely, if $f\colon\mathbb{N}\to\{0,1\}$, then $f$ is tracked by $\textup{graph}(F)$, where $F\colon\mathcal{S}\to\mathcal{S}$ is the continuous function defined by:

[TABLE]

Thus, $\Sigma^{N}$ is the assembly $(\{0,1\}^{\mathbb{N}},E)$ where $E(f)\subseteq\mathcal{S}$ is the set of trackers of the function $f$ (note, that this set is always nonempty).

We have a canonical bijection

[TABLE]

(where $\chi_{U}$ is the characteristic function of $U$) with inverse

[TABLE]

It remains to prove that these functions are tracked. For $\chi$, consider the continuous function $F\colon\mathcal{S}\to\mathcal{S}$ given by $U\mapsto\{\langle 2^{n},1\rangle\mid n\in U\}.$ Then $\chi$ is tracked by graph($F$). Indeed, if $U\in\mathcal{S}$ and $n\in\mathbb{N}$, then $\textup{graph}(F)U\overline{n}=F(U)\overline{n}$ and this is $\overline{1}$ if $n\in U$ and $\emptyset$ otherwise.

For the inverse of $\chi$, we define $G\colon\mathcal{S}\to\mathcal{S}$ continuous by $U\mapsto\{n\in\mathbb{N}\mid U\overline{n}=\overline{1}\}$. (This is continuous, because the application of $\mathcal{S}$ is continuous.) We claim that $\chi^{-1}$ is tracked by $\textup{graph}(G)$. Indeed, for $f\in\{0,1\}^{\mathbb{N}}$ and $U\in E(f)$, we have $n\in G(U)$ if and only if $f(n)=1$, since $U$ tracks $f$.

3.1. Order-discrete objects

{defi}

An object $X$ of $\mathsf{RT}(\mathcal{S})$ is order-discrete if it is orthogonal to $\Sigma$, viz. the diagonal $X\xrightarrow{\delta_{X}}X^{\Sigma}$ is an isomorphism.

We wish to characterize the order-discrete objects in terms of their realizers. To this end, we first present some useful lemmas.

Lemma 5**.**

An object $X$ is order-discrete if and only if the diagonal $\delta_{X}$ is an epimorphism.

Proof 3.2**.**

Of course, $\delta_{X}$ is epic if $X$ is order-discrete. Conversely, suppose $\delta_{X}$ is an epi. Clearly, the unique morphism $!_{\Sigma}\colon\Sigma\to 1$ is an epimorphism. Hence, the diagonal $\delta_{X}=X^{!_{\Sigma}}$ is monic. Thus, $\delta_{X}$ is an iso, as desired.

Proposition 6**.**

An object $X$ is order-discrete if and only if there is $A\in\mathcal{S}$ such that for any $x,x^{\prime}\in|X|$: if $U\in[x\sim_{X}x]$ and $V\in[x^{\prime}\sim_{X}x^{\prime}]$ with $U\subseteq V$, then $AUV\in[x\sim_{X}x^{\prime}]$.

Proof 3.3**.**

Suppose first that $X$ is order-discrete. We construct the desired element $A\in\mathcal{S}$. Assume we have $x,x^{\prime}\in|X|$ and $U\in[x\sim_{X}x],V\in[x^{\prime}\sim_{X}x^{\prime}]$ with $U\subseteq V$. By Lemma 1 we have $X^{\Sigma}\cong(|X|^{\{0,1\}},\approx)$. Define $f\colon\{0,1\}\to|X|$ by $f(0)=x$ and $f(1)=x^{\prime}$. The map $H\colon\mathcal{S}^{2}\to\mathcal{S}$ defined as

[TABLE]

is easily seen to be continuous. Write $G=\textup{graph}(H)$. We claim that $GUV\in[f\approx f]$. Indeed, $GUV=\{\langle 0,n\rangle\mid n\in U\}\cup\{\langle 2,n\rangle\mid n\in V\}$, so that $GUV\emptyset=U\in[f(0)\sim_{X}f(0)]$. Moreover, $GUV\overline{1}=U\cup V=V\in[f(1)\sim_{X}f(1)]$, since $e_{0}=\emptyset$ and $e_{2}=\overline{1}$ and $U\subseteq V$. Thus, $GUV\in[f\approx f]$. Now let $R\in\mathcal{S}$ be a realizer of the fact that $\delta$ is epic. Then $R(GUV)$ is an element of $[\forall p(E_{\Sigma}(p)\to x_{0}\sim_{X}f(p))]$ for some $x_{0}\in|X|$. Thus, $R(GUV)\emptyset\in[x_{0}\sim_{X}x]$ and $R(GUV)\overline{1}\in[x_{0}\sim_{X}x^{\prime}]$. Finally, let $t,s\in\mathcal{S}$ respectively realize transitivity and symmetry of $\sim_{X}$. Then, we see that

[TABLE]

is the desired element $A$.

Conversely, suppose we have an $A\in\mathcal{S}$ as in the proposition. Let $f\colon\{0,1\}\to|X|$ be arbitrary. By Lemma 5, it suffices to show that from an element of $[f\approx f]$, we can continuously find an $x\in|X|$ and an element of $[\forall p(E_{\Sigma}(p)\to x\sim_{X}f(p))]$. Let $F\in[f\approx f]$. Then $F\emptyset\in[f(0)\sim_{X}f(0)]$, $F\overline{1}\in[f(1)\sim_{X}f(1)]$ and $F\emptyset\subseteq F\overline{1}$, so $A(F\emptyset)(F\overline{1})\in[f(0)\sim_{X}f(1)]$ and $A(F\emptyset)(F\emptyset)\in[f(0)\sim_{X}f(0)]$. Hence, if we set $x=f(0)$, then the graph of the continuous function

[TABLE]

is the desired element.

Corollary 7**.**

An assembly $X$ is order-discrete if and only if the existence of realizers $U\in E_{X}(x)$ and $V\in E_{X}(y)$ with $U\subseteq V$ implies that $x$ and $y$ are equal.

Proof 3.4**.**

Immediate.

{exa}

The natural numbers object $N$ (c.f. the proof of 4) is easily seen to be order-discrete using the corollary above.

Recall from the section on preliminaries that an object is called discrete if it is orthogonal to $\nabla(2)$. For an assembly $X$, this means that the realizing sets are disjoint. Thus, Corollary 7 shows that any order-discrete assembly is also discrete (alternatively, one might observe that the map from $\Sigma$ to $\nabla(2)$ is an epi in ${\sf Ass}({\mathcal{S}})$, and therefore the map $X^{\nabla(2)}\to X^{\Sigma}$ is monic. From this one also easily deduces that order-discrete implies discrete, for assemblies). In fact, this holds for all objects, not just assemblies.

Proposition 8**.**

Any order-discrete object is discrete.

Proof 3.5**.**

This follows from Proposition 6 and [15], Corollary 3.2.20. The statement there carries over to arbitrary realizability toposes.

Remark 9**.**

One might expect the availability of a simpler proof of the proposition above, i.e. a proof that does not rely on the characterization of the (order-)discrete objects. However, note that although we have a morphism $\Sigma\to\nabla(2)$, it is not a regular epimorphism, so one cannot apply [4], Lemma 2.2.

In [4], it it shown that the class of objects orthogonal to an object $A$ satisfies some nice properties if $A$ is well-supported and internally projective. By Lemma 2, the object $\Sigma$ is internally projective. It is clearly well-supported, which gives us the following proposition:

Proposition 10**.**

The order-discrete objects are closed under all existing limits, subobjects and quotients in $\mathsf{RT}(\mathcal{S})$. Moreover, they form an exponential ideal. Finally, they form a reflective subcategory of $\mathsf{RT}(\mathcal{S})$.

Proof 3.6**.**

The first statement is true, because any collection of orthogonal objects is closed under all existing limits (see [4], p. 1). Similarly, any collection of orthogonal objects forms an exponential ideal. The other closure properties follow from Lemmas 2.3 and 2.8 of [4], and Lemma 2 above. The final claim is proven as a corollary right after Lemma 2.3 of [4].

Remark 11**.**

For comparison with the notion of homotopy to be defined below, we give a concrete representation of the order-discrete reflection of an arbitrary object $(X,\sim)$. It has the same underlying set $X$, and we let $[x\approx y]$ consist of those coded (in the sense of $\mathcal{S}$) $(3n+1)$-tuples $[U_{0},V_{0},W_{0},\ldots,U_{n-1},V_{n-1},W_{n-1},U_{n}]$ for which there is a sequence $(x_{0},y_{0},\ldots,x_{n},y_{n})$ of elements of $X$, such that the following conditions hold:

1. (1)

$x_{0}=x$* and $y_{n}=y$;* 2. (2)

$U_{k}\in[x_{k}\sim y_{k}]$* for $0\leq k\leq n$;* 3. (3)

$V_{k}\in[y_{k}\sim y_{k}]$* and $W_{k}\in[x_{k+1}\sim x_{k+1}]$ for $0\leq k<n$;* 4. (4)

$V_{k}\subseteq W_{k}$* or $W_{k}\subseteq V_{k}$ must hold.*

4. Arithmetic in ${\sf RT}({\mathcal{S}})$

The order-discrete modest sets already make a disguised appearance in [5]. Herein, Lietz singles out a class of so-called well-behaved modest sets. It is not hard to show that a modest set is well-behaved if and only if it is order-discrete and moreover, it has the join-property, which we define now. {defi} An assembly has the join-property if it is isomorphic to an assembly $X$ whose realizing sets are closed under binary joins, viz. if $U\in E_{X}(x)$ and $V\in E_{X}(x)$, then $U\cup V\in E_{X}(x)$ for all $x\in|X|$.

{exa} The natural numbers object $N$ has the join-property.

The following proposition is a very slight generalization of [5], Theorem 2.3.

Proposition 12**.**

Let $X$ and $Y$ be modest sets. If $X$ has the join-property and $Y$ is order-discrete, then the following form of the Axiom of Choice holds in $\mathsf{RT}(\mathcal{S})$:**

[TABLE]

Proof 4.1**.**

See the proof of [5], Theorem 2.3.

We have already seen that the order-discrete objects form an exponential ideal and are closed under binary products. In [5], Theorem 2.2, it is shown that this also holds for the modest objects that have the join-property. Since $N$ is order-discrete and has the join-property, it follows that the Axiom of Choice holds for all finite types. Consequently, the following two principles

[TABLE]

are equivalent (and false) in $\mathsf{RT}(\mathcal{S})$; c.f. [5], Section 2.3.

4.1. Second-order arithmetic in ${\sf RT}({\mathcal{S}})$

We close this section by some brief considerations on second-order arithmetic in realizability toposes and $\mathsf{RT}(\mathcal{S})$ in particular.

Lemma 13**.**

Let $A$ be any partial combinatory algebra. Write $\overline{n}$ for the $n$-th Curry numeral in $A$ and let ${\mathsf{p}}$ be a pairing combinator in $A$ with projections ${\mathsf{p}}_{0}$ and ${\mathsf{p}}_{1}$.

The power object ${\mathcal{P}}(N)$ of the natural numbers object $N$ in ${\sf RT}(A)$ can be given as the object $(P,\approx)$ where $P$ is the set

[TABLE]

and

[TABLE]

Proof 4.2**.**

Straightforward.

We now turn our attention to $\lnot\lnot$-stable subsets of $N$, viz. subsets $X$ such that

[TABLE]

is true in $\mathsf{RT}(A)$. We will abbreviate this formula by $\textup{Stab}(X)$.

We formulate the following triviality as a proposition for comparison with 15 below, in the case of $A={\mathcal{S}}$.

Proposition 14**.**

If $A$ is nontrivial, then not every subset is $\lnot\lnot$-stable, i.e. the sentence $\forall X\textup{Stab}(X)$ is not valid in ${\sf RT}(A)$.

Proof 4.3**.**

Note that $\forall X\textup{Stab}(X)$ implies $\forall p.\neg\neg p\to p$ (where $p$ is a variable of type $\Omega$), which fails in ${\sf RT}(A)$ as soon as $A$ has two disjoint nonempty subsets. If $A$ is trivial then ${\sf RT}(A)={\rm Set}$, and $\forall X\textup{Stab}(X)$ obviously holds.

By contrast, in ${\sf RT}({\mathcal{S}})$ we have the following result (substituting $\mathcal{S}$ for $A$ in the definition of $P$ in Lemma 13):

Proposition 15**.**

For any $\alpha\in P$, we have a realizer of $\textup{Stab}(\alpha)$. Hence, the sentence $\forall X\lnot\lnot\textup{Stab}(X)$ is true in $\mathsf{RT}(\mathcal{S})$.

Proof 4.4**.**

Let $\alpha\in P$. Note that there is a function $f_{\alpha}\colon\mathbb{N}\to\mathcal{S}$ such that

[TABLE]

Moreover, there is an element $F_{\alpha}\in\mathcal{S}$ such that $F_{\alpha}\overline{n}=f_{\alpha}(n)$. Now note that $\lambda{xy}.F_{\alpha}x$ realizes $\textup{Stab}(\alpha)$.

Corollary 16**.**

First-order arithmetic in ${\sf RT}({\mathcal{S}})$ is the same as first-order arithmetic in Set.

Proof 4.5**.**

Given a true first-order arithmetical sentence $\phi$, we have, by Proposition 15, a realizer for $\forall x(\psi(x)\vee\neg\psi(x))$, for every subformula $\psi$ of $\phi$. From this one constructs a realizer for $\phi$.

Just as for ordinary natural numbers, we write $\langle-,\!-\rangle$ for a definable coding of $N^{2}$ to $N$ in ${\sf RT}(A)$. The sentence $\forall X\exists Y(\textup{Stab}(Y)\land\forall x(x\in X\leftrightarrow\exists y\langle{y,x}\rangle\in Y))$ is known as Shanin’s Principle. It holds in the Effective Topos ([15], p. 127). Internally, it says that every subset of $N$ is covered by a stable subset of $N$.

Proposition 17**.**

If $|A|>|\mathbb{N}|$, then Shanin’s Principle does not hold in ${\sf RT}(A)$.

Proof 4.6**.**

Assume for the sake of contradiction that it does. Then we have a realizer

[TABLE]

Let us write $R_{0}=\mathsf{p_{0}}R$ and $R_{1}=\mathsf{p_{1}}R$. For each $a\in A$, define the element $\alpha_{a}\in P$ by:

[TABLE]

For each $a\in A$, pick some $\beta_{a}\in P$ such that $R\in\llbracket\textup{Stab}(\beta_{a})\land\forall x(x\in\alpha_{a}\leftrightarrow\exists y\langle y,x\rangle\in\beta_{a})\rrbracket$.

From $R_{1}$, we effectively obtain $R^{\prime}\in A$ such that for every $a\in A$, we have:

[TABLE]

for some $m\in\mathbb{N}$. As $|A|>|\mathbb{N}|$, there must be two different $a,a^{\prime}\in A$ such that

[TABLE]

for the same $m\in\mathbb{N}$.

From $R_{0}$, we effectively obtain $s\in A$ witnessing the stability of $\beta_{a}$ and $\beta_{a^{\prime}}$. Thus, by $(\ast)$, we can use $s$ to get a common realizer:

[TABLE]

Finally, using $s\overline{\langle m,0\rangle}\mathsf{i}$ and $R_{1}$, we find a realizer in the intersection $[0\in\alpha_{a}]\cap[0\in\alpha_{a^{\prime}}]=\alpha_{a}\cap\alpha_{a^{\prime}}$. But this is impossible, because $a$ and $a^{\prime}$ are different, so that $\alpha_{a}$ and $\alpha_{a^{\prime}}$ are disjoint.

Corollary 18**.**

Shanin’s Principle does not hold in $\mathsf{RT}(\mathcal{S})$ and $\mathsf{RT}({\mathcal{K}}_{2})$ (where ${\mathcal{K}}_{2}$ is Kleene’s second model).

5. The Sierpiński object as a dominance

One can also study the Sierpiński object from a synthetic domain theoretic standpoint. This was done by Wesley Phoa ([8], Chapter 12 and [9], Proposition 3.1), who worked in the category of modest sets over the r.e. graph model, John Longley ([6], 5.3.7) and Alex Simpson ([7]). Our treatment is based on Proposition 4. {defi} Define a relation $\in$ between $N$ and $S$ (the object of realizers) by taking the following pullback

[TABLE]

where $\Sigma\to\Omega$ is the morphism induced by the function $0\mapsto\emptyset$ and $1\mapsto\mathcal{S}$.

Remark 19**.**

Observe that $\in$ is given by

[TABLE]

In particular, $\in$ is $\lnot\lnot$-stable.

Lemma 20**.**

Let $\mathcal{A}$ be a arbitrary total pca and let $\mathsf{RT}(\mathcal{A})$ be its realizability topos. Let $A=(\mathcal{A},\{-\})$ be the object of realizers in the topos. The scheme

[TABLE]

with $x$ not free in $\phi$ is valid in $\mathsf{RT}(\mathcal{A})$.

Proof 5.1**.**

It is not hard to verify that $\lambda u.{\mathsf{p}}({\mathsf{p}}_{0}(u{\sf k}))(\lambda v.{\mathsf{p}}_{1}(u{\sf k}))$ realizes the scheme.

Proposition 21**.**

The subobject $\Omega^{\prime}$ of $\Omega$ given by

[TABLE]

with $p$ ranging over $\Omega$, is a dominance in $\mathsf{RT}(\mathcal{S})$. Moreover, it is $\lnot\lnot$-separated, i.e. $\forall p{:}\Omega^{\prime}(\lnot\lnot p\to p)$. Furthermore, $\bot\in\Omega^{\prime}$.

Proof 5.2**.**

Double negation separation is immediate by Remark 19. Further, it is clear that $\top\in\Omega^{\prime}$ (take $X=\overline{1}$).

Suppose $p\in\Omega^{\prime}$ and $p\to(q\in\Omega^{\prime})$. Take $U\in\mathcal{S}$ such that $p\leftrightarrow 1\in U$. Then, $1\in U\to\exists X{:}S(q\leftrightarrow 1\in X)$, so by Lemma 20 and Remark 19, we get that $\exists X{:}S(1\in U\to(q\leftrightarrow 1\in X))$. Take such $V\in\mathcal{S}$. Then, $p\land q\leftrightarrow 1\in U\cap V$. Hence, $p\land q\in\Omega^{\prime}$ and $\Omega^{\prime}$ is a dominance.

We have already remarked that the object $\Omega^{\prime}$ from 21 is $\lnot\lnot$-separated. Indeed, it is isomorphic to an assembly.

Proposition 22**.**

The object $\Omega^{\prime}$ is isomorphic to $\Sigma$.

Proof 5.3**.**

First of all, observe that $\Omega^{\prime}$ is isomorphic to the object $(\mathcal{P}(\mathcal{S}),\sim)$ where

[TABLE]

Define a continuous function $F\colon\mathcal{S}\to\mathcal{S}$ by

[TABLE]

Next, define $\Phi\colon\mathcal{P}(\mathcal{S})\times\{0,1\}\to\mathcal{P}(\mathcal{S})$ by

[TABLE]

We show that $\Phi$ is a functional relation from $(\mathcal{P}(\mathcal{S}),\sim)$ to $\Sigma$. Strictness is immediate. For single-valuedness, suppose we have $[W,U,C]\in\Phi(\mathcal{U},i)$ and $[W^{\prime},U^{\prime},C^{\prime}]\in\Phi(\mathcal{U},j)$. We show that $i=j$. By definition, we have

[TABLE]

and similarly, $i=0\Rightarrow j=0$. Thus, $i=j$, as desired. Suppose $[W,U,C]\in\Phi(\mathcal{U},i)$ and $B\in[\mathcal{U}\leftrightarrow\mathcal{V}]$. We must effectively obtain an element of $\Phi(\mathcal{V},i)$. But if $B_{0}$ realizes $\mathcal{U}\to\mathcal{V}$, then one easily sees that $[W,B_{0}U,C]$ is an element of $\Phi(\mathcal{V},i)$. So, $\Phi$ is relational. For totality, suppose $[W,U]\in E(\mathcal{U})$, then $[W,U,F(W)]\in\Phi(\mathcal{U},i)$ for some $i\in\{0,1\}$, by construction of $E$ and $F$. We conclude that $\Phi$ is a functional relation.

Moreover, (the arrow represented by) $\Phi$ is easily seen to be epic. For, if $C\in E_{\Sigma}(i)$, then $[F(C),F(C),C]\in\Phi(\mathcal{U}_{i},i)$ with $\mathcal{U}_{1}=\{\overline{1}\}$ and $\mathcal{U}_{0}=\emptyset$ by construction of $F$ and definition of $E_{\Sigma}$.

Finally, we prove that $\Phi$ is monic and hence that $\Phi$ represents an isomorphism, as desired. Suppose we have $[W,U,C]\in\Phi(\mathcal{U},i)$ and $[W^{\prime},U^{\prime},C]\in\Phi(\mathcal{V},i)$. It suffices to effectively provide an element of $\mathcal{U}\leftrightarrow\mathcal{V}$, since $[W,U]$ is an element of $E(\mathcal{U})$ already. But $[\lambda x.U^{\prime},\lambda x.U]$ is easily seen to do the job.

Proposition 22 implies that we have a notion of $\Sigma$-subobjects of any object in $\mathsf{RT}(\mathcal{S})$: a mono $Y\to X$ represents a $\Sigma$-subobject of $X$ if and only if its classifying map factors through $\Sigma$. We write $U\subseteq_{\Sigma}X$ to indicate that $U$ is a $\Sigma$-subobject of $X$.

The following proposition characterizes these $\Sigma$-subobjects for assemblies $X$.

Proposition 23**.**

Let $X$ be an assembly. There is a bijective correspondence between morphisms $X\to\Sigma$ and subsets $X^{\prime}\subseteq|X|$ for which there is an open $\mathcal{U}\subseteq\mathcal{S}$ with the following properties:

[TABLE]

Moreover, an assembly $Y$ is a $\Sigma$-subobject of $X$ if and only if $Y$ is isomorphic to some assembly $(X^{\prime},E)$ where $X^{\prime}\subseteq|X|$ is as above and $E$ is the restriction of $E_{X}$ to $X^{\prime}$.

Proof 5.4**.**

Let $f$ be a morphism from $X$ to $\Sigma$ that is tracked by $U\in\mathcal{S}$. Set

[TABLE]

We show that $\mathcal{U}$ is open. Let $\mathcal{Q}\coloneqq\{p\subseteq\mathcal{S}\mid p\text{ is finite and }Up=\overline{1}\}$. Recall the notation $\uparrow\!p=\{V\in\mathcal{S}\mid p\subseteq V\}$. By continuity of the application, one can show that $\mathcal{U}=\bigcup_{p\in\mathcal{Q}}\uparrow\!p$. Thus, $\mathcal{U}$ is an open of $\mathcal{S}$.

From the definition of $\mathcal{U}$ and the fact that $U$ tracks $f$, it is immediate that $\mathcal{U}$ has the desired properties.

For the converse, assume we are given an open $\mathcal{U}\subseteq\mathcal{S}$ and a subset $X^{\prime}\subseteq|X|$ with the properties stated. Define $f\colon X\to\Sigma$ by $f(x)=1$ if $x\in X^{\prime}$ and $f(x)=0$ if $x\not\in X^{\prime}$. We claim that it is tracked by $\textup{graph}(F)$ where $F(U)=\{1\mid U\in\mathcal{U}\}$. That this $F$ is continuous follows from the assumption that $\mathcal{U}$ is open. Now if $x\in X$ and $U\in E_{X}(x)$, then either $f(x)=1$, in which case $E_{X}(x)\subseteq\mathcal{U}$, so that $F(U)=\overline{1}\in E_{\Sigma}(f(x))$; or $f(x)=0$, in which case $E(x)\cap\mathcal{U}=\emptyset$, so that $F(U)=\emptyset\in E_{\Sigma}(f(x))$. So $f$ is tracked, as desired.

That the operations above are each other’s inverses is readily verified. The final claim follows immediately from the construction above and the description of pullbacks in the category of assemblies.

The referee has suggested that Proposition 23 gives a notion of synthetic topology on $\mathsf{RT}(\mathcal{S})$ in the sense of [2]. However, observe the caveat after Proposition 27.

For any dominance $\Sigma\subset\Omega$ in a topos, one has for every object $X$ the partial map classifier for $\Sigma$-subobjects: that is, a $\Sigma$-subobject $\eta_{X}:X\to L(X)$ which classifies partial maps into $X$ defined on a $\Sigma$-subobject. It follows that $L$ is a functor (generally dubbed the “lift functor”) and $\eta$ is a natural transformation from the identity functor to $L$. Now Propositions 21 and 22 together imply that the functor $L$ restricts to an endofunctor on the category of assemblies. The following proposition describes this restriction explicitly.

Proposition 24**.**

The lift functor $L$ on ${\sf Ass}({\mathcal{S}})$ is given by on objects by:

[TABLE]

where $\bot_{X}$ is some element not in $|X|$ and

[TABLE]

Given an arrow $f\colon X\to Y$, we define $L(f)$ as the unique extension of $f$ satisfying $\bot_{X}\mapsto\bot_{Y}$. The natural transformation $\eta\colon\operatorname{\textup{id}}_{\mathsf{Ass}(\mathcal{S})}\to L$ is defined as $\eta_{X}(x)=x$.

Proof 5.5**.**

Given a morphism $f\colon X\to Y$ of $\mathsf{Asm}(\mathcal{S})$ tracked by $U_{f}\in\mathcal{S}$, note that $L(f)$ is tracked, as

[TABLE]

is a continuous map $\mathcal{S}\to\mathcal{S}$. Verifying that $L$ is indeed a functor is routine. Also, note that $\eta_{X}$ is tracked by $\lambda{u}.[u,\overline{1}]$. That $\eta$ is natural is easily checked.

Finally, suppose we have a morphism $f\colon U\to Y$ and $U\subseteq_{\Sigma}X$. By Proposition 23, we may assume that we have $|U|\subseteq|X|$ and an open $\mathcal{U}$ such that for $x\in|X|$:

[TABLE]

Define $\tilde{f}\colon X\to L(Y)$ by

[TABLE]

Note that $\tilde{f}$ is tracked, for if $f$ is tracked by $U_{f}$, then

[TABLE]

is a continuous map $\mathcal{S}\to\mathcal{S}$, because $\mathcal{U}$ is open.

If we have morphisms $g\colon Z\to X$ and $h\colon Z\to Y$ such that $\tilde{f}g=\eta_{Y}h$, then we must have that $g(z)\in|U|$ for any $z\in|Z|$. Hence, $g$ factors uniquely through $(U,E_{U})$. This proves that $\tilde{f}$ makes the square

[TABLE]

into a pullback.

It remains to show that it is unique with this property. To this end, suppose we have $f^{\prime}\colon X\to L(Y)$, such that the square

[TABLE]

is a pullback. From the commutativity of the square, it follows that for $x\in|U|$ we must have $f^{\prime}(x)=f(x)=\tilde{f}(x)$. Now suppose for a contradiction that we have $x_{0}\in|X|\setminus|U|$ and $f^{\prime}(x_{0})\in|Y|$. The universal property of the pullback then yields a map $U\cup\{x_{0}\}\to U$ such that the inclusion $|U|\cup\{x_{0}\}\to|X|$ factors through $|U|$, but this is impossible, as $x_{0}\not\in|U|$. Hence, no such $x_{0}$ exists and therefore, $f^{\prime}$ and $\tilde{f}$ coincide.

Remark 25**.**

Observe that $L(1)\cong\Sigma$ and that $\eta_{1}=1\xrightarrow{t}\Sigma$.

Lemma 26**.**

For any $X$, we have $X\subseteq_{\Sigma}L(X)$ via $\eta_{X}$.

Proof 5.6**.**

It is straightforward to verify that

[TABLE]

with $\chi_{X}(x)=1$ and $\chi_{X}(\bot_{X})=0$ is a pullback. (Note the map $F(V)=\overline{1}$ if $1\in\mathsf{p_{1}}V$ and $\emptyset$ otherwise is continuous and its graph tracks $\chi_{X}$.)

As always, the lift functor $L$ is a monad on ${\sf Ass}({\mathcal{S}})$. The multiplication $\mu\colon L^{2}(X)\to L(X)$ is given by the map $x\mapsto x,\bot_{X}\mapsto\bot_{X},\bot_{L(X)}\mapsto\bot_{X}$.

6. A notion of homotopy for the order-discrete objects

In [14], a notion of homotopy for the Effective Topos is given. This notion is tied up with the subcategory of discrete objects, in the following way: internally, for each object $X$, the “discrete reflection” of $X$ is the set of path components of $X$. It is just natural to wonder whether this would also work for the order-discrete objects in ${\sf RT}({\mathcal{S}})$.

Another interpretation of homotopy for the Effective Topos is in the paper [3] by Dan Frumin and Benno van den Berg. They build a very elegant framework on purely category-theoretic notions. The basic ingredients are: an interval object $\mathbb{I}$ with two distinct points $\partial_{0},\partial_{1}:1\to\mathbb{I}$ , binary maps $\wedge,\vee:I\times I\to I$ satisfying some axioms, and a dominance $\Sigma$ which is closed under finite unions and satisfies the condition that the inclusion $[\partial_{0},\partial_{1}]:1+1\to\mathbb{I}$ is a $\Sigma$-subobject. From these notions, a subcategory of “fibrant objects” is defined, and there is a Quillen model structure on this subcategory. When applying to the Effective Topos they take the trivial dominance: $\Omega$ itself.

In ${\sf RT}({\mathcal{S}})$ we have an interesting dominance: the Sierpiński object. However, the Frumin-van den Berg framework is not applicable for this dominance, as the following proposition shows.

Proposition 27**.**

The Sierpiński object, as subobject of $\Omega$, is not closed under finite unions.

Proof 6.1**.**

We apply the characterization 22. Let the variables $X,Y,Z$ range over the object of realizers $S$ (which in turn is seen as subobject of ${\mathcal{P}}(N)$). We prove that the statement

[TABLE]

is not valid in ${\sf RT}({\mathcal{S}})$. Indeed, working out the realizability of $(\ast)$, we see that we need continuous functions $F$ and $G$ on $\mathcal{S}$ such that for all $U,V\in{\mathcal{S}}$ we have:

• •

If $1\in U$ or $1\in V$ then $1\in F(U,V)$.

• •

If $1\in F(U,V)$ then either $G(F(U,V))=\overline{0}$ and $1\in U$, or $G(F(U,V))=\overline{1}$ and $1\in V$.

However, this is impossible: consider $G(F(\{1\},\{1\}))$. If this is equal to $\overline{0}$ then by continuity we cannot have $G(F(\emptyset,\{1\}))=\overline{1}$; the other case is similar.

Caveat: note that if we interpret Escardó’s “synthetic topology” in ${\sf RT}({\mathcal{S}})$, we see from Proposition 27 that this topology will not be standard, but “substandard” in the terminology of [2].

In view of Proposition 27, we revert to the more ‘hands-on’ approach of [14]. The main extra complication is the essential asymmetry of the object $\Sigma$. In the effective topos case, we had for every natural number $n$ a ‘generic interval’ $I_{n}$ (which essentially is an iterated pushout of copies of $\nabla(2)$). Here, we have more generic intervals, indexed by 01-sequences. {defi} For each natural number $n\geq 1$ and each 01-sequence $\sigma=(\sigma_{0},\ldots,\sigma_{n-1})$ we define the assembly $I_{n,\sigma}=(\{0,\ldots,n\},E_{n,\sigma})$ where:

[TABLE]

So, each set $E_{n,\sigma}(k)$ consists of two elements $\alpha_{k}$, $\beta_{k}$ which satisfy the following conditions:

• •

${\sf p}_{0}\alpha_{k}=\overline{k}$, ${\sf p}_{0}\beta_{k}=\overline{k+1}$;

• •

$\beta_{k}\subset\alpha_{k+1}$ if $\sigma_{k}=0$;

• •

$\beta_{k}\supset\alpha_{k+1}$ if $\sigma_{k}=1$.

The object $I_{n,\sigma}$ is called a generic interval of length $n$.

Proposition 28**.**

Let $(X,\sim)$ be an arbitrary object of ${\sf RT}({\mathcal{S}})$ and let $I_{n,\sigma}$ be a generic interval of length $n$. The exponent $(X,\sim)^{I_{n,\sigma}}$ can be described as follows: its underlying set is the set of $2n+2$-tuples $(\vec{x},\vec{y})=(x_{0},y_{0},\ldots,x_{n},y_{n})$ of elements of $X$. Given such a tuple, we define $E(\vec{x},\vec{y})$ as the set of coded $3n-2$-tuples (coded in the sense of $\mathcal{S}$)

[TABLE]

of elements of $\mathcal{S}$ such that we have:

• •

$U_{k}\in[x_{k}\sim y_{k}]$* for $0\leq k\leq n$;*

• •

$V_{k}\in[y_{k}\sim y_{k}]$, $W_{k}\in[x_{k+1}\sim x_{k+1}]$ for $0\leq k<n$;

• •

$V_{k}\subseteq W_{k}$* if $\sigma_{k}=0$, and $V_{k}\supseteq W_{k}$ if $\sigma_{k}=1$.*

For two such tuples $(\vec{x},\vec{y}),(\vec{x^{\prime}},\vec{y^{\prime}})$, the set $[(\vec{x},\vec{y})\approx(\vec{x^{\prime}},\vec{y^{\prime}})]$ is the set of coded triples (in the sense of $\mathcal{S}$) $[\alpha,\beta,\gamma]$ of elements of $\mathcal{S}$, which satisfy:

• •

$\alpha\in E(\vec{x},\vec{y})$;

• •

$\beta\in E(\vec{x^{\prime}},\vec{y^{\prime}})$;

• •

$\beta\overline{k}\in[x_{k}\sim x^{\prime}_{k}]$* for $0\leq k\leq n$.*

Proof 6.2**.**

This is left to the reader, who may find it useful to review Proposition 3. It should be noted that realizers of elements of $(X,\sim)^{I_{n,\sigma}}$ don’t contain information about $\sigma$. This is not necessary, since for any $V,W\in{\mathcal{S}}$ we have a continuous endomap on $\mathcal{S}$ which sends ${\sf p}\overline{k}\emptyset$ to $V\cap W$ and ${\sf p}\overline{k}\,\overline{1}$ to $V\cup W$, so it is enough to know that some inclusion between $U_{k},V_{k}$ exists. Note also that the number $n$ can be retrieved from any element of $E(\vec{x},\vec{y})$.

{defi}

As in [14], we say that an arrow $I_{n,\sigma}\to I_{m,\tau}$ is order and end-point preserving if its underlying function: $\{0,\ldots,n\}\to\{0,\ldots,m\}$ is so (with respect to the usual order). {defi} Let $(X,\sim)$ be an object of ${\sf RT}({\mathcal{S}})$. Its path object ${\sf P}(X,\sim)$ defined as follows. Its underlying set is the set of all tuples $(x_{0},y_{0},\ldots,x_{n},y_{n})$, which we write as $(\phi,n)$. For two such tuples $(\phi,n)$ and $(\psi,m)$ we let $[(\phi,n)\sim(\psi,m)]$ be the set of coded triples (in the sense of $\mathcal{S}$) $[\alpha,s,\beta]$ of elements of $\mathcal{S}$ such that for suitable 01-sequences $\sigma,\tau$ we have:

1. (1)

$\alpha\in E(\phi,n)$ as element of $(X,\sim)^{I_{n,\sigma}}$; 2. (2)

$\beta\in E(\psi,m)$ as element of $(X,\sim)^{I_{m,\tau}}$; 3. (3)

There are order and endpoint preserving maps $I_{p,\rho}\stackrel{{\scriptstyle f}}{{\to}}I_{n,\sigma}$, $I_{p,\rho}\stackrel{{\scriptstyle g}}{{\to}}I_{m,\tau}$ such that $s\in[\phi f\approx\psi g]$ in the sense of $(X,\sim)^{I_{p,\rho}}$.

Remark 29**.**

The third clause corrects an inaccuracy in Definition 2.5 of [14], which was noted in [3].

With this definition of path object we can now mimick [14] and prove the following theorem:

Theorem 30**.**

1. (1)

The construction of ${\sf P}(X,\sim)$ extends to an endofunctor on ${\sf RT}({\mathcal{S}})$, which preserves finite limits. 2. (2)

The object ${\sf P}(X,\sim)$ comes equipped with well-defined maps:

• ${\sf s}$* (source), $\sf t$ (target): ${\sf P}(X,\sim)\to(X,\sim)$;*
• $\sf c$* (constant path): $(X,\sim)\to{\sf P}(X,\sim)$;*
• $\ast$* (composition of paths): ${\sf P}(X,\sim)\times_{(X,\sim)}{\sf P}(X,\sim)\to{\sf P}(X,\sim)$ where the domain is the pullback $\{(x,y)\,|\,{\sf t}(x)={\sf s}(y)\}$;*
• $\widetilde{(-)}$* (converse path): ${\sf P}(X,\sim)\to{\sf P}(X,\sim)$.*

Moreover, with these data the object ${\sf P}(X,\sim)$ has the structure of an internal category in ${\sf RT}({\mathcal{S}})$ with a contravariant involution which is the identity on objects.

Proposition 31**.**

The set of path components of $(X,\sim)$, i.e. the quotient of $(X,\sim)$ by the equivalence relation “there is a path from $x$ to $y$”, is exactly the order-discrete reflection of $(X,\sim)$.

Proof 6.3**.**

Inspection of Remark 11 and Definition 6.

Just as in [14], we see that we have a “path object category” in the sense of Van den Berg and Garner ([13]). {exa} For a countably based $T_{0}$-space, its image under the embedding in ${\sf RT}({\mathcal{S}})$ is always discrete (that is the $T_{0}$-property); it is order-discrete if and only if the space is $T_{1}$. For any $T_{0}$-space $X$, the specialization order on $X$ is the partial order defined by: $x\leq y$ if and only if every open set which contains $x$, also contains $y$ (in the notation of the introduction: $e(x)\subseteq e(y)$, if the embedding of X is $(X,E_{X})$ with $E_{X}(x)=\{e(x)\}$). We can see this order relation as an undirected graph on $X$. A path from $x$ to $y$ is just a path in this graph.