Notation. We write $p\ast x$ as the output result of feeding an input x to the realizable function coded by p. For instance, $e\ast x$ in $\mathsf {K}_1$ stands for $\{e\}(x)$ or $\varphi _e(x)$ in traditional notation.

Observation 3.3. A represented space A is a subobject of X iff $|A|\subseteq |X|$ and the inclusion map $i\colon A\rightarrowtail X$ is a morphism.

A represented space A is a regular subobject of X iff it is a subobject of X and the inclusion morphism $i\colon A\rightarrowtail X$ has a partial inverse morphism $i^{-1}\colon \!\!\!\subseteq X\to A$ ; that is, $i^{-1}(i(x))=x$ for any $x\in |A|$ .

Observation 3.5. A subspace of X is a regular subobject of X. Conversely, every regular subobject of X is equivalent to a subspace of X.

Observation 3.7. A witnessed subset of X is a subobject of X. Conversely, every subobject of X is equivalent to a witnessed subset of X.

Proof. For a witnessed subset A of X, the inclusion map $i\colon A\hookrightarrow X$ is clearly tracked by the projection map $\pi _1\colon \langle w,p\rangle \mapsto p$ . Conversely, if A is a subobject of X, that is, $i\colon A\hookrightarrow X$ is tracked by some f, then consider the following represented space $A_f$ : The underlying set is $|A_f|=|A|$ , and $\langle w,p\rangle $ is a name of $x\in A_f$ iff w is a name of $x\in A$ and $p=f(w)$ . Then, $A_f$ is clearly a witnessed subset of X. Moreover, $A_f\subseteq A$ is tracked by $\pi _0\colon \langle w,p\rangle \mapsto w$ , and $A\subseteq A_f$ is tracked by $w\mapsto \langle w,f(w)\rangle $ .

Proof. Suppose that $\mathsf {Fin}$ is regular. Then, there exists a partial realizable function F which, given $x\in |\mathsf {Fin}|$ , returns an $\mathsf {Fin}$ -name of x, say $F(x)=\langle n,x\rangle $ . By the continuity of F, the witness n is determined after reading a finite initial segment $x\upharpoonright s$ of x. Put $t=\max \{n,s\}$ , and consider $y=(x\upharpoonright t)\text {}^\smallfrown 1\text {}^\smallfrown 0^\infty $ . Then $y\in |\mathsf {Fin}|$ , so $F(y)$ returns a name of $y\in \mathsf {Fin}$ ; that is, $F(y)$ is of the form $\langle m,y\rangle $ . As y extends $x\upharpoonright s$ , the first value of $F(y)$ must be n; hence $F(y)=\langle n,y\rangle $ . However, we have $t\geq n$ and $y(t)=1$ , which means that $\langle n,y\rangle $ is not an $\mathsf {Fin}$ -name of y.

Observation 3.10. $(\mathrm {Sub}(X),\subseteq )$ is a poset.

Proof of Proposition 3.11

We show that the witnessed union $\uplus $ and the intersection give the join and the meet in any subobject poset. Let $X,Y$ be subobjects of Z. Then the inclusion maps $X\hookrightarrow X\uplus Y$ and $Y\hookrightarrow X\uplus Y$ are tracked by $a\mapsto \langle 0,a\rangle $ and $b\mapsto \langle 1,b\rangle $ , respectively. Now, let $S\rightarrowtail Z$ be such that $X,Y\subseteq S$ . Then the inclusion maps $X\hookrightarrow S$ and $Y\hookrightarrow S$ are tracked by some u and v, respectively. Then consider the process that, given a name $\langle i,p\rangle $ of $x\in X\uplus Y$ , if $i=0$ then returns $u(p)$ else $v(p)$ . Note that if $i=0$ then $p\vdash _X x$ , so $u(p)\vdash _S x$ . Similarly, if $i\not =0$ then $p\vdash _Y x$ , so $v(p)\vdash _Sx$ . Thus, in any case, the above process yields a name of $x\in S$ . This means that $X\uplus Y$ is included in S. Hence, $X\uplus Y$ is the join of X and Y in the poset of subobjects of Z.

Next, the inclusion maps and are tracked by projections $\pi _0$ and $\pi _1$ , respectively. Now, let $S\rightarrowtail Z$ be such that $S\subseteq X,Y$ . Then the inclusion maps $S\hookrightarrow X$ and $S\hookrightarrow Y$ are tracked by some u and v, respectively. Then $p\mapsto \langle u(p),v(p)\rangle $ tracks the inclusion map . To see this, if $p\vdash _S x$ then $u(p)\vdash _Xx$ and $v(p)\vdash _Yx$ , so . This means that S is included in . Hence, is the meet of X and Y in the poset of subobjects of Z.

To see that is the Heyting operation, for subobjects $A,B,C\rightarrowtail Z$ , first assume , which is realized by u. If $\langle p,q \rangle $ is a name of then, since p is an A-name of x, $u(p)$ is a -name of x by our assumption. If $u(p)$ is of the form $\langle u_0(p),u_1(p) \rangle $ , as q is a B-name of x, $u_1(p)\ast q$ is a C-name of x. This shows . Conversely, assume , which is realized by u. Assume that p is a name of $x\in A$ . As A is a subobject of Z, the inclusion map $A\rightarrowtail Z$ is tracked by some i, so $i(p)$ is a Z-name of x. If $x\not \in B$ then anything is a -name of x. If q is a name of $x\in B$ then $\langle p,q\rangle $ is a -name of x, so $u(p,q)$ is a C-name of x. Hence, $\langle i(p),\lambda q.u(p,q) \rangle $ is a -name of x. Note that $\lambda q.u(p,q)$ is always defined, and thus $\lambda p.\langle i(p),\lambda q.u(p,q) \rangle $ tracks the inclusion .

Proof. For the non-existence of $\sigma $ -join, for each $n\in \omega $ , think of the singleton $\{n\}$ as a subspace of $\omega $ . Let $I\rightarrowtail \omega $ be such that $\{n\}\subseteq I$ in $\mathrm {Sub}(\omega )$ for any $n\in \omega $ . Then $|I|=\omega $ . Let $E_I(n)$ be the set of all I-names of $n\in \omega $ . Since $E_I(n)\not =\emptyset $ for all $n\in \omega $ , take the least element $s(n)\in E_I(n)$ . Construct a new subobject $J\rightarrowtail \omega $ as follows: The underlying set is $|J|=\omega $ , and the only J-name of $n\in \omega $ is $s'(n)$ , where $s'$ is the Turing jump of s. Clearly, $\{n\}\subseteq J$ holds in $\mathrm {Sub}(\omega )$ for any $n\in \omega $ . If $I\subseteq J$ in $\mathrm {Sub}(\omega )$ then some computable function f tracks the inclusion $I\hookrightarrow J$ . Since $s(n)$ is an I-name of n, $f(s(n))$ must be a J-name of n, which means $f(s(n))=s'(n)$ . This implies that the jump $s'$ is Turing reducible to s, a contradiction. Hence, $I\not \subseteq J$ , which shows that any I cannot be a $\sigma $ -join of the singletons $\{n\}$ .

For the non-existence of $\sigma $ -meet, consider a sequence $g_0<_Tg_1<_T\dots $ , where $\leq _T$ is Turing reducibility. For each $i\in \omega $ , consider a subobject $A_i\rightarrowtail \omega $ such that its underlying set is $|A_i|=\omega $ and $g_i(n)$ is a unique name of $n\in A_i$ . Assume that $B\rightarrowtail \omega $ is a subobject such that $B\subseteq A_i$ for any $i\in \omega $ . We construct a subobject $C\rightarrowtail \omega $ such that $C\subseteq A_i$ for any $i\in \omega $ but $C\not \subseteq B$ . Put $|C|=\omega $ . We inductively define an increasing sequence $(n_e)_{e\in \omega }$ with $n_0=0$ . Assume that $n_e$ has already been defined. If the eth partial computable function $\varphi _e$ is not total then put $n_{e+1}=n_e+1$ . If $\varphi _e$ is total, we claim that there exists $n\geq n_e$ such that $\varphi _e(\langle g_i(n)\rangle _{i\leq e})$ is not a name of $n\in B$ . This is because, since $B\subseteq A_{e+1}$ , if one knows a name of $n\in B$ one can compute $g_{e+1}(n)$ . Thus, if the claim fails then we get $g_{e+1}\leq _T\bigoplus _{i\leq e}g_i\equiv _T g_e$ , a contradiction. Define $n_{e+1}=n+1$ where n is a number in the above claim. Then declare that, if $n_e\leq n<n_{e+1}$ , then $\langle g_i(n)\rangle _{i\leq e}$ is a unique name of $n\in C$ . For almost all n, the ith coordinate of a name of $n\in C$ yields a name of $A_i$ , so we have $C\subseteq A_i$ . Moreover, the above construction ensures that $\varphi _e$ cannot be a tracker of the inclusion $C\subseteq B$ for any e, which means that $C\not \subseteq B$ . Consequently, any B cannot be a $\sigma $ -meet of $(A_i)_{i\in \omega }$ .

Observation 3.24. Definition 3.23 is equivalent to Definition 3.21 in the category of represented spaces.

Proof. Definition 3.23 states that the subobject $A\rightarrowtail X$ is equivalent to the pullback $\varphi ^\ast B\rightarrowtail X$ in Definition 3.22. Indeed, if u is a tracker of $\varphi $ , then $p\mapsto \langle u(p),r_-(p) \rangle $ tracks $A\subseteq \varphi ^\ast B$ , and $r_+$ tracks $\varphi ^\ast B\subseteq A$ . Thus, $A\rightarrowtail X$ is also a pullback of $B\rightarrowtail Y$ along $\varphi $ . Conversely, if a subobject $A\rightarrowtail X$ is a pullback of $B\rightarrowtail Y$ along $\varphi $ , then one can easily see that A is equivalent to $\varphi ^\ast B$ .

Observation 3.29. $A\leq _{\mathsf {m}}B\implies A\leq _{\mathsf {m}}'B$ .

Observation 3.30. $A\leq _{\mathsf {m}}'B$ iff there exists a morphism $\varphi $ such that $\varphi ^\ast B\subseteq A\subseteq (\varphi ^\ast B)^{\neg \neg }$ .

Observation 3.31. If $A,B\rightarrowtail X$ are regular then $A\leq _{\mathsf {m}}B$ iff $A\leq _{\mathsf {m}}'B$ .

Observation 3.32. $\leq _{\mathsf {m}}$ and $\leq _{\mathsf {m}}'$ form preorders.

Proof. The proof for the many-one case follows from a general argument, but we give an explicit description applicable to the demi-many-one case. Reflexivity is trivial. For transitivity, for subobjects $A,B,C$ of $X,Y,Z$ , assume $A\leq _{\mathsf {m}}B$ via $\varphi ,r_-,r_+$ and $B\leq _{\mathsf {m}}C$ via $\psi ,s_-,s_+$ . Only an outer reduction is nontrivial. Let p be a tracker of $\varphi $ . Given a name a of $x\in X$ we know that $p\ast a$ is a name of $\varphi (x)\in Y$ . Thus, given a name c of $\psi (\varphi (x))\in C$ , $s^+(p\ast a,c)$ is a name of $\varphi (x)\in B$ , and $r^+(a,s^+(p\ast a,c))$ is a name of $x\in A$ . This process gives an outer reduction for $A\leq _{\mathsf {m}}C$ . This actually shows that $\leq _{\mathsf {m}}'$ is a preorder.

Proof. Again, the proof for the many-one case follows from a general argument, but we give an explicit description applicable to the demi-many-one case. We construct a join of subobjects $A\rightarrowtail X$ and $B\rightarrowtail Y$ . The coproduct $X+Y$ of represented spaces X and Y are defined as follows:

• • The underlying set is $|X+Y|=\{(0,x):x\in X\}\cup \{(1,y):y\in Y\}$ .

• • $\langle i,p \rangle $ is a name of $(j,z)$ iff $i=j$ and if $i=0$ then p is a name of $z\in X$ else p is a name of $z\in Y$ .

One can think of $A+B$ as a subobject of $X+Y$ . Clearly, $A,B\leq _{\mathsf {m}}A+B$ . Assume that C is a subobject of Z such that $A\leq _{\mathsf {m}}C$ via $\varphi ,r_-,r_+$ and $B\leq _{\mathsf {m}}C$ via $\psi ,s_-,s_+$ . Let $[\varphi ,\psi ]\colon X+Y\to Z$ be a morphism such that, for any $(i,x)\in X+Y$ , if $i=0$ then $[\varphi ,\psi ](i,x)=\varphi (x)$ else $[\varphi ,\psi ](i,x)=\psi (x)$ . Given $\langle i,u \rangle \vdash _{A+B}(i,x)$ , if $i=0$ then $r_-(u)\vdash _C\varphi (x)=[\varphi ,\psi ](i,x)$ else $s_-(u)\vdash _C\psi (x)=[\varphi ,\psi ](i,x)$ . Given $\langle i,u \rangle \vdash _{X+Y}(i,x)$ and $c\vdash _C[\varphi ,\psi ](i,x)$ , if $i=0$ then $[\varphi ,\psi ](i,x)=\varphi (x)$ , so $r_+(u,c)\vdash _Ax$ ; thus $\langle 0,r_+(u,c) \rangle \vdash _{A+B}(i,x)$ . Similarly, if $i\not =0$ then $\langle 1,r_+(u,c) \rangle \vdash _{A+B}(i,x)$ . This shows $A+B\leq _{\mathsf {m}}C$ . By a similar argument, one can show that $\leq _{\mathsf {m}}'$ also yields an upper semilattice.

Proof. First consider $\leq _{\mathsf {m}}'$ . Given subobjects $A\rightarrowtail X$ and $B\rightarrowtail Y$ , we define the space $A\odot B$ of common information of A and B as follows: First consider the subspace $C(A,B)$ of $\mathtt {Code}$ such that $\langle p,q,n \rangle \in |C(A,B)|$ iff

$$\begin{align*}(\exists x,y)\;[({p\ast n\downarrow}\vdash_Xx)\ \&\ ({q\ast n\downarrow}\vdash_Yy)\ \&\ (x\in |A|\iff y\in |B|)].\end{align*}$$

Then the equivalence relation $\sim $ on $C(A,B)$ is defined as follows:

$$\begin{align*}\langle p,q,n \rangle\sim\langle p,q,m \rangle\iff \delta_X(p\ast n)=\delta_X(p\ast m)\ \&\ \delta_Y(q\ast n)=\delta_Y(q\ast m).\end{align*}$$

Then let $A\odot B$ be the quotient space $C(A,B)/{\sim }$ ; that is, an $(A\odot B)$ -name of a $\sim $ -equivalence class $[p,q,n]$ is of the form $\langle p,q,m \rangle $ for some $\langle p,q,m \rangle \in [p,q,n]$ . Then we define a subobject $A\Cap B\rightarrowtail A\odot B$ as follows:

• • $[p,q,n] \in |A\Cap B|$ iff $[p,q,n]\in |A\odot B|$ and $\delta _X(p\ast n)\in |A|$ .

• • $\langle i,u,v\rangle $ is a name of $[p,q,n]\in A\Cap B$ iff u is a name of $[p,q,n]\in A\odot B$ and if $i=0$ then v is a name of $\delta _X(p\ast n)\in A$ else v is a name of $\delta _Y(q\ast n)\in B$ .

To see that $A\Cap B\leq _{\mathsf {m}}' A$ , consider $\varphi \colon [p,q,n]\mapsto \delta _X(p\ast n)$ , which is well-defined. If $[p,q,n]\in |A\odot B|$ then ${\varphi ([p,q,n])\downarrow }\in X$ since $\langle p,q,n \rangle \in C(A,B)$ . Thus, $[p,q,n]\in |A\Cap B|$ iff $\varphi ([p,q,n])\in |A|$ . Moreover, if $\langle p,q,m \rangle $ is a name of $[p,q,m]\in A\odot B$ and v is a name of $\varphi ([p,q,n])\in A$ then $\langle 0,p,q,m,v\rangle $ is a name of $[p,q,n]\in A\Cap B$ .

Similarly, to see that $A\Cap B\leq _{\mathsf {m}}' B$ , consider $\varphi \colon [p,q,n]\mapsto \delta _Y(q\ast n)$ , which is well-defined. If $[p,q,n]\in |A\odot B|$ then ${\varphi ([p,q,n])\downarrow }\in Y$ . By definition, $[p,q,n]\in |A\Cap B|$ iff $\delta _X(p\ast n)\in |A|$ , iff $\varphi ([p,q,n])=\delta _X(q\ast n)\in |B|$ since $\langle p,q,n\rangle \in C(A,B)$ . Moreover, if $\langle p,q,m \rangle $ is a name of $[p,q,m]\in A\odot B$ and v is a name of $\varphi ([p,q,n])\in B$ then $\langle 1,p,q,m,v\rangle $ is a name of $[p,q,n]\in A\Cap B$ .

For a subobject $C\rightarrowtail Z$ , if $C\leq _{\mathsf {m}}'A,B$ then there are $\varphi ,\psi $ such that, for any $x\in |Z|$ , $x\in |C|$ iff $\varphi (x)\in |A|$ and $\psi (x)\in |B|$ . We also have $r,s$ such that if u is a name of $\varphi (x)\in A$ then $r\ast u$ is a name of $x\in C$ , and if v is a name of $\psi (x)\in B$ then $s\ast v$ is a name of $x\in C$ .

To show $C\leq _{\mathsf {m}}'A\Cap B$ , let p and q be trackers of $\varphi $ and $\psi $ , respectively. Then if k is a name of some $x\in Z$ , then $k\vdash _Z x\in |C|$ iff ${p\ast k\downarrow }\vdash _X\varphi (x)\in |A|$ iff ${q\ast k\downarrow }\vdash _Y\psi (x)\in |B|$ . Hence, $[p,q,k]\in |A\odot B|$ , and moreover, $k\vdash _Z x\in |C|$ iff $[p,q,k]\in |A\Cap B|$ . Moreover, if k and $\ell $ are names of $x\in Z$ , then $\delta _X(p\ast k)=\delta _X(p\ast \ell )=\varphi (x)$ and $\delta _Y(q\ast k)=\delta _Y(q\ast \ell )=\psi (x)$ ; hence $[p,q,k]=[p,q,\ell ]$ . Therefore, $k\mapsto \langle p,q,k\rangle $ tracks some morphism $\theta \colon Z\to A\odot B$ such that $x\in |C|$ iff $[p,q,k]\in |A\Cap B|$ . Given a name $\langle i,u,v\rangle $ of $[p,q,k]\in A\Cap B$ , if $i=0$ then v is a name of $\delta _X(p\ast k)=\varphi (x)\in A$ , so $r\ast v$ is a name of $x\in C$ . If $i\not =0$ then v is a name of $\delta _Y(q\ast k)=\psi (x)\in B$ , so $s\ast v$ is a name of $x\in C$ . This completes the proof.

The proof for $\leq _{\mathsf {m}}$ is almost the same, but the construction is a little more complicated. Consider the subspace $D(A,B)$ of $\mathtt {Code}$ such that $\langle p,q,a,b,c,d,n \rangle \in |D(A,B)|$ iff $\langle p,q,n \rangle \in |C(A,B)|$ and the following hold:

• • If v is a name of $\delta _X(p\ast n)\in A$ then $a\ast (c\ast v)$ is a name of $\delta _X(p\ast n)\in A$ and $b\ast (c\ast v)$ is a name of $\delta _Y(q\ast n)\in B$ .

• • If v is a name of $\delta _Y(q\ast n)\in B$ then $a\ast (d\ast v)$ is a name of $\delta _X(p\ast n)\in A$ and $b\ast (d\ast v)$ is a name of $\delta _Y(q\ast n)\in B$ .

The construction after this is exactly the same as in the previous one, except for the additional information $\alpha =(a,b,c,d)$ .

To see that $A\Cap B\leq _{\mathsf {m}} A$ , consider $\varphi \colon [p,q,\alpha ,n]\mapsto \delta _X(p\ast n)$ , which is well-defined. If $[p,q,\alpha ,n]\in |A\odot B|$ then ${\varphi ([p,q,\alpha ,n])\downarrow }\in X$ since $\langle p,q,n \rangle \in C(A,B)$ . Thus, $[p,q,\alpha ,n]\in |A\Cap B|$ iff $\varphi ([p,q,\alpha ,n])\in |A|$ . Moreover, if $\langle p,q,\alpha ,m \rangle $ is a name of $[p,q,\alpha ,m]\in A\odot B$ and v is a name of $\varphi ([p,q,\alpha ,n])\in A$ then $\langle 0,p,q,\alpha ,m,v\rangle $ is a name of $[p,q,\alpha ,n]\in A\Cap B$ . Conversely, assume that $\langle 0,p,q,\alpha ,m,v\rangle $ is a name of $[p,q,\alpha ,n]\in A\Cap B$ . If $i=0$ then v is a name of $\delta _X(p\ast n)\in A$ . If $i=1$ then v is a name of $\delta _Y(q\ast n)\in B$ , so $a\ast (d\ast v)$ is a name of $\delta _X(p\ast n)\in A$ . By the same argument, one can also show $A\Cap B\leq _{\mathsf {m}} B$ .

For a subobject $C\rightarrowtail Z$ , if $C\leq _{\mathsf {m}}A,B$ then there are $\varphi ,\psi $ such that, for any $x\in |Z|$ , $x\in |C|$ iff $\varphi (x)\in |A|$ and $\psi (x)\in |B|$ . Let p and q be trackers of $\varphi $ and $\psi $ , respectively. Then if k is a name of some $x\in Z$ , then $k\vdash _Z x\in |C|$ iff ${p\ast k\downarrow }\vdash _X\varphi (x)\in |A|$ iff ${q\ast k\downarrow }\vdash _Y\psi (x)\in |B|$ . We also have $a,b,c,d$ such that $v\vdash _A\varphi (x)$ implies $c\ast v\vdash _Cx$ ; $v\vdash _B\psi (x)$ implies $d\ast v\vdash _Cx$ ; and $v\vdash _Cx$ implies $a\ast v\vdash _A\varphi (x)$ and $b\ast v\vdash _B\psi (x)$ . In particular, $v\vdash _A\varphi (x)$ implies $a\ast (c\ast v)\vdash _A\varphi (x)$ and $b\ast (c\ast v)\vdash _B\psi (x)$ , and $v\vdash _B\psi (x)$ implies $a\ast (d\ast v)\vdash _A\varphi (x)$ and $b\ast (d\ast v)\vdash _B\psi (x)$ . As $\varphi (x)=\delta _X(p\ast k)$ and $\psi (x)=\delta _Y(q\ast k)$ , this implies $\langle p,q,\alpha ,n\rangle \in D(A,B)$ . The rest of the proof of $C\leq _{\mathsf {m}}A\Cap B$ is the same as before.

To show distributivity, first consider $\leq _{\mathsf {m}}'$ . For subobjects $A,B,C$ of $X,Y,Z$ , it suffices to show $(A+B)\Cap (A+C)\leq _{\mathsf {m}}' A+(B\Cap C)$ . We construct a reduction $\varphi $ as follows: Given $[p,q,n]\in |(A+B)\odot (A+C)|$ , assume that $p\ast n$ and $q\ast n$ are of the forms $\langle i,u\rangle $ and $\langle j,v\rangle $ , respectively. If $i=0$ then define $\varphi ([p,q,n])=\langle 0,\delta _X(u) \rangle $ else if $j=0$ then $\varphi ([p,q,n])=\langle 0,\delta _X(v) \rangle $ . For instance, if $i=1$ and $j=0$ then $\delta _Y(u)\in |B|$ iff $\delta _X(v)\in |A|$ ; hence $[p,q,n]\in |(A+B)\Cap (A+C)|$ iff $\delta _X(v)\in |A|$ iff $\varphi ([p,q,n])=\langle 0,\delta _X(v) \rangle \in |A+(B\Cap C)|$ . If $i\not =0$ and $j\not =0$ then let $p_1$ and $q_1$ be such that $p_1\ast n=u$ and $q_1\ast n=v$ and then define $\varphi ([p,q,n])=\langle 1,[p_1,q_1,n]\rangle $ . As $\delta _Y(u)\in |B|$ iff $\delta _Z(v)\in |C|$ iff $[p_1,q_1,n]\in |B\Cap C|$ iff $\varphi ([p,q,n])\in |A+(B\Cap C)|$ . For an outer reduction, given a name $\langle p,q,m \rangle $ of $[p,q,n]\in (A+B)\odot (A+C)$ and a name $\langle k,w\rangle $ of $\varphi [p,q,n]\in A+(B\Cap C)$ , if $i=0$ or $j=0$ then $k=0$ and w is an A-name of $\delta _X(u)$ or $\delta _X(v)$ , so one can compute a name of $[p,q,n]\in (A+B)\Cap (A+C)$ . If $i\not =0$ and $j\not =0$ then w is of the form $\langle \ell ,p_1,q_1,m',z \rangle $ , where if $\ell =0$ then $z\vdash _B\delta _Y(u)$ else $z\vdash _C\delta _Z(v)$ . Thus, if $\ell =0$ then $\langle 1,z\rangle \vdash _{A+B}(1,\delta _Y(u))$ else $\langle 1,z\rangle \vdash _{A+C}(1,\delta _Z(v))$ , so one can compute a name of $[p,q,n]\in (A+B)\Cap (A+C)$ .

For $\leq _{\mathsf {m}}$ , if $i\not =0$ and $j\not =0$ then transform $\alpha =(a,b,c,d)$ into $\alpha '=(a',b',c',d')$ , where $a'=\lambda x.\pi _1(a\ast x)$ , $b'=\lambda x.\pi _1(b\ast x)$ , $c'=\lambda x.c(1,x)$ and $d'=\lambda x.d(1,x)$ . Then define $\varphi ([p,q,\alpha ,n])=\langle 1,[p_1,q_1,\alpha ',n]\rangle $ . The rest of the discussion is the same as above.

Proof. Regular monos are stable under pullback.

Proof. Assume $A\leq _{\mathsf {m}}' B$ via $\varphi ,r_+$ . Given an X-name p of $x\in |A|$ , using a tracker of $\varphi $ , one can find an X-name of $\varphi (x)\in |B|$ . As B is regular, we get a B-name q of $\varphi (x)$ . Then $r_+(p,q)$ is an A-name of x. Thus, A is regular.

Proof of Proposition 3.35

For the non-existence of meet, it is known that every increasing sequence of many-one degrees has an exact pair [Reference Odifreddi5, Theorem VI.3.4]; that is, for any sequence $A_0<_mA_1<_m\dots $ of subsets of $\omega $ there exists $B,C\subseteq \omega $ such that $A\leq _m B,C$ if and only if $A\leq _m A_i$ for some $i\in \omega $ , where $\leq _m$ is many-one reducibility in the classical sense (Definition 3.19). Now note that if $R,S$ are regular subobjects of $\omega $ then $R\leq _{\mathsf {m}}S$ iff $R\leq _{\mathsf {m}}'S$ iff $|R|\leq _m|S|$ . For each $i\in \omega $ , let us think of $A_i,B,C$ as regular subobjects of $\omega $ . We claim that B and C do not have meet. If $A\leq _{\mathsf {m}}' B,C$ then, by Lemma 3.37, A is also regular. Thus, the above property shows $A\leq _{\mathsf {m}}A_i$ for some $i\in \omega $ . Then we get $A<_{\mathsf {m}}A_{i+1}<_{\mathsf {m}}B,C$ , which means that A is not a meet of B and C.

Observation 4.5. An open subobject is regular. Similarly, a closed subobject is regular.

Proof. This is because an open subobject is a pullback of a regular subobject $\top \colon \mathbf {1}\rightarrowtail \mathbb {S}$ . The same applies to a closed subobject. See also the above explicit description of the pullback.

Observation 4.9. Every ${\Pi }^0_2$ subobject of a represented space X is regular.

Proof. Every $\Pi ^0_2$ subobject $A\rightarrowtail X$ is of the form for some open subobject $B\rightarrowtail \omega \times X$ . By Observation 4.5, B is regular, so a name of $(n,x)\in B$ is just the pair of $n\in \omega $ and an X-name of x. By definition, a name of $x\in A$ is a name of a function that, given $n\in \omega $ , returns an name of $(n,x)\in B$ . In particular, if p is a name of $x\in X$ then the constant function $n\mapsto p$ gives a name of $x\in A$ . This means that $A\rightarrowtail X$ is regular.

Observation 5.3. $\mathsf {L}\in \Sigma _{\pi \cup \pi }$ .

Proof. Assume that $A\rightarrowtail X$ is regular. Then the inclusion map $A\rightarrowtail X$ has a partial left-inverse morphism, so let r be its tracker. That is, if q is an X-name of $x\in |A|$ , then $r(q)$ is an A-name of x. Now, suppose that A has a non-regular point $x\in A$ , and let $\ell $ be a length for its non-regularity. For an X-name q of x and an A-name $r(q)$ of x, we get a witness $(y_t)_{t\in \omega }$ for non-regularity. By continuity, after reading some m bits of q, the first $\ell $ bits of $r(q)$ are determined. Then $q\upharpoonright m$ can be extended to an X-name $q'$ of $y_t\in |A|$ , so $r(q')$ must be an A-name of $y_t$ . However, $r(q')$ extends $r(q)\upharpoonright \ell $ , which cannot be an A-name of $y_t$ .

Proof. By Lemma 5.6 and Example 5.5, $\mathsf {L}$ is not regular. However, by Observation 4.9, every ${\Pi }^0_2$ subobject is regular. Hence, $\mathsf {L}$ is not ${\Pi }^0_2$ .

Proof. Let $x\in |\mathsf {Fin}|$ and $(p_1,\dots ,p_n)$ be given. Assume that $p_i$ is a name of $x\in \mathsf {Fin}$ for some $i\leq n$ . As a name of an element of $\mathsf {Fin}$ is of the form $\langle s,z\rangle $ , it does not lose generality to assume that each $p_i$ is of the form $\langle s_i,z_i\rangle $ . By our assumption, at least one of these is a correct name of $x\in \mathsf {Fin}$ , so it is of the form $p_j=\langle s_j,x\rangle $ for some j. Here, recall that $\langle s_j,x\rangle $ is a name of $x\in \mathsf {Fin}$ if and only if $x(t)=0$ for any $t\geq s_j$ . Note that, if we put $m=\max _{i\leq n}s_i$ , then $\langle m,x\rangle $ is also a name of $x\in \mathsf {Fin}$ . This is because we have $s_j\leq m$ , which implies $x(t)=0$ for any $t\geq m$ . In summary, $F(x,p_1,\dots ,p_n)=\langle \max _{i\leq n}\pi _0(p_i),x\rangle $ gives a name of $x\in \mathsf {Fin}$ . Hence, $\mathsf {Fin}$ is amalgamable.

Proof. Assume that $A\leq _{\mathsf {m}}B$ is witnessed by $\varphi \colon X\to Y$ and $r_-,r_+$ . To show that $A\rightarrowtail Z$ is regular, suppose that an X-name p of $x\in |A|$ is given. Since A is almost $\Pi ^0_1$ and any $\Pi ^0_1$ subobject is regular, we may assume that a name of $x\in A$ is of the form $(k,p)$ for some $k<n$ . Then $(r_-(k,p))_{k<n}$ is a sequence of candidates of names of $\varphi (x)\in B$ . That is, since $(k,p)$ is a correct name of $x\in A$ for some $k<n$ , $r_-(k,p)$ must be a correct name of $\varphi (x)\in B$ . Here, note that $r_-(k,p)$ may be undefined, but the condition $x\in |A_k|$ is $\Pi ^0_1(p)$ , so once we see that this is refuted, we modify it to output some value. In this way, we can assume that $r_-(k,p)$ is defined.

A tracker of $\varphi $ transforms an X-name of x into an Y-name of $\varphi (x)$ , which, together with the above candidates, can be used to obtain a correct B-name q of $\varphi (x)$ by the assumption that B is amalgamable. Then, $r_+(p,q)$ is an A-name of $x\in A$ . This concludes that A is regular.

Proof of Theorem 5.8

By Proposition 5.9, $\mathsf {Fin}$ is amalgamable. Obviously, $\mathsf {L}$ is almost $\Pi ^0_1$ . Hence, by Lemma 5.10, if $\mathsf {L}\leq _{\mathsf {m}}\mathsf {Fin}$ then $\mathsf {L}$ is regular, which is impossible by Lemma 5.6 and Example 5.5.

Observation 5.11. For any $\Sigma ^0_2$ subobject $A\rightarrowtail \omega ^\omega $ , we have $A\leq _{\mathsf {m}}'\mathsf {Fin}$ .

Proof. The argument is similar to the classical $\Sigma ^0_2$ -completeness proof of $\mathsf {Fin}$ . Let be given, where $\theta $ is decidable. Given x, we construct $\varphi (x)$ . In order to determine the value of $\varphi (x)(s)$ , we first calculate the largest $n_s\leq s$ fulfilling the following condition: For any $k\leq n_s$ there exists $m\leq s-n_s$ such that $\neg \theta (k,m,x)$ . If $n_s>n_{s-1}$ then put $\varphi (x)(s)=1$ ; otherwise $\varphi (x)(s)=0$ . Note that if $x\in A$ and if n is the least witness for $x\in A$ , then we have $n_s\leq n$ for any s. Hence, for the least s such that $n_s=n$ , the value $s+1$ must be a witness for $\varphi (x)\in \mathsf {Fin}$ . Conversely, if s is a witness for $\varphi (x)\in \mathsf {Fin}$ , then $n_t=n_s$ for any $t\geq s$ . Then it is easy to see that $n_s+1$ is a witness for $x\in A$ .

Observation 5.13. Let $A\rightarrowtail X$ be a $\Sigma ^0_2$ subobject such that for some morphism $f\colon \omega \times X\to 2$ . Then A has the unique witness property.

Proof. Define . Then, $(A_n)_{n\in \omega }$ is a uniform $\Pi ^0_1$ sequence, and $|A_n|\cap |A_m|=\emptyset $ for $n\not =m$ . Clearly, we have $\biguplus _nA_n\subseteq A$ . To see $A\subseteq \biguplus _nA_n$ , if n is a witness for $x\in A$ , then search for the least $n_0\leq n$ such that $f(m,x)=1$ for any $n_0\leq m\leq n$ . By our assumption on n, one can see that $n_0$ is the least witness for $x\in A$ . Therefore, $x\in A_{n_0}$ . As $n\mapsto n_0$ is computable, we have $A\subseteq \biguplus _nA_n$ .

Observation 5.14. A $\Sigma ^0_2$ subobject $A\rightarrowtail X$ has the increasing witness property iff there exists a $\Pi ^0_1$ subobject $P\rightarrowtail \omega \times X$ such that .

Proof. For the forward direction, $x\in A$ iff $x\in A_n$ for some n, and for such n, $x\in A_m$ for any $m\geq n$ . For the backward direction, consider , where $P_m\rightarrowtail X$ is the mth projection of P. Then $(A_n)_{n\in \omega }$ is a uniform $\Pi ^0_1$ sequence, and $|A_n|\subseteq |A_m|$ whenever $n\leq m$ . Note that n is a witness for $x\in A$ iff $x\in A_n$ , so it is also a witness for $x\in \biguplus _{n\in \omega }A_n$ . Thus, $A\equiv \biguplus _{n\in \omega }A_n$ .

Observation 5.15. Let $A\rightarrowtail X$ and $B\rightarrowtail Y$ be ${\Sigma }^0_2$ subobjects such that $A\leq _{\mathsf {m}}B$ .

1. 1. If B has the unique witness property, so does A.

2. 2. If B has the increasing witness property, so does A.

Proof. (1) Assume $B\equiv \biguplus _{n\in \omega }B_n$ . If $A\leq _{\mathsf {m}}B$ via $\varphi $ then we have $A\equiv \varphi ^\ast B$ . Note that $\varphi ^\ast (\biguplus _nB_n)\equiv \biguplus _n\varphi ^\ast B_n$ . Hence, $|B_n|\cap |B_m|=\emptyset $ implies $|\varphi ^\ast B_n|\cap |\varphi ^\ast B_m|=\varphi ^{-1}[|B_n|]\cap \varphi ^{-1}[|B_n|]=\varphi ^{-1}[|B_n|\cap |B_m|]=\emptyset $ . Thus, $\varphi ^\ast (\biguplus _nB_n)$ has the unique witness property. Now, $B\equiv \biguplus _nB_n$ implies $A\equiv \varphi ^\ast B\equiv \varphi ^\ast (\biguplus _nB_n)$ ; hence, A also has the unique witness property.

(2) Note that $|B_n|\subseteq |B_m|$ implies $|\varphi ^\ast B_n|=\varphi ^{-1}[|B_n|]\subseteq \varphi ^{-1}[|B_m|]=|\varphi ^\ast B_m|$ . Thus, by the same argument as above, one can see that A has the increasing witness property.

Proof. Assume $A\equiv \biguplus _{n\in \omega }A_n$ , and consider $A_m'=\biguplus _{k\leq m}A_k$ . Obviously, $m\leq n$ implies $|A_m'|\subseteq |A_n'|$ . One can see $A\equiv \biguplus _{m\in \omega }A_m'$ . This is because, if $(n,p)$ is a name of $x\in \biguplus _{n\in \omega }A_n$ then $(n,n,p)$ is a name of $x\in \biguplus _{m}\biguplus _{k\leq m}A_k$ , and if $(m,k,p)$ is a name of $x\in \biguplus _{m}\biguplus _{k\leq m}A_k$ then $(k,p)$ is a name of $x\in \biguplus _{n\in \omega }A_n$ .

Now note that, in general, even if $A_n$ is ${\Pi }^0_1$ for each n, $A_m'$ is not necessarily ${\Pi }^0_1$ . However, the unique witness property solves this problem. In this case, we claim that $A_m'$ is equivalent to a subspace $B_m$ of X whose underlying set is $|A_m'|$ . Clearly, $A_m'\subseteq B_m$ . Given a name p of $x\in B_m$ , by the unique witness property, there exists a unique $k\leq m$ such that $x\in A_k$ . Now wait for $x\not \in A_n$ to be recognized for all $n\leq m$ except one k. By continuity of trackers of co-characteristic functions of $A_n$ ’s, one can recognize this after reading a finite initial segment on p. Then we must have $x\in A_k$ . Now, as p is an X-name of x, by regularity, one can recover its $A_k$ -name $p_k$ . Then $(k,p_k)$ is a name of $x\in A_m'$ .