d_{\mathbf{X}}(p,x)\geq b_{t}\right\\}.$

We claim that for all $x\in B_{\mathbf{X}}\left(p,1\right)$ the set $A_{x}$ is
inhabited, though not by much. More precisely, we claim that there exists
$u\in\mathbb{N}^{\bullet}$ such that $u\in
A_{x}\subseteq{\mathbb{N}^{\bullet}}_{[\text{pred}(u),\text{succ}(u)]}$.
Define $\alpha$ to be a sequence $\mathbb{N}\to\mathbf{2}$ such that
$\alpha_{n}=1\implies d_{\mathbf{X}}(p,x)<a_{n+1}$ and $\alpha_{n}=0\implies
d_{\mathbf{X}}(p,x)>b_{n}$. Such $\alpha$ exists by countable choice because
$b_{n}<a_{n+1}$. Let $u:=r(\alpha)$ where
$r\colon\mathbf{2}^{\mathbb{N}}\to\mathbb{N}^{\bullet}$ is the standard
retraction. In particular this means that if $u\in\mathbb{N}$, then
$\alpha_{u}$ is the first zero in the sequence $\alpha$.

     * •

$u\in A_{x}$
First we prove $a_{u}\geq d_{\mathbf{X}}(p,x)$. If $u=0$, we are done since
$x\in B_{\mathbf{X}}\left(p,1\right)$. Assume now $u\geq 1$, and
$a_{u}<d_{\mathbf{X}}(p,x)$. This means there exists $n\in\mathbb{N}$ such
that $2^{-n}<d_{\mathbf{X}}(p,x)$. If $n<u$, then $\alpha_{n}=1$, so
$d_{\mathbf{X}}(p,x)<a_{n+1}<d_{\mathbf{X}}(p,y_{n})\leq 2^{-n-1}<2^{-n}$, a
contradiction. If $n\geq u$, then $u\in\mathbb{N}$, and $\alpha_{u}=0$ while
$\alpha_{u-1}=1$ (recall $u\geq 1$), so $d_{\mathbf{X}}(p,x)<a_{u}$ which is a
contradiction also.

Second, assume $d_{\mathbf{X}}(p,x)<b_{u}$. Then $b_{u}>0$, so
$u\in\mathbb{N}$. Consequently $\alpha_{u}=0$, meaning
$d_{\mathbf{X}}(p,x)>b_{u}$, a contradiction.

     * •

$A_{x}\subseteq{\mathbb{N}^{\bullet}}_{[\text{pred}(u),\text{succ}(u)]}$
Take any $t\in A_{x}$; then $a_{t}\geq d_{\mathbf{X}}(p,x)\geq b_{t}$ holds.

Assume $t<\text{pred}(u)$. Then $t\in\mathbb{N}$, and $t+1<u$, so
$\alpha_{t+1}=1$ which means $d_{\mathbf{X}}(p,x)<a_{t+2}<b_{t}$, a
contradiction.

Assume $t>\text{succ}(u)$. Then $u\in\mathbb{N}$, and $u+2\leq t$. We have
$\alpha_{u}=0$ which means $d_{\mathbf{X}}(p,x)>b_{u}>a_{u+2}\geq a_{t}$, a
contradiction.

     * •

$A_{x}$ is subcompact in $\mathbb{N}^{\bullet}$
The set $A_{x}$ is closed in
${\mathbb{N}^{\bullet}}_{[\text{pred}(u),\text{succ}(u)]}$ (because $\geq$ is
a closed relation since $<$ is open) which is in turn subcompact in
$\mathbb{N}^{\bullet}$ by Lemma 5.4.

Consequently $e(A_{x})$ is subcompact in $e(\mathbb{N}^{\bullet})$, so the set

$V:=\left\\{x\in B_{\mathbf{X}}\left(p,1\right)\;\middle|\;e(A_{x})\subseteq
U\right\\}$

is open in $B_{\mathbf{X}}\left(p,1\right)$, therefore also in $X$ (since
$\Sigma$ is a dominance). We prove the theorem once we conclude $V\cap
e(\mathbb{N}^{\bullet})=U$.

     * •

$A_{y_{u}}=\\{u\\}$ for all $u\in\mathbb{N}^{\bullet}$
Since $a_{u}\geq d_{\mathbf{X}}(p,y_{u})\geq b_{u}$, we have $u\in A_{y_{u}}$.
Conversely, take any $t\in A_{y_{u}}$. If $t<u$, then $t\in\mathbb{N}$, and we
obtain a contradiction $d_{\mathbf{X}}(p,y_{u})>a_{t+1}\geq a_{u}\geq
d_{\mathbf{X}}(p,y_{u})$. If $t>u$, we similarly obtain a contradiction
$d_{\mathbf{X}}(p,y_{u})>a_{u+1}\geq a_{t}\geq d_{\mathbf{X}}(p,y_{u})$. Thus
$t=u$.

     * •

$V\cap e(\mathbb{N}^{\bullet})=U$
The claim follows from $e(A_{y_{u}})\subseteq U\iff e(\\{u\\})\subseteq U\iff
y_{u}\in U$.

∎

###### Lemma 5.6

Let $A\subseteq X$, $A^{C}=\emptyset$, and let $\mathbf{X}=(X,d_{\mathbf{X}})$
be a metric space, with $\mathbf{A}=(A,d_{\mathbf{A}})$ its metric subspace.

  1. 1.

If $\mathbf{A}$ is metrized, then so is $\mathbf{X}$.

  2. 2.

If $A$ is compact, then so is $X$.

###### Proof.

  1. 1.

Take any $U\in\mathcal{O}(X)$. Then $U\cap A$ is open in $A$, so under the
assumption that $\mathbf{A}$ is metrized, we can write it as an overtly
indexed union

$U\cap A=\bigcup_{i\in I}B_{\mathbf{A}}\left(a_{i},r_{i}\right)$

where $a_{i}\in A$, $r_{i}\in\mathbb{R}$.

We claim that $U=\bigcup_{i\in I}B_{\mathbf{X}}\left(a_{i},r_{i}\right)$.
Since the sets both on the left and the right are open, and therefore
$\lnot\lnot$-stable, we can just as well prove that their complements match.
But for any $V\in\mathcal{O}(X)$ and $x\in X$ we have

$\lnot(x\in V\land x\in A)\iff\lnot(\lnot\lnot(x\in V)\land\lnot\lnot(x\in
A))\iff\lnot\lnot\lnot(x\in V)\iff\lnot(x\in V),$

so $(V\cap A)^{C}=V^{C}$. Since $U\cap A=\bigcup_{i\in
I}B_{\mathbf{A}}\left(a_{i},r_{i}\right)$ and $\left(\bigcup_{i\in
I}B_{\mathbf{X}}\left(a_{i},r_{i}\right)\right)\cap A=\bigcup_{i\in
I}B_{\mathbf{A}}\left(a_{i},r_{i}\right)$, the result follows.

  2. 2.

If $A$ is compact, it is subcompact in $X$, so by Lemma 5.3 ${A^{C}}^{C}=X$ is
subcompact in $X$, i.e. $X$ is compact.

∎

###### Theorem 5.7

Let $\mathbf{X}=(X,d)$ be a metric space with a metrically dense subovert
subset (e.g. a metrically separable space).

  1. 1.

If $\mathbf{X}$ has an accumulation point, then it is neither metrized nor
compact.

  2. 2.

Say that $\mathbf{X}$ is _locally semilocated_ when for every $x\in X$ there
exists $r\in\mathbb{R}_{>0}$ such that the distance $d\big{(}\left\\{y\in
X\;\middle|\;0<d(x,y)<r\right\\},x\big{)}$ is an extended real number. The
following are equivalent.

     * •

$\mathbf{X}$ is metrized and locally semilocated.

     * •

The metric $d$ is equivalent to the discrete metric.

In particular, if either (and therefore both) of these conditions holds, then
$X$ has decidable equality.

###### Proof.

  1. 1.

Let $p\in X$ be an accumulation point in $\mathbf{X}$, and
$\widehat{\mathbf{X}}$ the completion of $\mathbf{X}$ (we identify
$\mathbf{X}$ with a metric subspace of $\widehat{\mathbf{X}}$). By Theorem 5.5
there exist suitable sequences $a,b,y$ which induce an injective nonexpansive
map $e\colon\mathbb{N}^{\bullet}\to\widehat{\mathbf{X}}$ with a strongly
closed image. Let $X^{\prime}:=X\cup e(\mathbb{N}^{\bullet})$, and
$\mathbf{X^{\prime}}$ the metric subspace in $\widehat{\mathbf{X}}$ with the
underlying set $X^{\prime}$. By Theorem 5.5(2) the image of $e$ is strongly
closed also in $X^{\prime}$. If $\mathbf{X}$ is metrized/compact, then so is
$\mathbf{X^{\prime}}$ by Lemma 5.6 which implies that
$e(\mathbb{N}^{\bullet})$ is metrized/compact by Theorem 4.38. Since $e$ is
bijective onto its image, compactness of $e(\mathbb{N}^{\bullet})$ implies
compactness of $\mathbb{N}^{\bullet}$, and since $e$ is furthermore
nonexpansive, metrization of $e(\mathbb{N}^{\bullet})$ implies metrization of
$\mathbb{N}^{\bullet}$ by Lemma 4.33. Contradiction.

  2. 2.

Notice that $d$ is equivalent to the discrete metric if and only if for every
$x\in X$ there exists $\epsilon\in\mathbb{R}_{>0}$ such that
$B\left(x,\epsilon\right)=\\{x\\}$, or equivalently, $\left\\{y\in
X\;\middle|\;0<d(x,y)<\epsilon\right\\}=\emptyset$.

     * •

$(\Rightarrow)$
Take any $x\in X$, and let $r\in\mathbb{R}_{>0}$ witness local semilocatedness
around $x$. Let $A:=\left\\{y\in X\;\middle|\;0<d(x,y)<r\right\\}$, and define
$\epsilon:=\inf\\{d(A,x),r\\}$; then $\epsilon$ is a nonnegative real number.
Since $d(A,x)$ is the strict infimum, if $d(A,x)=0$, then $x$ is an
accumulation point, and $\mathbf{X}$ could not be metrized. Thus (by Markov
principle) $d(A,x)>0$, so $\epsilon>0$. If there is $y\in X$,
$0<d(x,y)<\epsilon$, then $y\in A$, therefore $d(x,y)\geq\epsilon$, a
contradiction, so this $\epsilon$ works.

     * •

$(\Leftarrow)$
Suppose for every $x\in X$ there is $\epsilon\in\mathbb{R}_{>0}$ such that
$B\left(x,\epsilon\right)=\\{x\\}$. Then $r:=\epsilon$ witnesses local
semilocatedness of $x$ (namely, $A:=\left\\{y\in
X\;\middle|\;0<d(x,y)<r\right\\}$ is empty, so $d_{\mathbf{X}}(A,x)=\infty$).
Moreover, we see that the only metrically dense subset of $X$ is $X$ itself,
so $X$ is overt, and for any $y\in X$,

$\top\iff 0<d(x,y)\lor d(x,y)<\epsilon\implies x\neq y\lor x=y,$

so $X$ has decidable equality. Thus $X$ is metrized by the discrete metric (by
Proposition 4.3), therefore also by $d$ since it is equivalent to it.

∎

The conclusion is that in Russian constructivism most interesting metric
spaces are not metrized. Granted, we considered only the case
$\Sigma=\Sigma^{0}_{1}$ (the smallest $\Sigma$ for which $\mathbb{N}$ is
overt), but if a space is not metrized with respect to $\Sigma^{0}_{1}$, then
it is not metrized with respect to any larger $\Sigma$. This suggests that
Type I computability is not an optimal choice for computation with metric
spaces.

###  5.3 Function Realizability or Brouwer’s Intuitionism

In this section we consider a slightly strengthened version of Brouwer’s
intuitionism. We adopt the following principles:

  1. 1.

_Function-Function Choice_
$\text{{AC}}(\mathbb{N}^{\mathbb{N}},\mathbb{N}^{\mathbb{N}})$,

  2. 2.

_Continuity Principle_ : for every
$f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ and
$\alpha\in\mathbb{N}^{\mathbb{N}}$ there exists $k\in\mathbb{N}$ such that
$\beta\in B_{C}\left(\alpha,2^{-k}\right)$ implies $f(\alpha)=f(\beta)$ (in
short: every $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ is
$\epsilon$-$\delta$-continuous),

  3. 3.

_Fan Principle_ : every decidable bar is uniform, cf. Section 4.1.

In the usual setting INT [7, 5.2] only the weaker _Function-Number Choice_
$\text{{AC}}(\mathbb{N}^{\mathbb{N}},\mathbb{N})$ is used. Kleene’s function
realizability and the corresponding realizability topos validate not only
Function-Function Choice but even _Function Choice_
$\text{{AC}}(\mathbb{N}^{\mathbb{N}})$. In Type II effectivity Function Choice
manifests itself as the fact that $\mathbb{N}^{\mathbb{N}}$ has an admissible
injective representation.

We show that $\Sigma=\Sigma^{0}_{1}$, Function-Function Choice, and Continuity
Principle together imply that the Baire space $\mathbb{B}$ is metrized. It
then follows from Theorem 4.36 that all CMSs are metrized, and from the Fan
Principle and Corollary 4.24 that the Cantor space $\mathbb{C}$, and more
generally any CTB, is compact.

We start by proving that $\mathbb{B}$ is weakly metrized, i.e. that every open
subset $U\subseteq\mathbb{N}^{\mathbb{N}}$ is a union of balls. Because the
map $q\colon\mathbf{2}^{\mathbb{N}}\to\Sigma$,
$q(\alpha):=(\exists\,n\,{\in}\,\mathbb{N}\,.\,\alpha_{n}=0)$ is surjective,
by Function-Function Choice there exists a map
$f\colon\mathbb{N}^{\mathbb{N}}\to\mathbf{2}^{\mathbb{N}}$ such that

$U=\left\\{\alpha\in\mathbb{B}\;\middle|\;\exists\,n\,{\in}\,\mathbb{N}\,.\,f(\alpha)(n)=0\right\\}.$

By Continuity Principle and Function-Number Choice there exists a modulus of
continuity $\mu\colon\mathbb{N}^{\mathbb{N}}\times\mathbb{N}\to\mathbb{N}$
such that for every $\alpha\in\mathbb{N}^{\mathbb{N}}$, $\beta\in
B(\alpha,2^{-\mu(\alpha,n)})$ implies $f(\alpha)(n)=f(\beta)(n)$. Define

$I:=\left\\{(\alpha,n)\in\mathbb{N}^{\mathbb{N}}\times\mathbb{N}\;\middle|\;f(\alpha)(n)=0\right\\},$

and observe that

$U=\bigcup_{(\alpha,n)\in I}B\left(\alpha,2^{-\mu(\alpha,n)}\right).$

We now know that open subsets are unions of open balls, therefore
$\mathbb{N}^{\mathbb{N}}$ is overt by Proposition 4.2. Consequently, $I$ is
overt as well. We proved that $\mathbb{B}$ is metrized.

We see that metric spaces are far better behaved in Type II effectivity than
Type I effectivity, suggesting that the former is better for modeling metric
spaces than the latter.

On a side note, one may wonder if Continuity Principle alone implies that CMSs
are metrized for the case $\Sigma=\Sigma^{0}_{1}$. This would make metrization
of CMSs equivalent to the Continuity Principle since the former implies the
latter by Theorem 4.58(6). However, in Russian constructivism the Continuity
Principle is validated by the Kreisel-Lacombe-Shoenfield-Ceitin theorem [33,
9, 8], but the CMSs are generally not metrized, as we showed in Section 5.2.

###  5.4 Gros Topos

In this section we review the notions of presheaves, sheaves and gros topos
[24, 41], and consider synthetic topological properties in gros topos.

Let $\mathfrak{T}$ denote a small full subcategory of
$\mathbf{\underline{Top}}$ with the property that for any space $X$ in
$\mathfrak{T}$ all its open subsets (and consequently their open embeddings)
are in $\mathfrak{T}$. It is not strictly necessary to assume that
$\mathfrak{T}$ has finite products, but it is very convenient, and we shall do
so. _Presheaves_ on $\mathfrak{T}$ are (contravariant) functors
$\mathfrak{T}^{\mathrm{op}}\to\mathbf{\underline{Set}}$; they form the functor
category $\mathbf{\underline{Set}}^{\mathfrak{T}^{\mathrm{op}}}$ with natural
transformations as morphisms. The Yoneda functor
$\mathsf{y}{}\colon\mathfrak{T}\to\mathbf{\underline{Set}}^{\mathfrak{T}^{\mathrm{op}}}$,
given by $\mathsf{y}{X}=\mathscr{C}(\text{---},X)$ and
$(\mathsf{y}{f})_{Z}=\mathscr{C}(Z,f)=f\circ\text{---}$, is a categorical
embedding (a full and faithful functor, injective on objects) of
$\mathfrak{T}$ into the category of presheaves.

Presheaves form a topos. The limits are computed pointwise (for example
$(F\times G)(X)=F(X)\times G(X)$, and the terminal object is the constant
functor $\mathbf{1}$), and exponentials are given as
$G^{F}(X)=\text{Nat}(\mathsf{y}{X}\times F,G)$ (where $\text{Nat}(F,G)$
denotes the set of natural transformations between functors $F$ and $G$) with
the evaluation map $\epsilon\colon G^{F}\times F\to G$,
$\epsilon_{X}(\eta,x)=\eta_{X}(\textrm{Id}_{X},x)$. The Yoneda functor
preserves limits and exponentials that exist in $\mathfrak{T}$.

In any category a morphism $f\colon X\to Y$ is a monomorphism if and only if
the diagram

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\textrm{Id}_{X}}$$\scriptstyle{\textrm{Id}_{X}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{Y}$

is a pullback. The consequence for our case is that the Yoneda embedding
$\mathsf{y}{}$ preserves monos, and that a natural transformation between
presheaves is a mono in
$\mathbf{\underline{Set}}^{\mathfrak{T}^{\mathrm{op}}}$ if and only if its
every component is an injective map (a mono in $\mathbf{\underline{Set}}$).

A _sieve_ $\mathcal{S}\subseteq\text{cod}^{-1}(X)$ on a space $X$ in
$\mathfrak{T}$ is a set of maps in $\mathfrak{T}$ with the codomain $X$ such
that if $f\colon B\to X$ is in $\mathcal{S}$ and $g\colon A\to B$ is any map
in $\mathfrak{T}$, then $f\circ g\colon A\to X$ is also in the sieve
$\mathcal{S}$. The subobject classifier in
$\mathbf{\underline{Set}}^{\mathfrak{T}^{\mathrm{op}}}$ is given as

$\Omega(X)=\text{ the set of all sieves on $X$}$

while for $f\colon X\to Y$ in $\mathfrak{T}$ and a sieve
$\mathcal{S}\in\Omega(Y)$

$\Omega(f)(\mathcal{S})=\left\\{g\in\text{cod}^{-1}(X)\;\middle|\;f\circ
g\in\mathcal{S}\right\\}.$

The truth map $\top\colon\mathbf{1}\to\Omega$ picks at each component $X$ the
_maximal sieve_ $\text{cod}^{-1}(X)$ on $X$, i.e. the set of all maps in
$\mathfrak{T}$ with the codomain $X$. Given any monomorphism $\iota\colon F\to
G$, the corresponding characteristic map $\chi^{\iota}\colon G\to\Omega$ at
component $X$ is

$\chi^{\iota}_{X}(x)=\left\\{f\in\text{cod}^{-1}(X)\;\middle|\;\exists\,a\,{\in}\,F(\text{dom}(f))\,.\left(G(f)(x)=\iota_{\text{dom}(f)}(a)\right)\right\\},$

i.e. the sieve of all maps $f\colon A\to X$ in $\mathfrak{T}$ for which
$G(f)(x)$ is in the image of $\iota_{A}$.

$\textstyle{a\in
F(A)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{A}}$$\textstyle{F(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\phantom{\owns
x}}$$\scriptstyle{F(f)}$$\scriptstyle{\iota_{X}}$$\textstyle{{}\phantom{a\in}G(A)}$$\textstyle{G(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\owns
x}$$\scriptstyle{G(f)}$

A presheaf $F\colon\mathfrak{T}^{\mathrm{op}}\to\mathbf{\underline{Set}}$ is a
_sheaf_ on $\mathfrak{T}$ when for every $X$ in $\mathfrak{T}$, every open
cover $\\{U_{i}\\}_{i\in I}$ of $X$ and every family of elements $\\{f_{i}\in
F(U_{i})\\}_{i\in I}$ satisfying the _gluing condition_

$F(U_{i}\cap U_{j}\hookrightarrow U_{i})(f_{i})=F(U_{i}\cap
U_{j}\hookrightarrow U_{j})(f_{j})\qquad\text{for all $i,j\in I$}$

there exists a unique element $f\in F(X)$ with the property that
$F(U_{i}\hookrightarrow X)(f)=f_{i}$ for all $i\in I$.

Let $\mathsf{Sh}(\mathfrak{T})$ denote the full subcategory of sheaves in
$\mathbf{\underline{Set}}^{\mathfrak{T}^{\mathrm{op}}}$. For any topological
space $X$ the functor $\mathscr{C}(\text{---},X)$ is a sheaf; in particular,
the Yoneda embedding restricts to
$\mathsf{y}{}\colon\mathfrak{T}\to\mathsf{Sh}(\mathfrak{T})$. Limits (but not
colimits) and exponentials in $\mathsf{Sh}(\mathfrak{T})$ are computed the
same as in $\mathbf{\underline{Set}}^{\mathfrak{T}^{\mathrm{op}}}$, so
$\mathsf{y}{}$ still preserves them.

A _closed sieve_ on $X$ is a sieve on $X$ with the additional property that
for every space $A$ in $\mathfrak{T}$, every open cover $\\{U_{i}\\}_{i\in I}$
of $A$, and every family of maps $\\{f_{i}\colon U_{i}\to X\\}_{i\in I}$ in
the sieve which satisfy the gluing condition that $f_{i}$ and $f_{j}$ restrict
to the same map on $U_{i}\cap U_{j}$ for all $i,j\in I$, the unique map
$f\colon A\to X$ with the property that restricted to $U_{i}$ is $f_{i}$ for
all $i\in I$, is also in the sieve333This has nothing to do with closedness in
the sense of synthetic topology; it is the established terminology, in the
sense that a sieve is closed for the operation of gluing maps together.. The
subobject classifier in $\mathsf{Sh}(\mathfrak{T})$ is given as
$\Omega(X)=\text{ the set of closed sieves on $X$}$. The morphism part of
$\Omega$, the truth map and the characteristic maps are the same as in
$\mathbf{\underline{Set}}^{\mathfrak{T}^{\mathrm{op}}}$. The category
$\mathsf{Sh}(\mathfrak{T})$ is called _gros topos_ (over $\mathfrak{T}$).

While $\top$ is represented as the maximal sieve at each component, $\bot$ is
represented as the minimal closed sieve; at component $X$, this is the sieve
which contains only the map $\emptyset\hookrightarrow X$ (which every closed
sieve must contain since $\emptyset$ is covered by an empty family of open
subsets)444This differs from the situation in presheaves where the minimal
sieve is the empty one.. One may calculate that the negation
$\lnot\colon\Omega\to\Omega$ maps a closed sieve $\mathcal{S}\in\Omega(X)$ to
the closed sieve of all maps in $\mathfrak{T}$ with codomain $X$ which have
the image disjoint from all maps in $\mathcal{S}$, i.e. which map into the
complement of the union of images of maps in $\mathcal{S}$. This means that
sieves in the image of $\lnot$ are of the form “all maps with the image in a
certain subspace”, and so can be identified with the subspaces themselves, or
alternatively, the subsets of the underlying set of a topological space. Thus,
the $\lnot\lnot$-stable truth values can be represented as

${\Omega}_{\lnot\lnot}(X)=\mathcal{P}(X)\text{ = the power set of the
underlying set of the space $X$},$ ${\Omega}_{\lnot\lnot}(f)=f^{-1},$

while the inclusion ${\Omega}_{\lnot\lnot}\hookrightarrow\Omega$ maps a subset
to the closed sieve of all maps with the image in that subset.

The natural choice of $\Sigma=\mathrm{T}$ in the sheaf topos is to assign the
set of all open subsets (the topology) to each space:

$\Sigma(X)=\mathcal{O}(X),\qquad\Sigma(f)=f^{-1},$

and $\Sigma$ is embedded into $\Omega$ the same way as ${\Omega}_{\lnot\lnot}$
is, so it factors through the inclusion
$\Sigma\hookrightarrow{\Omega}_{\lnot\lnot}$ which just embeds the topologies
into the power sets. Hence $\Sigma\subseteq{\Omega}_{\lnot\lnot}$ in gros
topos.

To argue that this is a reasonable choice of topology we note that the Yoneda
embedding $\mathsf{y}{}$ “preserves topologies”. Recall that Yoneda lemma (in
contravariant form) states (in our case) that for every topological space
$X\in\text{Obj}(\mathfrak{T})$ and a (pre)sheaf $F$ we have
$\text{Nat}(\mathsf{y}{X},F)\cong F(X)$. Thus the set of global elements of a
(pre)sheaf $F$ is $F(\mathbf{1})$ (since
$F(\mathbf{1})\cong\text{Nat}(\mathsf{y}{\mathbf{1}},F)$, and
$\mathsf{y}{\mathbf{1}}$ is the terminal (pre)sheaf). Then by Lemma 5.8 below
the set of global elements of the intrinsic topology of $\mathsf{y}{X}$ is
precisely the topology of $X$,

$\Sigma^{(\mathsf{y}{X})}(\mathbf{1})\cong\mathcal{O}(\mathbf{1}\times
X)\cong\mathcal{O}(X).$

Consider now the Heyting lattice operations. The negation, restricted to
${\Omega}_{\lnot\lnot}$, is just the complementation at each component. The
conjunction on ${\Omega}_{\lnot\lnot}$ is the intersection; the same on
$\Sigma$ when finite. Because in $\mathsf{Sh}(\mathfrak{T})$ we restrict to
closed sieves, the disjunction on $\Sigma$ (but not in general on
${\Omega}_{\lnot\lnot}$) is the union.555That does not mean that $\Sigma$ has
all (internal) disjunctions, though it has all external (i.e. set-indexed)
ones. However, in the case of finite disjunctions, internal and external view
amount to the same thing. In particular, $\Sigma$ is a bounded sublattice of
$\Omega$.

Altogether, we may apply Theorem 2.53. From it it is obvious that closed truth
values are the subfunctor of $\Omega$ as follows:

$\mathrm{Z}(X)=\Big{\\{}\mathcal{S}\in\Omega(X)\;\Big{|}\;\bigcup_{f\in\mathcal{S}}\text{im}(f)\in\mathcal{Z}(X)\Big{\\}}$

(in words, $\mathrm{Z}(X)$ is the set of all closed sieves $\mathcal{S}$ such
that the union of images of maps in $\mathcal{S}$ is a closed subset of $X$)
while the morphism part of $\mathrm{Z}$ is the same as for $\Omega$. Also, the
$\lnot\lnot$-stable closed truth values can be expressed as the subfunctor of
${\Omega}_{\lnot\lnot}$,

${\mathrm{Z}}_{\lnot\lnot}(X)=\mathcal{Z}(X)\text{ = the set of all closed
subsets of $X$}$

with the morphism part being the same as for ${\Omega}_{\lnot\lnot}$. Finally,
the decidable truth values are

$\mathbf{2}(X)=\mathcal{O}(X)\cap\mathcal{Z}(X)=\text{the set of clopen
subsets of $X$}.$

Note that functors $\mathrm{T}=\Sigma$, ${\Omega}_{\lnot\lnot}$,
${\mathrm{Z}}_{\lnot\lnot}$ and $\mathbf{2}$ can be equivalently represented
as continuous maps into familiar spaces — recall Section 2.1. The functor
${\Omega}_{\lnot\lnot}$ is isomorphic to $\mathscr{C}(\text{---},\mathbf{T})$,
the functor $\Sigma$ to $\mathscr{C}(\text{---},\mathbf{S})$, the functor
${\mathrm{Z}}_{\lnot\lnot}$ to $\mathscr{C}(\text{---},\tilde{\mathbf{S}})$,
and $\mathbf{2}$ to $\mathscr{C}(\text{---},\mathbf{2})$; in all cases, the
isomorphism takes a subset to its characteristic map (mapping the elements of
the subset to $1$ and the others to $0$). Thus if
$\mathbf{S}\in\text{Obj}(\mathfrak{T})$, then
$\Sigma\cong\mathsf{y}{\mathbf{S}}$.

We also remark that powers of these functors simplify when the exponent is
representable.

###### Lemma 5.8

For $X,Z\in\text{Obj}(\mathfrak{T})$ we have

${\Omega}_{\lnot\lnot}^{\mathsf{y}{X}}(Z)\cong\mathcal{P}(Z\times
X),\qquad\Sigma^{\mathsf{y}{X}}(Z)\cong\mathcal{O}(Z\times
X),\qquad{\mathrm{Z}}_{\lnot\lnot}^{\mathsf{y}{X}}(Z)\cong\mathcal{Z}(Z\times
X).$

###### Proof.

Let $F$ be one of ${\Omega}_{\lnot\lnot}$, $\Sigma$ or
${\mathrm{Z}}_{\lnot\lnot}$. The result follows from the calculation

$F^{(\mathsf{y}{X})}(Z)\cong\text{Nat}(\mathsf{y}{Z}\times\mathsf{y}{X},F)\cong\text{Nat}\big{(}\mathsf{y}{(Z\times
X)},F\big{)}\cong F(Z\times X),$

using Yoneda lemma for the last isomorphism. ∎

It is known that $\Sigma$ is a dominance. The proof is basically the same as
the proof that stable closed subsets are subspaces which we present here, as
we will need it later.

###### Proposition 5.9

Stable closedness is a transitive relation in $\mathsf{Sh}(\mathfrak{T})$
(stable closed subobjects of stable closed subobjects are stable closed).

###### Proof.

Let $\iota\colon F\to G$ and $\kappa\colon G\to H$ be monomorphisms in
$\mathsf{Sh}(\mathfrak{T})$, classified by ${\mathrm{Z}}_{\lnot\lnot}$. We
must prove that their composition is classified by ${\mathrm{Z}}_{\lnot\lnot}$
as well.

Take any $Z\in\text{Obj}(\mathfrak{T})$ and any $c\in H(Z)$. Since
$\chi^{\kappa}$ maps into ${\mathrm{Z}}_{\lnot\lnot}$, there exists a closed
subset $Y\subseteq Z$ such that the sieve $\chi^{\kappa}_{Z}(c)$ consists of
maps which factor through $Y\hookrightarrow Z$. In particular the inclusion
$Y\hookrightarrow Z$ is in the sieve as well, so there exists $b\in G(Y)$ such
that $\kappa_{Y}(b)=H(Y\hookrightarrow Z)(c)$.

Again, since $\chi^{\iota}$ maps into ${\mathrm{Z}}_{\lnot\lnot}$, there
exists a closed subset $X\subseteq Y$ such that the sieve
$\chi^{\iota}_{Y}(b)$ consists of maps which factor through $X\hookrightarrow
Y$, so $(X\hookrightarrow Y)\in\chi^{\iota}_{Y}(b)$, and there exists $a\in
F(X)$ such that $\iota_{X}(a)=G(X\hookrightarrow Y)(b)$.

$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\owns}$$\textstyle{F(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{X}}$$\textstyle{F(Y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F(X\hookrightarrow
Y)}$$\scriptstyle{\iota_{Y}}$$\textstyle{F(Z)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F(Y\hookrightarrow
Z)}$$\scriptstyle{\iota_{Z}}$$\textstyle{\iota_{X}(a)=G(X\hookrightarrow
Y)(b)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\owns}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\in}$$\textstyle{\mathrm{Z}(Y)}$$\textstyle{G(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\kappa_{X}}$$\textstyle{G(Y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{G(X\hookrightarrow
Y)}$$\scriptstyle{\kappa_{Y}}$$\scriptstyle{\chi^{\iota}_{Y}}$$\textstyle{G(Z)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{G(Y\hookrightarrow
Z)}$$\scriptstyle{\kappa_{Z}}$$\textstyle{\kappa_{Y}(b)=H(Y\hookrightarrow
Z)(c)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\in}$$\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\in}$$\textstyle{H(X)}$$\textstyle{H(Y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H(X\hookrightarrow
Y)}$$\textstyle{H(Z)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H(Y\hookrightarrow
Z)}$$\scriptstyle{\chi^{\kappa}_{Z}}$$\textstyle{{\mathrm{Z}}_{\lnot\lnot}(Z)}$

We claim that $\chi^{\kappa\circ\iota}_{Z}(c)$ consists precisely of maps
which factor through $X\hookrightarrow Z$. For one direction it is sufficient
to verify that $(X\hookrightarrow Z)\in\chi^{\kappa\circ\iota}_{Z}(c)$. This
holds because

$\kappa_{X}\circ\iota_{X}(a)=\kappa_{X}\circ G(X\hookrightarrow
Y)(b)=H(X\hookrightarrow Y)\circ\kappa_{Y}(b)=$ $=H(X\hookrightarrow Y)\circ
H(Y\hookrightarrow Z)(c)=H\big{(}(Y\hookrightarrow Z)\circ(X\hookrightarrow
Y)\big{)}=H(X\hookrightarrow Z)(c).$

Conversely, take any map $f\colon A\to Z$ in $\chi^{\kappa\circ\iota}_{Z}(c)$,
i.e. there exists $o\in F(A)$ such that $H(f)(c)=\kappa_{A}\circ\iota_{A}(o)$.
In particular $H(f)(c)$ is in the image of $\kappa_{A}$ which means that the
restriction $\left.{f}\right|^{Y}\colon A\to Y$ exists (i.e. the image of $f$
is contained in $Y$). We have

$\kappa_{A}\circ
G(\left.{f}\right|^{Y})(b)=H(\left.{f}\right|^{Y})\circ\kappa_{Y}(b)=H(\left.{f}\right|^{Y})\circ
H(Y\hookrightarrow Z)(c)=$ $=H\big{(}(Y\hookrightarrow
Z)\circ\left.{f}\right|^{Y}\big{)}(c)=H(f)(c)=\kappa_{A}\circ\iota_{A}(o),$

and since $\kappa_{A}$ is injective,
$G(\left.{f}\right|^{Y})(b)=\iota_{A}(o)$. Thus
$\left.{f}\right|^{Y}\in\chi^{\iota}_{Y}(b)$, so the image of
$\left.{f}\right|^{Y}$, and therefore also the image of $f$, is contained in
$X$.

The statement of the proposition now follows from transitivity of closedness
in classical topology: since $X$ is closed in $Y$ which is closed in $Z$, $X$
is also closed in $Z$. ∎

###### Corollary 5.10

Stable closed subobjects in $\mathsf{Sh}(\mathfrak{T})$ are subspaces.

###### Proof.

By Proposition 5.9 and Theorem 2.53. ∎

However, in general not all closed subobjects are subspaces in
$\mathsf{Sh}(\mathfrak{T})$, i.e. $\mathrm{Z}$ need not be a codominance. One
can see this already on representable objects: the open subobjects of
$\mathsf{y}{X}$ are given by open embeddings into $X$ while closed subobjects
are given by continuous injective maps into $X$ with closed image which are
not necessarily (closed) embeddings.

Our next task is to show that Yoneda embedding preserves overtness and
compactness.

###### Lemma 5.11

Let $X$ be a topological space from $\mathfrak{T}$. The quantifiers
$\exists^{\mathsf{y}{X}},\forall^{\mathsf{y}{X}}\colon\Omega^{\mathsf{y}{X}}\to\Omega$
of the representable object $\mathsf{y}{X}$ restrict to
$\exists^{\mathsf{y}{X}},\forall^{\mathsf{y}{X}}\colon\Sigma^{\mathsf{y}{X}}\to{\Omega}_{\lnot\lnot}$,
given (in view of Lemma 5.8) as
$\exists^{\mathsf{y}{X}}_{Z},\forall^{\mathsf{y}{X}}_{Z}\colon\mathcal{O}(Z\times
X)\to\mathcal{P}(Z)$,

$\exists^{\mathsf{y}{X}}_{Z}(U)=\left\\{z\in
Z\;\middle|\;\exists\,x\,{\in}\,X\,.\,(z,x)\in U\right\\}=p(U)$

and

$\forall^{\mathsf{y}{X}}_{Z}(U)=\left\\{z\in
Z\;\middle|\;\forall\,x\,{\in}\,X\,.\,(z,x)\in U\right\\}=p(U^{C})^{C}$

where $U\in\mathcal{O}(Z\times X)$ and $p\colon Z\times X\to Z$ is the
projection.

###### Proof.

Recall the construction of the quantifiers in a topos from Section 1.2.

We start with the existential quantifier. An exercise in using Yoneda lemma
shows that the evaluation map
$\epsilon\colon{\Omega}_{\lnot\lnot}^{\mathsf{y}{X}}\times\mathsf{y}{X}\to{\Omega}_{\lnot\lnot}$
is given by

$\epsilon_{Z}\colon\mathcal{P}(Z\times
X)\times\mathscr{C}(Z,X)\to\mathcal{P}(Z),$ $\epsilon_{Z}(A,f)=\left\\{z\in
Z\;\middle|\;(z,f(z))\in A\right\\}=(\textrm{Id}_{Z},f)^{-1}(A).$

Thus the pullback of the truth map along $\epsilon$ at component $Z$ equals

$\left\\{(A,f)\in\mathcal{P}(Z\times
X)\times\mathscr{C}(Z,X)\;\middle|\;(\textrm{Id}_{Z},f)^{-1}(A)=Z\right\\}.$

We skip the calculation what the image of its projection onto
${\Omega}_{\lnot\lnot}^{\mathsf{y}{X}}$ is by recalling how internal
statements in $\mathsf{Sh}(\mathfrak{T})$ are interpreted externally [41],
obtaining

$\left\\{A\in\mathcal{P}(Z\times X)\;\middle|\;\exists(U_{i})_{i\in I}\text{
an open cover of
}Z.\forall\,i\,{\in}\,I\,.\,\exists\,f_{i}\,{\in}\,\mathscr{C}(U_{i},X)\,.\,\text{im}{(\textrm{Id}_{U_{i}},f_{i})}\subseteq
A\right\\}.$

The (restriction of) the existential quantifier is the characteristic map
$\chi\colon{\Omega}_{\lnot\lnot}^{\mathsf{y}{X}}\to\Omega$ of the inclusion of
this set,

$\chi_{Z}\colon\mathcal{P}(Z\times X)\to\Omega(Z),$
$\chi_{Z}(A)=\big{\\{}f\in\text{cod}^{-1}(Z)\,\big{|}\,\exists(U_{i})_{i\in
I}\text{ an open cover of }\text{dom}(f).\\\
\forall\,i\,{\in}\,I\,.\,\exists\,g_{i}\,{\in}\,\mathscr{C}\big{(}U_{i},X\big{)}\,.\,\text{im}{(\textrm{Id}_{U_{i}},g_{i})}\subseteq(f\times\textrm{Id}_{X})^{-1}(U)\big{\\}}=$
$=\left\\{f\in\text{cod}^{-1}(Z)\;\middle|\;\exists(U_{i})_{i\in I}\text{ an
open cover of
}\text{dom}(f).\forall\,i\,{\in}\,I\,.\,\exists\,g_{i}\,{\in}\,\mathscr{C}\big{(}U_{i},X\big{)}\,.\,\text{im}{(\left.{f}\right|_{U_{i}},g_{i})}\subseteq
U\right\\}.$

We prove that $\chi$ factors through ${\Omega}_{\lnot\lnot}$, and is given by
the map $\mathcal{P}(Z\times X)\to\mathcal{P}(Z)$, $U\mapsto p(U)$. Clearly if
$f$ is in the sieve above, its image is contained in $p(U)$. To prove the
converse, it is sufficient to verify that the inclusion $p(U)\hookrightarrow
Z$ is in the sieve. For any $x\in X$ let $e_{x}\colon p(U)\to Z\times X$ be
the map $e_{x}(z):=(z,x)$. Then $\left\\{e_{x}^{-1}(U)\;\middle|\;x\in
X\right\\}$ is an open cover of $p(U)$, and for every $x\in X$ the constant
map $g_{x}(a):=x$ is such that $\text{im}{(e_{x}^{-1}(U)\hookrightarrow
Z,g_{x})}\subseteq U$.

The universal quantifier is simpler. The transpose of the map
$\mathsf{y}{\mathbf{1}}\times\mathsf{y}{X}\to\mathsf{y}{\mathbf{1}}\stackrel{{\scriptstyle\top}}{{\longrightarrow}}\Sigma$
is the map $\mathsf{y}{\mathbf{1}}\to\Sigma^{\mathsf{y}{X}}$, given at
component $Z$ as

$\mathbf{1}\to\mathcal{O}(Z\times X),\qquad*\mapsto Z\times X.$

Thus its characteristic map $\chi\colon\Sigma^{\mathsf{y}{X}}\to\Omega$ at $Z$
is

$\chi_{Z}\colon\mathcal{O}(Z\times X)\to\Omega(Z),$
$\chi_{Z}(U)=\left\\{f\in\text{cod}^{-1}(Z)\;\middle|\;(f\times\textrm{Id}_{X})^{-1}(U)=\text{cod}(f)\times
X\right\\}=$
$=\left\\{f\in\text{cod}^{-1}(Z)\;\middle|\;\text{im}(f\times\textrm{Id}_{X})\subseteq
U\right\\}=\left\\{f\in\text{cod}^{-1}(Z)\;\middle|\;\text{im}(f)\times
X\subseteq U\right\\}.$

From here the result easily follows. ∎

###### Proposition 5.12

  1. 1.

All representable objects are overt in $\mathsf{Sh}(\mathfrak{T})$.

  2. 2.

If $X\in\text{Obj}(\mathfrak{T})$ is a compact topological space, then
$\mathsf{y}{X}$ is a compact object in $\mathsf{Sh}(\mathfrak{T})$.

###### Proof.

  1. 1.

By Lemma 5.11 the existential quantifier at a component $Z$ restricts to
$\mathcal{O}(Z\times X)\to\mathcal{P}(Z)$, and is given by $U\mapsto p(U)$. We
need to see that it further restricts to $\mathcal{O}(Z\times
X)\to\mathcal{O}(Z)$, but this is true since classically all projections are
open maps.

  2. 2.

By Lemma 5.11 the universal quantifier at a component $Z$ restricts to
$\mathcal{O}(Z\times X)\to\mathcal{P}(Z)$, given by $U\mapsto p(U^{C})^{C}$.
If $X$ is compact, then projections along it are closed maps by Theorem 2.2,
so $p(U^{C})^{C}$ is open.

∎

We note however, that representable objects can be compact even if they are
not represented by a compact topological space. This is because we “test
compactness just on spaces in $\mathfrak{T}$”. For example, if $\mathfrak{T}$
contains only discrete spaces, then
$\Sigma=\mathrm{Z}={\Omega}_{\lnot\lnot}=\Omega=\mathbf{2}$, so all objects in
$\mathsf{Sh}(\mathfrak{T})$ are compact.

We have enough preparation to consider metrization in gros topos. Which metric
spaces are metrized depends very much on what $\mathfrak{T}$ we take. For
example, if $\mathfrak{T}$ contains only $\emptyset$ and a singleton, then
$\mathsf{Sh}(\mathfrak{T})$ is equivalent to $\mathbf{\underline{Set}}$, and
we are in the situation of Section 5.1. Topological properties of gros topos
are nicer when $\mathfrak{T}$ contains more diverse spaces. Here we consider
the case when $\mathfrak{T}$ consists of separable metric spaces666Separable
metric spaces form a proper class rather than a set, so we can’t literally
take them all. However, we can take its skeleton, i.e. one out of every
homeomorphism class, which amounts to a set, as the cardinalities of such
spaces are bounded above by the cardinality of continuum. When we discuss that
a space is in this $\mathfrak{T}$, we actually refer to its representative in
its homeomorphism class, but we don’t bother keeping mentioning this.. This
$\mathfrak{T}$ is closed for countable limits and countable coproducts (all of
which are calculated the same as in $\mathbf{\underline{Top}}$).

It is known [41] that for such $\mathfrak{T}$ the objects of natural numbers
and real numbers in $\mathsf{Sh}(\mathfrak{T})$ are simply
$\mathsf{y}{\mathbb{N}}$ and $\mathsf{y}{\mathbb{R}}$, respectively. Actually,
$\mathsf{y}{\mathbb{R}}$ is the object of Dedekind reals, but it is easy to
see that its strict order is open, therefore in $\mathsf{Sh}(\mathfrak{T})$
Dedekind reals match what we defined as real numbers. Similarly, certain
subspaces such as internal $\mathbb{N}_{<n}$ and $\mathbb{R}_{\geq 0}$ are
representable as well.

Note that we can study metrization in this $\mathsf{Sh}(\mathfrak{T})$ since
$\mathsf{y}{\mathbb{N}}$ and $\mathsf{y}{\emptyset}$ are overt by Proposition
5.12. Also, observe that the real numbers (and hence all metric spaces) are
Hausdorff in $\mathsf{Sh}(\mathfrak{T})$ by Corollary 3.35.

###### Theorem 5.13

Let $(X,d)$ be a metric space in $\mathfrak{T}$. Then
$(\mathsf{y}{X},\mathsf{y}{d})$ is a metrized metric space in
$\mathsf{Sh}(\mathfrak{T})$.

###### Proof.

Since the object of real numbers in $\mathsf{Sh}(\mathfrak{T})$ is
$\mathsf{y}{\mathbb{R}}$, and because the conditions for the metric space are
expressed in the negative fragment of logic (which is preserved by
$\mathsf{y}{}$ since limits are), $\mathsf{y}{d}\colon\mathsf{y}{(X\times
X)}\to\mathsf{y}{\mathbb{R}}$, or equivalently
$\mathsf{y}{d}\colon\mathsf{y}{X}\times\mathsf{y}{X}\to\mathsf{y}{\mathbb{R}}$,
is a metric on $\mathsf{y}{X}$.

We phrase the internal metrization of $(\mathsf{y}{X},\mathsf{y}{d})$ in such
a way as to be suitable to interpret it externally. It is sufficient to prove

$\displaystyle\forall\,U\,{\in}\,\mathcal{O}(\mathsf{y}{X})\,.\,\exists\,V\,{\in}\,\mathcal{O}(\mathsf{y}{X}\times\mathsf{y}{\mathbb{R}})\,.\,$
$\displaystyle\Big{(}$
$\displaystyle\forall\,(x,r,y)\,{\in}\,\mathsf{y}{X}\times\mathsf{y}{\mathbb{R}}\times\mathsf{y}{X}\,.\left((x,r)\in
V\land\mathsf{y}{d}(x,y)<r\implies y\in U\right)\land$
$\displaystyle\forall\,y\,{\in}\,\mathsf{y}{X}\,.\left(y\in
U\implies\exists\,(x,r)\,{\in}\,\mathsf{y}{X}\times\mathsf{y}{\mathbb{R}}\,.\left((x,r)\in
V\land\mathsf{y}{d}(x,y)<r\right)\right)\Big{)}$

since by Proposition 5.12 $\mathsf{y}{X}\times\mathsf{y}{\mathbb{R}}$ is
overt, so an open subset in it is subovert (in fact even overt by Corollary
2.26).

For the proof we have to take an arbitrary $A\in\text{Obj}(\mathfrak{T})$, and
any $U\in\mathcal{O}(A\times X)$. Next we need a suitable open cover of $A$,
but we claim that the cover with the single member $A$ will do. We pick the
following $V\in\mathcal{O}(A\times X\times\mathbb{R})$:

$V:=\text{Int}\left\\{(a,x,r)\in A\times
X\times\mathbb{R}\;\middle|\;\\{a\\}\times B\left(x,r\right)\subseteq
U\right\\}.$

We prove the two conjuncts individually.

  * •

Take any $f\colon B\to A$ from $\mathfrak{T}$, any
$(x,r,y)\in\mathscr{C}(B,X)\times\mathscr{C}(B,\mathbb{R})\times\mathscr{C}(B,X)$,
and any $g\colon C\to B$ from $\mathfrak{T}$. Suppose that

$\forall\,c\,{\in}\,C\,.\,\big{(}f(g(c)),x(g(c)),r(g(c))\big{)}\in
V\quad\text{and}\quad\forall\,c\,{\in}\,C\,.\,d\big{(}x(g(c)),y(g(c))\big{)}<r(g(c))$

hold; by the definition of $V$ this clearly implies
$\forall\,c\,{\in}\,C\,.\,\big{(}f(g(c)),y(g(c))\big{)}\in U$.

  * •

Take any $f\colon B\to A$ from $\mathfrak{T}$, any $y\in\mathscr{C}(B,X)$, and
any $g\colon C\to B$ from $\mathfrak{T}$. Suppose
$\forall\,c\,{\in}\,C\,.\,\big{(}f(g(c)),y(g(c))\big{)}\in U$ holds. We
require a suitable open cover of $C$, and again we take just the whole $C$
while picking $(x,r)\in\mathscr{C}(C,X)\times\mathscr{C}(C,\mathbb{R})$ in the
following way:

$x(c):=y(g(c)),\qquad
r(c):=\tfrac{1}{4}\sup\left\\{s\in{\mathbb{R}}_{[0,1]}\;\middle|\;B_{A}\left(f(g(c)),s\right)\times
B_{X}\left(x(c),s\right)\subseteq U\right\\}.$

The map $r$ is indeed continuous since it is the quarter of the infimum of $1$
and the product distance of the point $\big{(}f(g(c)),x(c)\big{)}$ from the
complement of $U$ (we bound $s$ by $1$ in case the complement of $U$ is
empty); also note that it is always positive (by the supposition above since
$U$ is open).

The statement $\forall\,c\,{\in}\,C\,.\,\big{(}f(g(c)),x(c),r(c)\big{)}\in V$
holds because we can wiggle $f(g(c))$, $x(c)$ and $r(c)$ by the distance
$r(c)$, and still satisfy the condition $\\{f(g(c))\\}\times
B\left(x(c),r(c)\right)\subseteq U$. The statement
$\forall\,c\,{\in}\,C\,.\,d\big{(}x(c),y(g(c))\big{)}<r(c)$ obviously holds
since the distance is zero.

∎

Let $(U,d_{\mathbf{U}},u,E)$ be the classical Urysohn space where the map
$E\colon P\to\mathbb{U}$ witnesses Urysohn properties; here
$P=\left\\{\left({x}_{i},{\omega}_{i}\right)_{i\in\mathbb{N}_{<n}}\in(U\times\mathbb{R}_{\geq
0})^{*}\;\middle|\;\forall\,i,j\,{\in}\,\mathbb{N}_{<n}\,.\left(\omega_{i}-\omega_{j}\leq
d_{\mathbf{U}}(x_{i},x_{j})\leq\omega_{i}+\omega_{j}\right)\right\\}$ (recall
Definition 4.45). We can write

$(U\times\mathbb{R}_{\geq
0})^{*}\cong\coprod_{n\in\mathbb{N}}(U\times\mathbb{R}_{\geq 0})^{n}.$

The Yoneda embedding preserves coproducts in $\mathfrak{T}$ which are
calculated the same as in $\mathbf{\underline{Top}}$, as is the case here.
Since it preserves the negative fragment of logic as well, in which the other
conditions for the Urysohn space can be expressed, we conclude that
$(\mathsf{y}{U},\mathsf{y}{d_{\mathbf{U}}})$ is the Urysohn space in
$\mathsf{Sh}(\mathfrak{T})$, witnessed by $\mathsf{y}{E}$ (after the tedious
verification that it is a CMS in $\mathsf{Sh}(\mathfrak{T})$). In short, the
Urysohn space in $\mathsf{Sh}(\mathfrak{T})$ is representable by the Urysohn
space in $\mathfrak{T}$.

###### Theorem 5.14

  1. 1.

All CMSs in $\mathsf{Sh}(\mathfrak{T})$ are metrized.

  2. 2.

All CTBs in $\mathsf{Sh}(\mathfrak{T})$ are metrized and compact.

###### Proof.

  1. 1.

By Theorem 4.56, using Proposition 4.42 and the fact that the Urysohn space is
metrized by Theorem 5.13.

  2. 2.

By the previous item $\textbf{CTB}{s}$ are metrized. In particular, the
Hilbert cube is metrized, and since it is representable (because
$(\mathsf{y}{\mathbb{I}})^{\mathsf{y}{\mathbb{N}}}\cong\mathsf{y}{(\mathbb{I}^{\mathbb{N}})}$),
it is compact by Proposition 5.12, as the classical Hilbert cube
$\mathbb{I}^{\mathbb{N}}$ is compact. We know that $\mathsf{y}{\mathbb{R}}$ is
Hausdorff. We conclude that $\textbf{CTB}{s}$ are compact by Theorem 4.44 (and
Proposition 4.42).

∎

[*]

## Bibliography

  * [1] P. Aczel.  The type-theoretic interpretation of constructive set theory.  In A. MacIntyre, L. Pacholski, and Paris J., editors, Logic Colloquium ’77, Amsterdam, 1978. North Holland.
  * [2] P. Aczel and Rathjen M.  Notes on constructive set theory.  Technical Report 40, Institut Mittag-Leffler, The Royal Swedish Academy of Sciences, 2001.
  * [3] A. Bauer.  First steps in synthetic computability.  Electronic Notes in Theoretical Computer Science, 155:5–31, 2006\.
  * [4] A. Bauer and D. Lešnik.  Metric spaces in synthetic topology.  Accepted for publication in Annals of Pure and Applied Logic, 2010.
  * [5] A. Bauer and P. Taylor.  The Dedekind reals in abstract Stone duality.  Mathematical Structures in Comp. Sci., 19(4):757–838, 2009.
  * [6] E. Bishop and D. Bridges.  Constructive Analysis.  Springer-Verlag, New York, 1985.
  * [7] D.S. Bridges and F. Richman.  Varieties of Constructive Mathematics, volume 97 of Lecture Note Ser. London Math. Soc., London, 1987.
  * [8] G.S. Ceĭtin.  Algorithmic operators in constructive complete separable metric spaces.  Doklady Akademii Nauk, 128:49–52, 1959.  In Russian.
  * [9] G.S. Ceĭtin.  Algorithmic operators in constructive metric spaces.  Tr. Mat. Inst. Steklov, 67:295–361, 1962.  In Russian, English trans. in AMS Trans. 64, 1967.
  * [10] T. Coquand, G. Sambin, J.M. Smith, and S. Valentini.  Inductively generated formal topologies.  Annals of Pure and Applied Logic, 124:71–106, 2003.
  * [11] T. Coquand and B. Spitters.  Constructive Gelfand duality for C*-algebras.  Accepted for publication in Mathematical Proceedings of the Cambridge Philosophical Society, 2009.
  * [12] J. Dugundji.  Topology.  Allyn and Bacon Series in Advanced Mathematics. Allyn and Bacon, Inc., Boston, 1974.
  * [13] M. Escardó.  Notes on synthetic topology.  Unpublished notes, 2004.
  * [14] M. Escardó.  Synthetic topology of data types and classical spaces.  Electronic Notes in Theoretical Computer Science, 87:21–156, 2004\.
  * [15] M. Escardó.  Intersections of compactly many open sets are open.  Unpublished notes, 2009.
  * [16] M. Escardó, J.D. Lawson, and A. Simpson.  Comparing cartesian closed categories of (core) compactly generated spaces.  Topology and its Applications, 143(1–3):105–145, 2004.
  * [17] R.M. Friedberg.  Un contre-example relatif aux fonctionnelles récursives.  Comptes rendus hebdomadaires des séances de l’Académie des Sciences (Paris), 247:852–854, 1958.  In French.
  * [18] G. Gierz, K.H. Hoffmann, K. Keimel, J.D. Lawson, M.W. Mislove, and D.S. Scott.  Continuous Lattices and Domains.  Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2003.
  * [19] C. Giovanni.  On the collection of points of a formal space.  Annals of Pure and Applied Logic, 137:126–146, 2006.
  * [20] M.R. Holmes.  The universal separable metric space of Urysohn and isometric embeddings thereof in Banach spaces.  In Fundamenta Mathematicae 140, pages 199–223. 1992.
  * [21] J.M.E. Hyland.  The effective topos.  In A.S. Troelstra and D. Van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165–216. North Holland Publishing Company, 1982.
  * [22] H. Ishihara.  Constructive reverse mathematics: Compactness properties.  In L. Crosilla and P. Schuster, editors, From Sets and Types to Analysis and Topology: Towards Practicable Foundations for Constructive Mathematics, volume 48 of Oxford Logic Guides, pages 245–267. Oxford University Press, 2005.
  * [23] T. Jech.  Set Theory.  Springer Monographs in Mathematics. Springer Verlag, Heidelberg, 2002\.
  * [24] P.T. Johnstone.  On a topological topos.  Proc. London Math. Soc., 38(3):237–271, 1979.
  * [25] P.T. Johnstone.  Open locales and exponentiation.  In Mathematical applications of category theory (Denver, Col., 1983), volume 30 of Contemp. Math., pages 84–116. Amer. Math. Soc., 1984\.
  * [26] P.T. Johnstone.  Sketches of an Elephant: A Topos Theory Compendium.  Oxford University Press, 2002.
  * [27] P.T. Johnstone.  Stone Spaces.  Cambridge University Press, 2002.  First published in 1982.
  * [28] A. Joyal and M. Tierney.  An extension of the Galois theory of Grothendieck.  Mem. Amer. Math. Soc., 51(309), 1984.
  * [29] M. Katětov.  On universal metric spaces.  In Z. Frolik, editor, General Topology and its Relations to Modern Analysis and Algebra, VI, pages 323–330. Heldermann, Berlin, 1988.
  * [30] S.C. Kleene.  On the interpretation of intuitionistic number theory.  Journal of Symbolic Logic, 10:109–124, 1945.
  * [31] S.C. Kleene and R. Vesli.  The Foundations of Intuitionistic Mathematics. Especially in Relation to Recursive Functions. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1965.
  * [32] A. Kock.  Synthetic Differential Geometry.  London Math. Society Lecture Note Series No 333. Cambridge University Press, 2006.  First published in 1981.
  * [33] G. Kreisel, D. Lacombe, and J.R. Shoenfield.  Partial recursive functionals and effective operations.  In A. Heyting, editor, Constructivity in Mathematics, Studies in Logic and the Foundations of Mathematics, pages 290–297, Amsterdam, 1959. North-Holland.  Proc. Colloq., Amsterdam, Aug. 26–31, 1957.
  * [34] B. Lambov.  RealLib: An efficient implementation of exact real arithmetic.  Mathematical Structures in Computer Science, 17:81–98, 2007.
  * [35] F.W. Lawvere.  Outline of synthetic differential geometry.  Preprint, available at http://www.acsu.buffalo.edu/~wlawvere/SDG_Outline.pdf, 1998.
  * [36] W.F. Lawvere.  Diagonal arguments and cartesian closed categories.  Lecture Notes in Mathematics, 92:135–145, 1969.  Republished as [37].
  * [37] W.F. Lawvere.  Diagonal arguments and cartesian closed categories with author commentary.  Reprints in Theory and Applications of Categories, 15:1–13, 2006\.
  * [38] D. Lešnik.  Constructive Urysohn universal metric space.  Journal of Universal Computer Science, 15(6):1236–1263, 2009.
  * [39] E. Lowen-Colebunders and G. Richter.  An elementary approach to exponential spaces.  Applied Categorical Structures, 9(3):303–310, 2001.
  * [40] Robert S. Lubarsky.  On the cauchy completeness of the constructive cauchy reals.  Electron. Notes Theor. Comput. Sci., 167:225–254, January 2007\.
  * [41] S. Mac Lane and I. Moerdijk.  Sheaves in Geometry and Logic.  Springer, New York, 1992.
  * [42] N. Müller.  The iRRAM: Exact arithmetic in C++.  In Jens Blanck, Vasco Brattka, and Peter Hertling, editors, Computability and Complexity in Analysis: 4th International Workshop, CCA 2000 Swansea, UK, September 17, 2000, Selected Papers, number 2064 in Lecture Notes in Computer Science, pages 222–252. Springer, 2001.
  * [43] J. Myhill.  Constructive set theory.  Journal of Symbolic Logic, 40(3):347–382, 1975.
  * [44] W. Phoa.  Domain Theory in Realizability Toposes.  PhD thesis, Cambridge, 1990.
  * [45] M. Pretnar.  Sintetična topologija.  Diplomsko delo, Fakulteta za matematiko in fiziko, Univerza v Ljubljani, 2005.  In Slovene.
  * [46] F. Richman.  Church’s thesis without tears.  The Journal of Symbolic Logic, 48(3):797–803, September 1983.
  * [47] F. Richman.  The fundamental theorem of algebra: a constructive development without choice.  Pacific Journal of Mathematics, 196(1):213–230, 2000.
  * [48] F. Richman.  Real numbers and other completions.  Mathematical Logic Quarterly, 54(1):98–108, 2008.
  * [49] A. Robinson.  Non-standard Analysis.  Princeton Landmarks in Mathematics and Physics. Princeton University Press, 1996.  First published in 1966.
  * [50] G. Rosolini.  Continuity and Effectiveness in Topoi.  PhD thesis, University of Oxford, 1986.
  * [51] G. Sambin.  Intuitionistic formal spaces — a first communication.  In D. Skordev, editor, Mathematical logic and its Applications, pages 187–204. Plenum, 1987.
  * [52] G. Sambin and Smith J.M., editors.  Twenty-five Years of Constructive Type Theory. Oxford University Press, 1998.  Reprinted in 2002.
  * [53] M. Shulman.  Synthetic differential geometry.  Notes from a talk at the graduate student pizza seminar at Chicago, available at http://www.math.uchicago.edu/~shulman/exposition/sdg/pizza-seminar.pdf, 2006\.
  * [54] P. Taylor.  Geometric and higher order logic in terms of abstract Stone duality.  Theory and Applications of Categories, 7(15):284–338, 2000.
  * [55] P. Taylor.  Computably based locally compact spaces.  Logical Methods in Computer Science, 2(1):1–70, 2006.
  * [56] P. Taylor.  Foundations for computable topology.  Unpublished notes, available at http://www.paultaylor.eu/ASD/foufct, 2009.
  * [57] A.S. Troelstra and D. van Dalen.  Constructivism in Mathematics, Volume 1, volume 121 of Studies in Logic and the Foundations of Mathematics.  North-Holland, Amsterdam, 1988.
  * [58] A.S. Troelstra and D. van Dalen.  Constructivism in Mathematics, Volume 2, volume 123 of Studies in Logic and the Foundations of Mathematics.  North-Holland, Amsterdam, 1988.
  * [59] P.S. Urysohn.  Sur un espace métrique universel.  Bulletin des Sciences Mathématiques, 51:43–64, 74–90, 1927\.  In French.
  * [60] K. Weihrauch.  Computable Analysis.  Springer, Berlin, 2000.

## Povzetek v slovenskem jeziku

Klasični matematični pristop k obravnavi matematičnih pojmov, kot so grupe,
vektorski prostori, topološki prostori, gladke mnogoterosti itd., je
obravnavati jih kot _množice_ z ustrezno _dodatno strukturo_ , morfizmi med
njimi pa so preslikave, ki to strukturo ohranjajo. Tak pristop se je izkazal
za plodovitega, saj imajo različne matematične panoge skupno osnovo — _teorijo
množic_.

Neprijetna posledica takega pristopa je, da je struktura, ki nas zanima,
pravzaprav dodatek in ne intrinzična lastnost množic, ki jih obravnavamo, kar
prinese zapletenejše definicije in dokaze. Na primer, v analizi na
mnogoterostih je tangentni sveženj matematično zelo kompleksen objekt, pa tudi
predstavljati si smerne vektorje kot ekvivalenčne razrede poti ni blizu
običajni intuiciji. Splošneje, pri konstrukciji kateregakoli svežnja je
potrebno opredeliti gladko strukturo na njegovi domeni in kodomeni ter
preveriti, da je projekcija gladka, kar je postopek, ki je pogosto samo
računsko zahteven, nima pa resne matematične vsebine, kljub vsemu pa ga je
treba opraviti, četudi na gladkost sklepamo že “po občutku”, kadar uporabljamo
standardne metode za konstrukcije.

Filozofija _sintetičnega_ pristopa k matematiki je obratna klasični: ne
izberemo eno osnovo za matematiko, pač pa za posamezno vejo zanjo
specializirano v smislu, da so objekti, preslikave, aksiomi, logika in
definicije prilagojeni tako, da zajamejo tisto vejo, izbrana struktura postane
intrinzična lastnost objektov in da se dokazi poenostavijo. Sintetična
diferencialna geometrija (s katero se je sintetični pristop začel) reši zgoraj
opisane težave.

V tej disertaciji predstavimo sintetično verzijo _topologije_. Za model
sintetične topologije vzamemo kategorijo z dovolj logične strukture (topos,
tj. kategorični model konstruktivne intuicionistične logike višjega reda), v
katerem so vsi objekti avtomatsko opremljeni z lastno (intrinzično) topologijo
in vsi morfizmi so glede na to topologijo zvezni. To dosežemo z izbiro
podobjekta $\Sigma$ klasifikatorja podobjektov $\Omega$ v toposu (tj.
podmnožice v množici resničnostnih vrednosti). Elementi $\Sigma$ so _odprte_
resničnostne vrednosti, podmnožice, klasificirane z njimi, pa _odprte_
podmnožice. Pogosto zahtevamo še dodatne lastnosti za $\Sigma$, kot naprimer,
da je dominanca (kar pomeni, da so končni preseki odprtih množic odprti in da
je odprtost tranzitivna lastnost — podmnožica, odprta v odprti podmnožici, je
odprta).

V drugem delu disertacije se osredotočimo na metrične prostore v modelih
sintetične topologije. Posebej proučimo, kdaj se metrična in intrinzična
topologija ujemata.

### Sintetična topologija

Definicijo sintetične topologije posplošimo tako, da začnemo s testnimi
resničnostnimi vrednostmi, iz katerih izpeljemo tako odprtost kot zaprtost.
Naj bo $\mathrm{T}\subseteq\Omega$ poljubna podmnožica množice resničnostnih
vrednosti $\Omega$. Definiramo

$\Sigma:=\left\\{u\in\Omega\;\middle|\;(u\land t)\in\mathrm{T}\text{ za vse
}t\in\mathrm{T}\right\\},$
$\mathrm{Z}:=\left\\{f\in\Omega\;\middle|\;(f\Rightarrow t)\in\mathrm{T}\text{
za vse }t\in\mathrm{T}\right\\}.$

Elementi množic $\mathrm{T}$, $\Sigma$ in $\mathrm{Z}$ se imenujejo _testne_ ,
_odprte_ in _zaprte_ resničnostne vrednosti. Podobno poimenujemo podmnožice,
klasificirane z njimi. Za množico $X$ vpeljemo oznake $\mathcal{T}(X)$,
$\mathcal{O}(X)$, $\mathcal{Z}(X)$ za njene testne, odprte in zaprte
podmnožice.

$\Sigma$ in $\mathrm{Z}$ sta spodnji omejeni polmreži.

###### Definicija 1

Množica $X$ je

  * •

_odkrita_ , kadar za vse $U\in\mathcal{O}(X)$ velja, da je resničnostna
vrednost $\exists\,x\,{\in}\,X\,.\,x\in U$ odprta,

  * •

_kompaktna_ , kadar za vse $U\in\mathcal{O}(X)$ velja, da je resničnostna
vrednost $\forall\,x\,{\in}\,X\,.\,x\in U$ odprta,

  * •

_kondenzirana_ , kadar za vse $F\in\mathcal{Z}(X)$ velja, da je resničnostna
vrednost $\exists\,x\,{\in}\,X\,.\,x\in F$ zaprta,

  * •

_Hausdorffova_ , kadar je diagonala v $X\times X$ zaprta podmnožica.

Odkritost, kompaktnost in kondenziranost se posplošijo na podmnožice.

###### Definicija 2

Podmnožica $A\subseteq X$ je

  * •

_pododkrita_ v $X$, kadar za vse $U\in\mathcal{O}(X)$ velja, da je
resničnostna vrednost $\exists\,x\,{\in}\,A\,.\,x\in U$ odprta,

  * •

_podkompaktna_ v $X$, kadar za vse $U\in\mathcal{O}(X)$ velja, da je
resničnostna vrednost $\forall\,x\,{\in}\,A\,.\,x\in U$ odprta,

  * •

_podkondenzirana_ v $X$, kadar za vse $F\in\mathcal{Z}(X)$ velja, da je
resničnostna vrednost $\exists\,x\,{\in}\,A\,.\,x\in F$ zaprta.

###### Trditev 3

Množica $X$ je kondenzirana natanko tedaj, ko je za vsako množico $Y$
projekcija $p\colon X\times Y\to Y$ zaprta preslikava.

###### Trditev 4

Če je $C\subseteq X$ podkondenzirana in $A\subseteq X$ zaprta, tedaj je $C\cap
A$ podkondenzirana.

###### Trditev 5

Če je $X$ Hausdorffov in $C\subseteq X$ podkondenzirana, tedaj je $C$ zaprta.

Odkritost, kompaktnost in kondenziranost posplošimo še na preslikave.

###### Definicija 6

Preslikava $f\colon X\to Y$ je

  * •

_odkrita_ , kadar za vse $U\in\mathcal{O}(Y)$ velja, da je resničnostna
vrednost $\exists\,x\,{\in}\,X\,.\,f(x)\in U$ odprta,

  * •

_kompaktna_ , kadar za vse $U\in\mathcal{O}(Y)$ velja, da je resničnostna
vrednost $\forall\,x\,{\in}\,X\,.\,f(x)\in U$ odprta,

  * •

_kondenzirana_ , kadar za vse $F\in\mathcal{Z}(Y)$ velja, da je resničnostna
vrednost $\exists\,x\,{\in}\,X\,.\,f(x)\in F$ zaprta.

###### Trditev 7

  1. 1.

Kompozicija odkrite/kompaktne/kondenzirane preslikave s poljubno preslikavo na
levi je odkrita/kompaktna/kondenzirana.

  2. 2.

Končni produkt odkritih/kompaktnih/kondenziranih preslikav je
odkrita/kompaktna/kondenzirana.

  3. 3.

Diagonalna preslikava v povleku preslikave z odprto/zaprto sliko vzdolž
odkrite/kondenzirane preslikave je odkrita/kondenzirana. Če
$\mathrm{T}=\Sigma$, analogno velja za kompaktne preslikave in zaprte slike.

Vemo, da so odprte podmnožice podprostori, kadar je $\Sigma$ dominanca. Za
zaprte množice obstaja analogen pojem kodominance.

###### Definicija 8

  * •

Podmnožica $A\subseteq X$ je _podprostor_ v $X$, kadar, za vsako testno
množico $B\in\mathcal{T}(A)$ obstaja taka testna množica $C\in\mathcal{T}(X)$,
da je $B=A\cap C$.

  * •

Odprta podmnožica, ki je obenem podprostor, se imenuje _krepko odprta_.

  * •

Zaprta podmnožica, ki je obenem podprostor, se imenuje _krepko zaprta_.

Krepko odprte in krepko zaprte podmnožice so podprostori na kanoničen način.

###### Lema 9

  1. 1.

Naj bo $A\subseteq U\subseteq X$. Če je $U$ krepko odprta v $X$ in $A$ testna
v $U$, tedaj je $A$ ($=U\cap A$) testna v $X$.

  2. 2.

Naj bo $A\subseteq F\subseteq X$. Če je $F$ krepko zaprta v $X$ in $A$ testna
v $F$, tedaj je $F\mathop{==\raisebox{0.94722pt}{\text{\scriptsize$)$}}_{X}}A$
testna v $X$.

###### Trditev 10

Podmnožica, odprta/zaprta v krepko odprti/zaprti podmnožici, je odprta/zaprta.

###### Trditev 11

  1. 1.

Resničnostna vrednost $u\in\Omega$ je krepko odprta natanko tedaj, ko zanjo
velja pogoj

$\forall\,p\,{\in}\,\Omega\,.\left((u\Rightarrow(p\in\mathrm{T}))\implies(u\land
p)\in\mathrm{T}\right).$

  2. 2.

Resničnostna vrednost $f\in\Omega$ je krepko zaprta natanko tedaj, ko zanjo
velja pogoj

$\forall\,p\,{\in}\,\Omega\,.\left((f\Rightarrow(p\in\mathrm{T}))\implies(f\Rightarrow
p)\in\mathrm{T}\right).$

###### Definicija 12

  * •

$\Sigma$ je _dominanca_ za $\mathrm{T}$, kadar so vse odprte resničnostne
vrednosti krepko odprte.

  * •

$\mathrm{Z}$ je _kodominanca_ za $\mathrm{T}$, kadar so vse zaprte
resničnostne vrednosti krepko zaprte.

###### Lema 13

Naj bo $U\subseteq X$. Če za vsak $x\in X$ velja, da je resničnostna vrednost
$x\in U$ krepko odprta, tedaj je $U$ krepko odprta podmnožica v $X$. Analogno
za zaprtost.

###### Trditev 14

Naslednje trditve so ekvivalentne.

  1. 1.

$\Sigma$ je dominanca.

  2. 2.

Krepko odprte podmnožice so klasificirane s krepko odprtimi resničnostnimi
vrednostmi.

  3. 3.

Krepko odprte podmnožice so klasificirane z neko podmnožico v $\Omega$.

  4. 4.

Preslikave so zvezne glede na krepko odprte podmnožice.

Analogno za zaprtost.

V tipičnih modelih sintetične topologije ima običajno $\Sigma$ dodatne
lastnosti.

###### Izrek 15

Predpostavimo, da velja $\mathrm{T}=\Sigma\subseteq{\Omega}_{\lnot\lnot}$ in
da je $\Sigma$ zaprta za $\lor$. Tedaj velja:

  1. 1.

$\mathrm{Z}=\left\\{f\in\Omega\;\middle|\;\lnot{f}\in\Sigma\right\\}$,

  2. 2.

$\Sigma=\lnot\mathrm{Z}$,

  3. 3.

$\lnot\lnot\mathrm{Z}=\lnot\Sigma={\mathrm{Z}}_{\lnot\lnot}$,

  4. 4.

kondenziranost in kompaktnost se ujemata; poleg tega je kondenziranost dovolj
preveriti le za stabilne zaprte podmnožice,

  5. 5.

$\mathrm{Z}$ je omejena podmreža v $\Omega$,

  6. 6.

$\Sigma\cap\mathrm{Z}=\mathbf{2}=\Sigma\cap{\mathrm{Z}}_{\lnot\lnot}$,

  7. 7.

$\Sigma$ je dominanca natanko tedaj, ko je odprtost tranzitivna,

  8. 8.

$\mathrm{Z}$ je kodominanca natanko tedaj, ko je zaprtost tranzitivna, in prav
tako so stabilne zaprte podmnožice podprostori natanko tedaj, ko je stabilna
zaprtost tranzitivna.

Topologijo lahko opišemo z bazo.

###### Definicija 16

Preslikava $b\colon\mathscr{B}\to\mathcal{O}(X)$ je _baza_ za $X$, kadar za
vsak $U\in\mathcal{O}(X)$ obstaja množica $I$ in odkrita (indeksirajoča)
preslikava $a\colon I\to\mathscr{B}$, da velja
$U=\bigcup\left\\{b(a(i))\;\middle|\;i\in I\right\\}$.

Primer uporabe baze je definicija produktne topologije.

###### Definicija 17

Množica $X\times Y$ ima _produktno topologijo_ , kadar je preslikava
$p\colon\mathcal{O}(X)\times\mathcal{O}(Y)\to\mathcal{O}(X\times Y)$, dana kot
$P(U,V):=U\times V$, baza za $X\times Y$.

### Realna števila in metrični prostori

Naš namen je obravnavati metrične prostore v kontekstu sintetične topologije.
Posebej želimo uvideti povezavo med metrično in intrinzično topologijo
metričnih prostorov. Osnovni pogoj za to obravnavo je, da so števne množice
odkrite (v tem in naslednjem razdelku to predpostavimo) in da je relacija
stroge urejenosti $<$ na realnih številih odprta (ekvivalentno, da so metrične
odprte krogle intrinzično odprte). V ta namen rekonstruiramo realna števila.

###### Definicija 18

Struktura $(X,<,+,0,\cdot,1)$ je _proga_ , kadar je

  * •

$<$ stroga linearna urejenost,

  * •

$(X,+,0)$ komutativni monoid,

  * •

$(X_{>0},\cdot,1)$ komutativni monoid na pozitivnih elementih iz $X$, pri
čemer je množenje distributivno glede na seštevanje,

  * •

$<$ arhimedsko ureja $X$,

  * •

za vsak $x\in X$ obstaja $a\in X_{>0}$, da je $x+a>0$,

  * •

$<$ je intrinzično odprta relacija na $X$.

Preslikava med progama je _morfizem prog_ , kadar ohranja vso strukturo proge.

Izkaže se:

  * •

vsi morfizmi prog so injektivni in kategorija prog je šibka urejenost,

  * •

množica naravnih števil $\mathbb{N}$ je začetna proga,

  * •

množica celih števil $\mathbb{Z}$ je začetna med progami, ki so kolobarji,

  * •

množica racionalnih števil $\mathbb{Q}$ je začetna med progami, ki so obsegi.

Intuitivno so proge aditivni podmonoidi realnih števil, ki vsebujejo $1$ in so
zaprti za množenje pozivnih elementov. Posledično je smiselna sledeča
definicija.

###### Definicija 19

Realna števila $\mathbb{R}$ so končna proga.

###### Izrek 20

V toposu z naravnimi števili za vsak $\Sigma$, glede na katerega so števne
množice odkrite, realna števila obstajajo. Primer modela so odprti
(dvostranski) Dedekindovi rezi.

Naša konstrukcija realnih števil je torej običajna, le da se omejimo na odprte
Dedekindove reze in s tem dosežemo odprtost relacije $<$. V primeru
$\Sigma=\Omega$ dobimo standardna Dedekindova realna števila (v standardnih
modelih sintetične topologije so sicer vsi Dedekindovi rezi odprti in se torej
naša realna števila ujemajo z običajnimi).

Definicija metričnih prostorov in njihovih lastnosti je večidel standardna.
Izjemi sta (zaradi odsotnosti aksioma izbire) popolna omejenost in polnost.

###### Definicija 21

Metrični prostor $(X,d,s,a)$, skupaj z zaporedjema
$s\colon\mathbb{N}\to\mathbf{1}+X$, $a\colon\mathbb{N}\to\mathbb{N}$, je
_popolnoma omejen_ , kadar velja

$\forall\,n\,{\in}\,\mathbb{N}\,.\,\forall\,x\,{\in}\,X\,.\,\exists\,k\,{\in}\,(s^{-1}(X)\cap\mathbb{N}_{<a_{n}})\,.\,d(x,s_{k})<2^{-n}.$

###### Definicija 22

_Napolnitev metričnega prostora_ $(X,d)$ je končna med gostimi izometrijami z
domeno $X$. Prostor je _poln_ , kadar je identiteta na njem njegova
napolnitev.

###### Izrek 23

Če metrični prostor vsebuje gosto pododkrito podmnožico, tedaj je njegova
vložitev v prostor ekvivalenčnih razredov Cauchyjevih družin oziroma v prostor
lokacij njegova napolnitev. Če velja $\text{{AC}}_{\Sigma}(\mathbb{N})$, tedaj
je vložitev v prostor ekvivalenčnih razredov Cauchyjevih zaporedij njegova
napolnitev.

### Metrizacijski izreki

Priprava iz prejšnjega razdelka implicira, da so v metričnih prostorih krogle
intrinzično odprte in se torej lahko vprašamo, ali tvorijo bazo prostora.

###### Definicija 24

Za metrični prostor $(X,d)$ rečemo, da je _metriziran_ (oziroma da je $X$
_metriziran_ z metriko $d$), kadar je preslikava $B\colon
X\times\mathbb{R}\to\mathcal{O}(X)$, definirana kot

$B\left(a,r\right):=\left\\{x\in X\;\middle|\;d(a,x)<r\right\\},$

baza za $X$.

Primer metriziranih prostorov so odkrite množice z odločljivo enakostjo,
opremljene z diskretno metriko. Po drugi strani je jasno, da vsi metrični
prostori ne morejo biti metrizirani, saj na množici v splošnem obstajajo
medsebojno neekvivalentne metrike. V tem razdelku podamo nekaj zadostnih (in
potrebnih) pogojev za to, kdaj so določene skupine metričnih prostorov
metrizirane. To dosežemo s preslikavami med metričnimi prostori, ki ohranjajo
metriziranost. Zanimivi prostori, ki imajo obilo takih preslikav in se jih
poslužimo v disertaciji, so sledeči:

  * •

poln metrično separabilen ultrametričen _Bairov prostor_
$\mathbb{N}^{\mathbb{N}}$, tj. števni produkt prostorov $\mathbb{N}$,
opremljenih z diskretno metriko;

  * •

Cantorjev prostor $\mathbf{2}^{\mathbb{N}}$, ki je poln popolnoma omejen
ultrametričen podprostor (še več, retrakt) Bairovega prostora;

  * •

podprostor (in retrakt) Cantorjevega prostora, definiran kot

$\mathbb{N}^{\bullet}:=\left\\{\alpha\in\mathbf{2}^{\mathbb{N}}\;\middle|\;\forall\,n\,{\in}\,\mathbb{N}\,.\left(\alpha_{n}=0\implies\alpha_{n+1}=0\right)\right\\}$

(intuitivno je $\mathbb{N}^{\bullet}$ “kompaktifikacija prostora $\mathbb{N}$
z eno točko”, v smislu, da zaporedje $n$ enic, ki se nadaljuje z ničlami,
predstavlja $n\in\mathbb{N}$, medtem ko zaporedje samih enic predstavlja
$\infty$);

  * •

prostora $\mathbb{R}$ in $\mathbb{I}$, opremljena z evklidsko topologijo;

  * •

_Hilbertova kocka_ $\mathbb{I}^{\mathbb{N}}$;

  * •

_Urisonov prostor_ , tj. poln metrično separabilen prostor, univerzalen za
razširjanje izometrij vanj s končne na metrično separabilno domeno (ob tem
pokažemo, da tak prostor obstaja tudi konstruktivno).

Kdaj je diskreten metrični prostor metriziran, vemo. Za obravnavo prostorov s
stekališči je uporaben princip WSO:

$\forall\,U\,{\in}\,\mathcal{O}(\mathbb{N}^{\bullet})\,.\left(\infty\in
U\implies U\between\mathbb{N}\right).$

Gre za to, da je $\infty$ stekališče $\mathbb{N}$ v metričnem smislu, WSO pa
zagotavlja, da je tudi v intrinzičnem. Okrajšava WSO pomeni (v angleščini)
‘weakly sequentially open’.

Princip WSO je tesno povezan s sintetično kompaktnostjo in metriziranostjo
(predvsem metrično separabilnih ter popolnoma omejenih) metričnih prostorov.

###### Trditev 25

Princip WSO je neklasičen (tj. implicira negacijo izključene tretje možnosti).

###### Definicija 26

Metrični prostor je _Lebesgueov_ , kadar za vsako njegovo odkrito indeksirano
pokritje s kroglami velja, da obstaja $\epsilon\in\mathbb{R}_{>0}$, za
katerega lahko zmanjšamo radije, pa krogle še vedno pokrivajo prostor.

###### Izrek 27

Za metrični prostor $\mathbf{X}=(X,d)$ veljajo sledeče trditve.

  1. 1.

Če je $X$ odkrit, WSO velja in so zaprte krogle v $\mathbf{X}$ s polmeri
oblike $2^{-t}$, $t\in\mathbb{N}^{\bullet}$, podkompaktne, tedaj je
$\mathbf{X}$ metriziran.

  2. 2.

Če je $X$ kompakten in WSO velja, je $\mathbf{X}$ Lebesgueov.

  3. 3.

Naj velja $\text{{AC}}_{\Sigma}(\mathbb{N},\mathbb{N})$ in WSO. Če je $X$
kompakten in $\mathbf{X}$ metrično separabilen, tedaj je $\mathbf{X}$
popolnoma omejen.

  4. 4.

Če je $\mathbf{X}$ popolnoma omejen, Lebesgueov in metriziran, tedaj je odkrit
in kompakten.

###### Posledica 28

Naj velja WSO in naj bo $\mathbb{R}$ Hausdorffov. Sledeči trditvi sta
ekvivalentni za popolnoma omejen metrični prostor $\mathbf{X}=(X,d,s,a)$.

  1. 1.

$X$ je odkrit in kompakten.

  2. 2.

$\mathbf{X}$ je Lebesgueov in metriziran.

Posledično je odkrita kompaktna množica metrizirana s katerokoli popolnoma
omejeno metriko na njej (posebej to pomeni, da so vse te metrike medsebojno
ekvivalentne).

###### Izrek 29

Predpostavimo WSO.

  1. 1.

Vsaka kompaktna preslikava, ki slika v $\mathbb{R}$, je omejena.

  2. 2.

Naj velja $\Sigma\subseteq{\Omega}_{\lnot\lnot}$. Če je $X$ posedujoč in
$f\colon X\to\mathbb{R}$ odkrita kompaktna preslikava, tedaj ima $f$ supremum
in infimum.

###### Posledica 30

Če WSO velja, tedaj so (pod)kompaktni metrični (pod)prostori omejeni.

###### Trditev 31

  1. 1.

$\mathbb{N}^{\bullet}$ je Lebesgueov.

  2. 2.

$\mathbf{2}^{\mathbb{N}}$ je Lebesgueov natanko tedaj, ko je vsaka pododkrita
prečka enakomerna (različica Brouwerjevega načela za pahljače).

  3. 3.

$\mathbb{N}^{\mathbb{N}}$ ni Lebesgueov.

###### Izrek 32

Izmed sledečih trditev sta prvi dve ekvivalentni, iz njiju sledi tretja in če
je $\Sigma$ dominanca, so vse tri ekvivalentne.

  1. 1.

$\mathbb{N}^{\bullet}$ je kompakten in WSO velja.

  2. 2.

$\mathbb{N}^{\bullet}$ je metriziran.

  3. 3.

Za vsak $U\in\mathcal{O}(\mathbb{N}^{\bullet})$ velja, da če vsebuje $\infty$,
tedaj obstaja $\epsilon\in\mathbb{R}_{>0}$, da
$B\left(\infty,r\right)\subseteq U$.

###### Izrek 33

Spodnji trditvi sta ekvivalentni.

  1. 1.

$\mathbf{2}^{\mathbb{N}}$ je kompakten in WSO velja.

  2. 2.

$\mathbf{2}^{\mathbb{N}}$ je metriziran in vsaka pododkrita prečka je
enakomerna.

###### Izrek 34

Spodnji trditvi sta ekvivalentni tako za Bairov kot za Cantorjev prostor.

  1. 1.

Bairov/Cantorjev prostor je metriziran.

  2. 2.

Bairov/Cantorjev prostor ima produktno intrinzično topologijo in WSO velja.

Naš cilj je sedaj karakterizirati metrizacijo polnih metrično separabilnih in
polnih popolnoma omejenih metričnih prostorov z metrizacijo enega prostora iz
vsake skupine. Spomnimo se dveh skupin preslikav iz klasične topologije, preko
katerih je topologija enega prostora porojena s topologijo drugega: kvocientne
preslikave in topološke vložitve. V splošnem v sintetični topologiji
surjekcije ohranjajo intrinzično topologijo, ne pa nujno metrične, medtem ko
za injekcije velja ravno obratno.

###### Definicija 35

Preslikava med metričnimi prostori $f\colon\mathbf{X}\to\mathbf{Y}$ je
_metrična kvocientna_ , kadar je surjektivna in ohranja metrično topologijo v
smislu, da za vsak $U\subseteq\mathbf{Y}$ velja

$U\text{ metri\v{c}no odprta v }\mathbf{Y}\iff f^{-1}(U)\text{ metri\v{c}no
odprta v }\mathbf{X}.$

###### Trditev 36

Če je $f\colon\mathbf{X}\to\mathbf{Y}$ metrična kvocientna in je $\mathbf{X}$
metriziran, potem je metriziran tudi $\mathbf{Y}$.

###### Izrek 37

Predpostavimo $\text{{AC}}_{\Sigma}(\mathbb{N},\mathbb{N})$.

  1. 1.

Za vsak poln metrično separabilen prostor obstaja kvocientna preslikava z
retrakta Bairovega prostora nanj.

  2. 2.

Za vsak poln popolnoma omejen metrični prostor obstaja kvocientna preslikava z
retrakta Cantorjevega prostora nanj.

###### Izrek 38

Naj velja $\text{{AC}}_{\Sigma}(\mathbb{N},\mathbb{N})$.

  1. 1.

Če je Bairov prostor metriziran, so metrizirani vsi polni metrično separabilni
prostori.

  2. 2.

Če je Cantorjev prostor metriziran, so metrizirani vsi polni popolnoma omejeni
metrični prostori.

  3. 3.

Če je Cantorjev prostor kompakten, so kompaktni vsi polni popolnoma omejeni
metrični prostori.

Zdaj se posvetimo še vložitvam.

###### Izrek 39

Naj bo $A\subseteq X$, $\mathbf{X}=(X,d_{\mathbf{X}})$ metrični prostor in
$\mathbf{A}=(A,d_{\mathbf{A}})$ njegov metrični podprostor.

  1. 1.

Če je $\mathbf{A}$ metriziran, je $A$ podprostor (v intrinzičnem smislu) v
$X$.

  2. 2.

Če je $\mathbf{X}$ metriziran, $A$ podprostor v $X$ in $A$ vsebuje pododkrito
metrično gosto podmnožico, tedaj je $\mathbf{A}$ metriziran.

###### Posledica 40

Metrično separabilen metrični podprostor v metriziranem prostoru je metriziran
natanko tedaj, ko je podprostor v intrinzičnem smislu.

###### Definicija 41

Podmnožica $A\subseteq X$ je _krepko umeščena_ v metričnem prostoru
$\mathbf{X}=(X,d)$, kadar je umeščena v $\mathbf{X}$ in velja $A=\left\\{x\in
X\;\middle|\;d(A,x)=0\right\\}$.

###### Lemma 5.15

Naj bo $\mathbf{X}=(X,d_{\mathbf{X}})$ metrični prostor, $A\subseteq X$
umeščena v $\mathbf{X}$ in $\mathbf{A}=(A,d_{\mathbf{A}})$ poln metrični
podprostor v $\mathbf{X}$, ki vsebuje pododkrito metrično gosto podmnožico.
Tedaj je $A$ krepko umeščena.

###### Trditev 42

Če je $\mathbb{R}$ Hausdorffov in so stabilne zaprte množice podprostori,
potem so krepko umeščene podmnožice podprostori.

###### Izrek 43

  1. 1.

Vsak metrično separabilen metrični prostor se vloži v Urisonov prostor kot
umeščena podmnožica. Če je poln, je vložitev krepko umeščena.

  2. 2.

Vsak popolnoma omejen metrični prostor se vloži v Hilbertovo kocko kot
umeščena podmnožica. Če je poln, je vložitev krepko umeščena.

###### Izrek 44

Naj velja, da so krepko umeščene podmnožice podprostori.

  1. 1.

Če je Urisonov prostor metriziran, so metrizirani vsi polni metrično
separabilni prostori.

  2. 2.

Če je Hilbertova kocka metrizirana, so metrizirani vsi polni popolnoma omejeni
metrični prostori.

  3. 3.

Če je Hilbertova kocka kompaktna in $\mathbb{R}$ Hausdorffov, so vsi polni
popolnoma omejeni metrični prostori kompaktni.

Sledeči izrek povzame teorijo metrizacije polnih metrično separabilnih oziroma
popolnoma omejenih metričnih prostorov.

###### Izrek 45

Predpostavimo, da so polni metrično separabilni/popolnoma omejeni prostori
metrizirani. Tedaj veljajo naslednje trditve.

  1. 1.

Intrinzična topologija polnih metrično separabilnih/popolnoma omejenih
prostorov se izraža z metričnimi kroglami. Natančneje, podmnožica je odprta
natanko tedaj, ko je odkrito indeksirana unija krogel.

  2. 2.

Do topološke ekvivalence natančno lahko množico opremimo z največ eno metriko,
glede na katero postane poln metrično separabilen/popolnoma omejen prostor.

  3. 3.

Polni metrično separabilni/popolnoma omejeni prostori imajo števno bazo.

  4. 4.

Polni metrično separabilni/popolnoma omejeni prostori so odkriti.

  5. 5.

Princip WSO, skupaj s svojimi posledicami, velja.

  6. 6.

Za poljuben poln metrično separabilen/popolnoma omejen prostor
$\mathbf{X}=(X,d)$ je vsaka preslikava $f\colon X\to Y$ metrično zvezna in
posledično $\epsilon\text{-}\delta$-zvezna, ne glede na izbiro metrike na $Y$.

### Modeli sintetične topologije

V tem razdelku uporabimo splošno teorijo za štiri konkretne modele sintetične
topologije:

  * •

klasično matematiko,

  * •

izračunljivost prvega tipa oziroma ruski konstruktivizem,

  * •

izračunljivost drugega tipa oziroma močnejša verzija Brouwerjevega
intuicionizma,

  * •

gros topos nad separabilnimi metričnimi prostori.

V klasični teoriji množic velja $\Omega=\mathbf{2}$. Imamo torej štiri
možnosti za $\mathrm{T}\subseteq\Omega$.

  * •

$\mathrm{T}=\emptyset$
Tedaj $\Sigma=\mathrm{Z}=\mathbf{2}$. Vse množice so diskretne, Hausdorffove,
odkrite, kompaktne in kondenzirane.

  * •

$\mathrm{T}=\\{\bot\\}$
Tedaj $\Sigma=\mathbf{2}$, ampak $\mathrm{Z}=\\{\top\\}$, torej so vse
podmnožice odprte, a le celotne množice so zaprte v samih sebi. Vse množice so
diskretne, odkrite in kompaktne, samo prazna in enojci so Hausdorffovi in
posedujoče množice so kondenzirane.

  * •

$\mathrm{T}=\\{\top\\}$
Tedaj $\Sigma=\\{\mathrm{T}\\}$ in $\mathrm{Z}=\mathbf{2}$. Samo celotne
množice so odprte v sebi, so pa vse množice zaprte. Le prazna množica in
enojci so diskretni, posedujoče množice so odkrite, medtem ko so vse množice
Hausdorffove, kompaktne in kondenzirane.

  * •

$\mathrm{T}=\mathbf{2}$
Tedaj spet $\Sigma=\mathrm{Z}=\mathbf{2}$. Vse množice so diskretne,
Hausdorffove, odkrite, kompaktne in kondenzirane.

Za našo teorijo metričnih prostorov pride v poštev le slednja (ki je tudi
standardna) izbira $\mathrm{T}=\Sigma=\mathrm{Z}=\mathbf{2}$, saj želimo, da
so števne množice odkrite in $\mathrm{T}=\Sigma$. To je trivialni model naše
teorije, saj so vse množice odkrite in imajo odločljivo enakost ter so
posledično metrizirane z diskretno metriko.

Za izračunljivost prvega tipa veljajo sledeči aksiomi.

  * •

Števna izbira $\text{{AC}}(\mathbb{N})$ in splošneje odvisna izbira.

  * •

_Princip Markova_ : če v dvojiškem zaporedju niso vsi členi enaki $1$, obstaja
člen, ki je enak $0$.

  * •

_Aksiom naštevnosti_ : števnih podmnožic $\mathbb{N}$ je števno mnogo.

V tem modelu vzamemo $\Sigma=\Sigma^{0}_{1}$. Čeprav WSO velja, nediskretni
metrični prostori nasplošno niso metrizirani.

###### Izrek 46

WSO velja, obenem pa obstaja taka $V\in\mathcal{O}(\mathbb{N}^{\bullet})$, da
$\infty\in V$, vendar $B\left(\infty,r\right)$ ni vsebovana v $V$ za noben
$r\in\mathbb{R}_{>0}$.

###### Izrek 47

Naj metrični prostor $\mathbf{X}=(X,d)$ vsebuje pododkrito metrično gosto
podmnožico.

  1. 1.

Če $\mathbf{X}$ vsebuje stekališče, tedaj ni niti metriziran niti kompakten.

  2. 2.

Definirajmo, da je $\mathbf{X}$ lokalno polumeščen, kadar za vsak $x\in X$
obstaja tak $r\in\mathbb{R}_{>0}$, da je razdalja od $x$ do prebodene krogle
okrog $x$ s polmerom $r$, tj.

$d\big{(}\left\\{y\in X\;\middle|\;0<d(x,y)<r\right\\},x\big{)},$

razširjeno realno število. Tedaj sta sledeči trditvi ekvivalentni.

     * •

$\mathbf{X}$ je metriziran in lokalno polumeščen.

     * •

Metrika $d$ je ekvivalentna diskretni metriki.

Posebej, če drži ena od teh trditev (in s tem obe), ima $X$ odločljivo
enakost.

Ta izrek velja tudi, če povečamo $\Sigma$.

Za izračunljivost drugega tipa veljajo sledeči aksiomi.

  * •

_Funkcijsko funkcijska izbira_
$\text{{AC}}(\mathbb{N}^{\mathbb{N}},\mathbb{N}^{\mathbb{N}})$.

  * •

_Princip zveznosti_ : za vsako $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$
in $\alpha\in\mathbb{N}^{\mathbb{N}}$ obstaja $k\in\mathbb{N}$, da $\beta\in
B\left(\alpha,2^{-k}\right)$ implicira $f(\alpha)=f(\beta)$ (na kratko: $f$ je
$\epsilon\text{-}\delta$-zvezna).

  * •

_Princip pahljače_ : vsaka odločljiva prečka je enakomerna.

Spet vzamemo $\Sigma=\Sigma^{0}_{1}$.

###### Izrek 48

Bairov prostor $\mathbb{N}^{\mathbb{N}}$ je metriziran. Posledično, vsi polni
metrično separabilni prostori so metrizirani.

###### Izrek 49

Cantorjev prostor je kompakten. Posledično so vsi polni popolnoma omejeni
metrični prostori kompaktni.

Gros topos $\mathsf{Sh}(\mathfrak{T})$ je topos snopov nad majhno polno
podkategorijo $\mathfrak{T}$ kategorije topoloških prostorov, zaprto za odprte
vložitve in končne produkte. _Yonedova vložitev_
$\mathsf{y}{}\colon\mathfrak{T}\to\mathsf{Sh}(\mathfrak{T})$ je poln, zvest in
na objektih injektiven funktor; objekti in morfizmi so _predstavljivi_ , kadar
so v njeni sliki.

Smiselna izbira za $\Sigma$ je $\mathscr{C}(\text{---},\mathbf{S})$, kjer je
$\mathbf{S}$ prostor Sierpińskega.

###### Lema 50

Stabilna zaprtost je tranzitivna v $\mathsf{Sh}(\mathfrak{T})$. Posledično so
stabilne zaprte podmnožice podprostori.

###### Izrek 51

  1. 1.

Vsi predstavljivi objekti v $\mathsf{Sh}(\mathfrak{T})$ so odkriti.

  2. 2.

Objekti v $\mathsf{Sh}(\mathfrak{T})$, predstavljivi s kompaktnim topološkim
prostorom iz $\mathfrak{T}$, so kompaktni v $\mathsf{Sh}(\mathfrak{T})$.

###### Izrek 52

Naj bo $\mathfrak{T}$ skelet separabilnih metričnih prostorov.

  1. 1.

Za vsak metrični prostor $(X,d)$ iz $\mathfrak{T}$ je
$(\mathsf{y}{X},\mathsf{y}{d})$ metriziran metrični prostor v
$\mathsf{Sh}(\mathfrak{T})$.

  2. 2.

Urisonov prostor v $\mathsf{Sh}(\mathfrak{T})$ je predstavljiv (s klasičnim
Urisonovim prostorom), torej metriziran. Posledično so vsi polni metrično
separabilni prostori v $\mathsf{Sh}(\mathfrak{T})$ metrizirani.

  3. 3.

Hilbertova kocka v $\mathsf{Sh}(\mathfrak{T})$ je predstavljiva s klasično
Hilbertovo kocko in torej kompaktna. Ker so obenem realna števila
Hausdorffova, so vsi popolnoma omejeni metrični prostori v
$\mathsf{Sh}(\mathfrak{T})$ kompaktni.

## Izjava o avtorstvu

Davorin Lešnik

Spodaj podpisani Davorin Lešnik izjavljam, da je disertacija plod lastnega
študija in raziskav.

## Synthetic Topology and Constructive Metric Spaces

Davorin Lešnik