University of Ljubljana

Faculty of Mathematics and Physics

Department of MathematicsSynthetic Topology and Constructive Metric
SpacesDoctoral thesisAdvisor

Univerza v Ljubljani

Fakulteta za matematiko in fiziko

Oddelek za matematikoSintetična topologija in konstruktivni metrični
prostoriDoktorska disertacijaMentor

## Abstract

The thesis presents the subject of synthetic topology, especially with
relation to metric spaces. A model of synthetic topology is a categorical
model in which objects possess an intrinsic topology in a suitable sense, and
all morphisms are continuous with regard to it. We redefine synthetic topology
in order to incorporate closed sets, and several generalizations are made.
Real numbers are reconstructed (to suit the new background) as open Dedekind
cuts. An extensive theory is developed when metric and intrinsic topology
match. In the end the results are examined in four specific models.

Math. Subj. Class. (MSC 2010): 03F60, 18C50

Keywords:
synthetic, topology, metric spaces, real numbers, constructive

## Povzetek

Disertacija predstavi področje sintetične topologije, zlasti njeno povezavo z
metričnimi prostori. Model sintetične topologije je kategorični model, v
katerem objekti posedujejo intrinzično topologijo v ustreznem smislu, glede na
katero so vsi morfizmi zvezni. Definicije in izreki sintetične topologije so
posplošeni, med drugim tako, da vključujejo zaprte množice. Realna števila so
(zaradi sintetičnega ozadja) rekonstruirana kot odprti Dedekindovi rezi.
Obširna teorija je razvita, kdaj se metrična in intrinzična topologija
ujemata. Na koncu proučimo dobljene rezultate v štirih izbranih modelih.

Math. Subj. Class. (MSC 2010): 03F60, 18C50

Ključne besede:
sintetičen, topologija, metrični prostori, realna števila, konstruktiven

###### Contents

  1. Introduction
    1. 0.1 Acknowledgements
    2. 0.2 Overview
    3. 0.3 Terminology and Notation
  2. 1 Constructive Setting
    1. 1.1 Intuitionistic Logic
    2. 1.2 Topoi
  3. 2 Synthetic Topology
    1. 2.1 From Point-Set to Synthetic Topology
    2. 2.2 Redefinition of Basic Notions in Synthetic Topology
    3. 2.3 (Co)limits and Bases
    4. 2.4 Predicative Setting
  4. 3 Real Numbers and Metric Spaces
    1. 3.1 Real Numbers
    2. 3.2 Metric Spaces
    3. 3.3 Metric Completions
  5. 4 Metrization Theorems
    1. 4.1 The WSO Principle
    2. 4.2 Transfer of Metrization via Quotients
    3. 4.3 Transfer of Metrization via Embeddings
    4. 4.4 Consequences of Metrization
  6. 5 Models of Synthetic Topology
    1. 5.1 Classical Mathematics
    2. 5.2 Number Realizability or Russian Constructivism
    3. 5.3 Function Realizability or Brouwer’s Intuitionism
    4. 5.4 Gros Topos
  7. Povzetek v slovenskem jeziku

## Introduction

###  0.1 Acknowledgements

I would like to thank my parents for all the support over the years. This
gratitude extends to my other relatives and all my friends, too numerous to
mention.

I am grateful to the government of the Republic of Slovenia for funding my
doctoral study, and to the staff at the Institute of mathematics, physics and
mechanics for the employment and all the cooperation over the years.

I thank my roommates Sara, Samo and Vesna (not to mention the two cats Odi and
Edi) for being closest to me while I was writing this dissertation (as well as
having to endure my crankiness during this time).

Regarding the mathematical work for the thesis, I am grateful for insights and
discussions with Paul Taylor, Matija Pretnar and Martín Escardó. Matija, my
former schoolmate, was the one who introduced me to synthetic topology, and
has been a good friend and collaborator for years. Martín was the first to
explicitly define synthetic topology, and did good work on the subject; I am
thankful for his cooperation and for hosting me in Birmingham during the
finishing stage of the thesis.

Most of all I would like to thank my advisor Andrej Bauer who singlehandedly
taught me category theory, constructive mathematics and computability theory,
has been extremely friendly, supportive and helpful, has taken considerable
amount of time for discussions with me, introduced me to professional
mathematics and professional mathematicians, and for being so patient with me,
a trait which was no doubt tested numerous times. I am especially grateful for
his trust in me, and for the freedom he has given me that I needed to finish
my work. In his own thesis he wrote that he hoped to one day be as good an
advisor to his students as his had been to him; I daresay he succeeded.

###  0.2 Overview

In this introductory section we explain the title and give an overview of the
thesis.

We start by explaining the first word in the title. The ‘synthetic’ approach
to mathematics started some three decades ago with synthetic differential
geometry [32, 35, 53]. The differentials were originally thought of as
“infinitely small” quantities (infinitesimals) until it was shown that no such
real numbers (aside from the trivial case of $0$) exist. Consequently a
differential (form) nowadays means a section of a cotangent bundle, a
distinctly more complicated object. In spite of this, reasoning with
differentials as infinitesimal quantities still yields correct theorems and
formulae, physicists get numerically correct results, and even mathematicians
prefer this heuristic when dealing with differential equations (e.g. when
solving them via separation of variables). Is there a way then to explain
this, and develop mathematics of infinitely small quantities formally?

One way to do it is to change the notion of real numbers; see e.g. Robinson’s
non-standard analysis [49]. This method works, but has an unfortunate
consequence that even though differentials by themselves become simpler
(compared to the classical approach), the entire analysis becomes more
complicated since the real numbers are now more complicated objects.

An ideal solution would be if the real numbers stayed what they are (or at
least altered in a way small enough as to not make them more complicated), and
meaningful differentials still existed. As mentioned, their non-existence can
in that case be proven, but the crucial assumption is the _decidable equality_
of the reals, i.e. for all real numbers $x,y\in\mathbb{R}$, either $x=y$ or
$x\neq y$. This is a special instance of the more general _law of excluded
middle_ LEM which states that for all propositions (more precisely, their
truth values) $p$ either $p$ or the negation $\lnot{p}$ holds (“every
statement is either true or false”). The corollary is that if we want non-
trivial infinitesimals to be real numbers, we need to relinquish the use of
decidability of equality on the reals, and consequently the use of the full
LEM as well, leading us into the realm of constructive mathematics.

Models of a theory in which we have the reals with infinitesimals can be
constructed, showing that this theory is consistent. These models are
complicated though (e.g. certain kind of sheaves over differential manifolds);
what makes this approach useful is that we can forget about specific models,
reasoning instead with a different kind of axioms and logical rules of
inference, but within those working just like in the usual set theory (the new
axioms essentially capture the existence and uniqueness of a derivative of
every map from reals to reals).

The point is that when studying a certain structure (smoothness in this case),
the classical approach is to equip sets with this additional structure and
identify maps which preserve it, e.g. groups and group homomorphisms, vector
spaces and linear maps, partial order and monotone maps, topological spaces
and continuous maps, measure spaces and measurable maps, smooth manifolds and
smooth maps etc. The fact that the structure is an addition onto a set, not a
part of its intrinsic structure, brings with itself a lot of baggage — it is
not sufficient to construct a space, one must also equip it with smooth
structure (consider for example what it takes to fully define the tangent
bundle), and after constructing a map, one has to verify that it is smooth (or
if not, “smoothen” it, i.e. suitably approximate it with a smooth map).
However, within a model of synthetic differential geometry every object
(satisfying a certain _microlinearity_ property) automatically has a unique
smooth structure, and every map is automatically differentiable.

Because the structure we study is ingrained in the sets and maps themselves,
constructions and proofs simplify significantly.111For example, if
$\Delta\subseteq\mathbb{R}$ denotes the set of differentials, then the tangent
bundle on a manifold $M$ is just the set of maps from $\Delta$ to $M$, and the
projection is the evaluation at $0$. Still, by itself this merely means that
it is easier to prove a statement _within_ a synthetic model, but we don’t
know yet whether that implies anything for the classical mathematics, so part
of the synthetic approach is to also construct a bridge between them over
which synthetic proofs translate to classical ones. In practice this usually
means that a classical category is embedded into a synthetic model in such a
way that content of logical statements is (sufficiently) preserved, and thus a
synthetic theorem yields a corresponding classical one. For example, it is
very easy to prove synthetically the usual formulae for length of curves,
areas between curves etc., and this theory ensures that these proofs are good
enough.

This “synthetic approach” proves fruitful in contexts other than differential
geometry as well. Generally it consists of the following.

  * •

Identify what axioms and logic are suitable for study of a particular
structure.
This is why this is called a _synthetic_ approach: we create an artificial
framework which is specifically tailored to the studied field. The logic in
these systems is typically constructive (see Chapter 1), either because
assuming excluded middle yields a trivial special case (as for example in
synthetic topology) or because the chosen axioms falsify LEM outright (as in
the case of synthetic differential geometry).

  * •

Reason within these axioms and logic to develop the theory.
The classical definitions must be reinterpreted within the synthetic setting;
in particular, a notion might have several definitions which are classically,
but not constructively, equivalent, so it must be determined which one (if
any) is suitable synthetically. After the definitions the development of the
theory usually starts by reproving classical theorems synthetically.
Naturality and simplicity of definitions and proofs is a good indication of
how good a choice of axioms we made. If we did well, we get an immediate
payoff in simpler proofs, but it is better if the theory gives us new insight
to prove new theorems as well.

  * •

Construct models of the theory.
Since Gödel onward we know that we can expect to have many non-isomorphic
models satisfying prescribed axioms, as long as they are of any reasonable
complexity (with apologies to ultrafinitists, natural numbers are practically
a must). While inability to have an (up to isomorphism) unique (and therefore
the “right one”) model was seen detrimental to some mathematicians, this
diversity is appreciated in the synthetic approach. At the very basic level
constructing models serves to prove consistency of our chosen axioms, but it
is otherwise useful — and often insightful — to see what general theorems mean
in a specific model. Furthermore, specific models are a source of
(counter)examples as well.

  * •

Connect classical theory with synthetic one.
Validity of theorems in some odd model tells us little about the validity of
these theorems in mathematics, done by a working mathematician (usually the
classical one). Thus a method of translating proofs and validity from
synthetic to classical setting is required. Once done, the outcome is that we
can prove full classical results with simpler synthetic proofs.

The purpose of this thesis is to present the reinterpretation of the field of
_topology_ in a synthetic way, and demonstrate synthetic methods specifically
in the case of metric spaces. The last point — the transfer of synthetic
theorems to classical ones — has been done [14, 55, 45]; hints of it may also
be found in Section 5.4 in this thesis, though we won’t go into detail.
Instead we focus on the other three points. Here is the breakdown of the
thesis, together with notes which results are new.

  * •

Chapter 1 recalls the notions and methods of constructivism which serves as
background of our theory. Specifically we consider (higher-order)
intuitionistic logic, as well as its categorical models, the topoi. We recall
how number sets (natural numbers, integers, rationals, reals) are defined and
constructed within this background.

The chapter is introductory in nature (for classical mathematicians to
constructivism), and contains results which are (for constructivists) already
well-known.

  * •

Chapter 2 contains basic results in general synthetic topology.

Section 2.1 recaps basic definitions and known results, together with
motivation for them from the point of view of a classical topologist.

Section 2.2 presents my suggestion for the redefinition of synthetic topology
(in order to accommodate closed sets), and develops this theory. The
introduction of test truth values, the derivation of open and closed subsets
from them, the redefinitions, the generalization of compactness (and
overtness) to maps, the notion of condenseness, the codominance axiom,
continuity of maps with regard to synthetically closed subsets, and the
analysis of topology when open truth values are stable and form a bounded
lattice, are new.

Section 2.3 examines the topology of limits and colimits, and introduces the
notion of a basis for synthetic topology. Aside from the obvious result that
the topology of a colimit is the limit of topologies, the rest is new.

Throughout the thesis models of synthetic topology are taken to be topoi.
Section 2.4 suggests how to develop synthetic topology in a general category
(but does not go in depth). It is new.

  * •

Chapter 3 develops real numbers, metric spaces and their generalizations,
suitable for synthetic topology. It serves as the preparation for the next
chapter.

Section 3.1 is an in-depth construction of real numbers, satisfying the (for
us) crucial condition that the strict order is open in synthetic topology. The
ideas for the construction of real numbers are of course not new, but the
addition of the topological part (at least the way we do it) is. Also, the
introduction of the structure of a _streak_ , and using it for the
construction of the reals (and probably the fact that the whole detailed
construction of the reals is actually written down in one place) is new. The
set of real numbers is defined as the terminal streak, and we show that open
Dedekind cuts are its model.

Section 3.2 introduces metric, pseudometric and protometric spaces, as well as
the standard related definitions (such as metric separability). As such, most
of the content is already familiar to mathematicians. The definition of total
boundedness in the choiceless environment is new. As far as I know, usage of
protometric spaces (here they are just defined; they are actually used in
Section 4.3) is new as well.

Section 3.3 deals with completions of the spaces, defined in the previous
section. The standard constructions of completions are well known, but we
adopt them to synthetic setting. Also, the actual definition of completeness
(the terminal object in the coslice category of (pseudo)metric spaces and
dense isometries) is, as far as I know, new.

  * •

Chapter 4 examines the connection between the synthetic and metric topology,
giving sufficient (and necessary) conditions for metrization (= match between
them) for complete separable (or at least complete totally bounded) metric
spaces. It is entirely new.

Section 4.1 defines WSO, a principle closely connected to metrization, and
explores its consequences. Sections 4.2 and 4.3 prove the transfer of
metrization via sufficiently nice maps, the former via quotients, and the
latter via embeddings. As a bonus, Section 4.3 presents a constructive version
of the Urysohn space.

  * •

Chapter 5 examines the results, especially those in the previous chapter, in
specific models of synthetic topology: the classical set theory in Section
5.1, Type I computability in Section 5.2, Type II computability in Section
5.3, and gros topos in Section 5.4. It is new.

Of the new parts of the thesis, Sections 4.1, 4.2 and 5.2 are joint work with
my advisor Andrej Bauer, and Section 5.3 is entirely his work. The rest is
mine.

The text is written very linearly, and should be read in order, as nearly
every section requires the ones before. The few exceptions to this rule are
the following.

  * •

Chapter 1 can be skipped by readers already familiar with constructivism.

  * •

Section 2.4 is a detour from the main thread, and is not required later.

  * •

Section 5.4 is independent from Sections 5.2 and 5.3, and can be read before
or after them.

The required foreknowledge for the thesis is solid background in general
topology and category theory (though a good portion of the thesis can be
understood without the latter). Familiarity with logic and constructive
(reverse) mathematics is welcome.

###  0.3 Terminology and Notation

Most of the terminology and notation is standard. We present possible
exceptions and borderline cases here.

  * •

For a category $\mathbf{\underline{C}}$ we denote the family of its objects by
$\text{Obj}(\mathbf{\underline{C}})$, and the family of its morphisms by
$\text{Morph}\left(\mathbf{\underline{C}}\right)$. The domain and the codomain
of a morphism $f\in\text{Morph}\left(\mathbf{\underline{C}}\right)$ are
denoted by $\text{dom}(f)$ and $\text{cod}(f)$, respectively.

  * •

The category of sets and maps is denoted by $\mathbf{\underline{Set}}$. The
category of (classical) topological spaces and continuous maps is denoted by
$\mathbf{\underline{Top}}$.

  * •

Number sets are denoted by $\mathbb{N}$ (natural numbers), $\mathbb{Z}$
(integers), $\mathbb{Q}$ (rationals), and $\mathbb{R}$ (reals). Zero is taken
as a natural number (so $\mathbb{N}=\\{0,1,2,3,\ldots\\}$).

  * •

Subsets of number sets, obtained by comparison with a certain number, are
denoted by the suitable order sign and that number in the index. For example,
$\mathbb{N}_{<42}$ denotes the set
$\left\\{n\in\mathbb{N}\;\middle|\;n<42\right\\}=\\{0,1,\ldots,41\\}$ of all
natural numbers smaller than $42$, and $\mathbb{R}_{\geq 0}$ denotes the set
$\left\\{x\in\mathbb{R}\;\middle|\;x\geq 0\right\\}$ of non-negative real
numbers.

  * •

Intervals between two numbers are denoted by these two numbers in brackets and
in the index. Round, or open, brackets $(\ )$ denote the absence of the
boundary in the set, and square, or closed, brackets $[\ ]$ its presence; for
example ${\mathbb{N}}_{[5,10)}=\left\\{n\in\mathbb{N}\;\middle|\;5\leq
n<10\right\\}=\\{5,6,7,8,9\\}$. We specifically denote the closed unit real
interval by
$\mathbb{I}:={\mathbb{R}}_{[0,1]}=\left\\{x\in\mathbb{R}\;\middle|\;0\leq
x\leq 1\right\\}$.

  * •

The difference of sets $A$ and $B$ is denoted and defined as $A\setminus
B:=\left\\{x\in A\;\middle|\;x\notin B\right\\}$. If a set $X$ is fixed, then
a complement of its subset $A$ is denoted and defined as $A^{C}:=X\setminus
A$.

  * •

The statement $A\between B$ denotes that the sets $A$ and $B$ intersect (in
constructive terms, that their intersection is inhabited).

  * •

The set of maps from $A$ to $B$ is written as the exponential $B^{A}$.

  * •

The set of finite sequences of elements in $A$ is denoted by ${A}^{*}$.

  * •

Concatenation of sequences $a$ and $b$ is $a{{:}{:}}b$.

  * •

Given sets $A\subseteq X$, $B\subseteq Y$ and a map $f\colon X\to Y$ with the
image $\text{im}(f)\subseteq B$, the restriction of $f$ to $A$ and $B$ is
denoted by $\left.{f}\right|_{A}^{B}$. When we restrict only the domain or
only the codomain, we write $\left.{f}\right|_{A}$ and $\left.{f}\right|^{B}$,
respectively.

  * •

The empty set (categorically, the initial object) is denoted by $\emptyset$, a
singleton (the terminal object) by $\mathbf{1}$ (and its sole element by $*$),
and a two-element set (binary coproduct $\mathbf{1}+\mathbf{1}$) by
$\mathbf{2}$. In logical context we denote its elements by
$\mathbf{2}=\\{\top,\bot\\}$, and in the context of number sets by
$\mathbf{2}=\\{0,1\\}$.

  * •

The onto maps are called surjective, and the one-to-one maps injective. This
should not be confused with injectivity in the categorical sense which is used
nowhere in the thesis.

  * •

The quotient of a set $X$ by an equivalence relation $\sim$ is denoted by
$X/_{\sim}$. Its elements — the equivalence classes — are denoted by $[x]$
where $x\in X$ (i.e. if $q\colon X\to X/_{\sim}$ is the quotient map, then
$[x]:=q(x)$).

  * •

Maps $f\colon X\to Y$ and $g\colon Y\to X$ with the property $f\circ
g=\textrm{Id}_{Y}$ are called _split_ (by one another). In that case $f$ is
called a _retraction_ , and $g$ its _section_.

  * •

The topology (the set of open subsets) of $X$ is denoted by $\mathcal{O}(X)$,
and the set of closed subsets by $\mathcal{Z}(X)$.

  * •

Classically various definitions of finiteness are equivalent, but
constructively this is not so. _Finite_ in this thesis means _Kuratowski
finite_ , i.e. nullary or unary or (recursively) a binary union of finite. See
also the (equivalent) definition of finiteness in Section 1.1 after assuming
that we have the set of natural numbers. That said, we adopt the following
terminology for (co)products: by a binary (co)product we mean one indexed by
$\mathbf{2}$, a finite (co)product means indexed by $\mathbb{N}_{<n}$ for some
$n\in\mathbb{N}$, and a countable or countably infinite (co)product means it
is indexed by $\mathbb{N}$.

  * •

A lattice is called _bounded_ when it has the smallest and the largest element
(which are the nullary join and nullary meet respectively, so in other words,
a bounded lattice is a partial order with all finite meets and joins).
Similarly, a bounded meet-semilattice is the one which has the largest element
(and thus all finite meets), and a bounded join-semillatice is the one which
has the smallest element (has all finite joins).

  * •

For notation of variants of the axiom of choice see Definition 1.2.

The following symbols are introduced later in the text (we present them here
for reference):

  * •

$\Omega$: the set of truth values (Section 1.1), or the subobject classifier
in a topos (Section 1.2),

  * •

$\mathbf{T}$: a two-elements set, equipped with trivial topology (Section
2.1),

  * •

$\mathbf{S}$: the Sierpiński topological space (Section 2.1),

  * •

$\Sigma$: the Sierpiński object, or the set of open truth values (Sections 2.1
and 2.2),

  * •

$\mathrm{T}$: the set of test truth values (Section 2.2),

  * •

$\mathrm{Z}$: the set of closed truth values (Section 2.2),

  * •

$\mathbb{S}$: a (fixed) overt interpolating ring streak, used to construct the
real numbers from (Section 3.1),

  * •

$\mathbb{D}$: a (fixed) lattice ring streak which serves as the set of
possible distances in a metric space (Sections 3.2 and 4.3),

  * •

$d_{E}$: the Euclidean metric (Section 3.2),

  * •

$d_{D}$: the discrete metric (Section 3.2),

  * •

$\mathbb{B}$: the Baire space, i.e. the metric space $\mathbb{N}^{\mathbb{N}}$
with the comparison metric $d_{C}$ (Chapter 4),

  * •

$\mathbb{C}$: the Cantor space, i.e. the metric space
$\mathbf{2}^{\mathbb{N}}$ with (the restriction of) the comparison metric
(Chapter 4),

  * •

$\mathbb{N}^{\bullet}$: the “one-point compactification” of $\mathbb{N}$, the
metric space of decreasing binary sequences, equipped with (the restriction
of) the comparison metric (Chapter 4),

  * •

succ, pred: the successor and predecessor map on $\mathbb{N}^{\bullet}$
(Chapter 4),

  * •

$\mathfrak{T}$: the site of topological spaces over which gros topos is made
(Section 5.4).

A few more words about style.

  * •

Most of the thesis (when the writer is the subject) is written in first person
plural (as is usual in mathematical texts), but occasionally I use first
person singular. The former is used more formally (and when I expect the
reader to go along with and except what is written), whereas the latter is
used when I want to express my personal style, opinion, preference or
suggestion.

  * •

A crossed-out relation always denotes just the negation of that relation, as
opposed to some constructively stronger notion. For example, $x\neq y$ means
$\lnot(x=y)$ while the stronger apartness relation is denoted by
$x\mathrel{\\#}y$.

  * •

Given a map $a\colon N\to A$ where $N$ is a subset of natural numbers, we
often write simply $a_{k}$ instead of $a(k)$ for the value of $a$ at $k\in N$.

  * •

In mathematical practice definitions typically follow the pattern that a term
is defined to be equivalent to something having some property, so
mathematically the phrase “if and only if” or similar should be used in
definitions. It is tedious to always write this, and often doesn’t sound
natural, so in practice mathematicians usually write simply “if”. This means
equivalence in definitions, but merely an implication everywhere else, and
this discrepancy bothers me. Therefore I use the word “when” in definitions;
it’s a single word, and has the connotation of equivalence.

  * •

A statement is often identified with its truth value. Consequently I use the
equivalence $\iff$ and equality $=$ between statements/truth values
interchangeably.

  * •

I often speak about _the_ (co)limit (for example, _the_ terminal object) and
other categorical constructions, though this is not strictly correct since
uniqueness of these constructions is only up to isomorphism, and that is how
this definite article should be understood (the same way as we say _the_ set
of natural numbers, and so on); but see also the explanation in Section 1.2
about these constructions being functors.

  * •

I don’t always go into excruciating detail about foundational issues, and am
willing to write a statement which for example quantifies over all
sets222Technically one can do this if using classes, but definitely not in an
internal language in a topos., especially if this makes the subject
conceptually clearer. It is assumed that the reader possesses enough
mathematical experience to translate such a statement to an unobjectionable
formal mathematical form. For example, Theorem 2.2 states that $X$ is compact
if and only if every projection $X\times Y\to Y$ is closed. While this looks
like quantification over all topological spaces $Y$, one implication should be
understood in a schematic sense (we have one theorem for every $Y$), and from
the proof it is clear that we only require a _set_ of topological spaces for
the other implication.

  * •

In the Elephant [26], the “Bible of topos theory”, Peter Johnstone mentions
(only half-jokingly, I think) that one of the most difficult issues in topos
theory is to decide on the plural of ‘topos’. One possibility is the form
‘topoi’, following the Greek etymology, and the other is the anglicized
version ‘toposes’. Johnstone himself argues for the latter option, saying,
among other things, that “when going for walks in the country you don’t carry
hot refreshments in ‘thermoi”’. I confess I have yet to hear someone say
‘thermoi’ myself, but then again I haven’t heard anyone say ‘thermoses’
either. Regardless, for both patterns of plural there are other words in
English which follow one or the other, so I would say that neither is
incorrect as such, and that this is more a matter of preference and style.
Personally I prefer the form ‘topoi’, for the simple reason that I find it
more euphonic. (This is, of course, just the English problem; for example in
my (Slovenian) language there is (mercifully) no such issue.)

##  Chapter 1 Constructive Setting

In this chapter we review the notions of constructivism, intuitionistic logic
and topoi which will serve as background theory in the thesis. This is meant
to be an introduction to (and motivation for) constructivism for a classical
mathematician; a constructive mathematician can skip the chapter entirely. We
focus on themes which we actually require; for a deeper (and more formal)
exposition on the subject see [57, 58].

Constructive mathematics is, very vaguely put, the method of doing mathematics
in such a way that to prove the existence of something, it is actually
constructed rather than merely proving the impossibility of non-existence. A
classical mathematician considers the latter to be good enough due to the law
of excluded middle (abbrev. LEM) which states that every proposition is either
true or false; thus if it cannot be false, it must be true. However, this does
not actually specify an instance of the object in question, and so might not
be good enough in practice (for example, a physicist might find it useless to
know that a solution of his differential equation exists if he does not also
have a way to construct it).

Constructivist movement originated from philosophical issues (most notably by
Brouwer), but has since developed into a full-fledged mathematical theory.
Generally a mathematical theory consists of specifying the language, logical
inference rules, and axioms. Most mathematicians (at the time of this writing,
at least) work within the classical set theory, with ZFC axioms [23].
Constructively some of the axioms and inference rules are omitted (definitely
LEM, though it need not be the only one), and possibly some others added.
Which ones those are depends on the type of constructive mathematics one does;
there are many different versions of constructivism [7]. For our purposes
intuitionistic logic will serve.

Intuitionism is a version of constructive mathematics which has the same
language and inference rules as classical mathematics, with the exception of
law of excluded middle; this logic is called _intuitionistic_. The axioms are
mostly the same, the main difference is the lack of the axiom of choice since
it implies LEM.

###  1.1 Intuitionistic Logic

Let $\Omega$ denote the set of truth values. Classically there are exactly two
truth values, _true_ $\top$ and _false_ $\bot$, so
$\Omega=\mathbf{2}=\\{\top,\bot\\}$. Indeed, this is precisely the law of
excluded middle: every truth value is either true or false.

Intuitionistically we still have truth and falsehood, so
$\mathbf{2}\subseteq\Omega$, but we do not require this inclusion to be
surjective (in full generality we do not require it not to be surjective
either, so classical logic is a special case of intuitionistic one).

Classically if a map is not surjective, there is a point outside its image
which in our case would mean that intuitionistically there is a third truth
value, different from $\top$ and $\bot$. But this is provably false: there is
no such value. Rather, one should view all truth values in intuitionistic
$\Omega$ to be to some extent true (i.e. equal to $\top$), and to some extent
false (equal to $\bot$), but none of them completely different from both
$\top$ and $\bot$.

Models of such a $\Omega$ are complete Heyting lattices. A _Heyting lattice_
is a bounded distributive lattice (the largest element is $\top$, the smallest
is $\bot$, the infimum is conjunction $\land$, the supremum disjunction
$\lor$) with implication $\Rightarrow$, defined to be the right adjoint to
conjuntion in the partial order $\leq$ of the Heyting lattice, viewed as a
category. Because the only isomorphisms in a partial order category are
identities, this condition determines the implication uniquely; spelling it
out, for $p,q\in\Omega$ the implication $p\Rightarrow q$ is the unique element
of $\Omega$ which satisfies the condition that $x\leq p\Rightarrow q$
precisely when $x\land p\leq q$. Dropping the categorical jargon for a moment,
in a (shall we say) normal language this means that $p\Rightarrow q$ is the
largest truth value for which the condition111This is of course the well-known
_modus ponens_. $p\land(p\Rightarrow q)\leq q$ holds. Consequently a complete
distributive lattice is automatically a (complete) Heyting lattice: $\top$ and
$\bot$ are the nullary infimum and supremum respectively, and the implication
is

$p\Rightarrow q\ =\ \bigvee\left\\{x\in\Omega\;\middle|\;p\land x\leq
q\right\\}.$

In any Heyting lattice the negation of $p\in\Omega$ can be defined as $p$
being false. However since clearly always $\bot\Rightarrow p$, the negation
can be given as $\lnot{p}:=p\Rightarrow\bot$. Consequently $p\land\lnot{p}$ is
false (a contradiction) just as in classical logic, and indeed $\lnot{p}$ is
the largest such truth value, but $\lnot{p}$ is still not a complement of $p$
in a classical sense since $p\lor\lnot{p}$ need not hold (again, this is just
LEM for $p$). When it does, $p$ is called _decidable_ (since $p\lor\lnot{p}$
means precisely that we can decide whether $p$ is true or false).

In the same vein, the double negation of a truth value need not imply that
truth value (if something is not false, it need not automatically be true);
those $p\in\Omega$ for which it does, i.e. $\lnot\lnot{p}\Rightarrow p$, are
called _$\lnot\lnot$ -stable_ (or just _stable_). The existence statements are
often not stable; the impossibility of non-existence of an object with some
property does not mean we can actually find such an object. The converse,
$p\Rightarrow\lnot\lnot{p}$ still always holds though; if something is true,
it cannot be false.

Decidable truth values are also stable. The converse need not hold; it is
equivalent to the _weak law of excluded middle_ WLEM which states
$\lnot\lnot{p}\lor\lnot{p}$ for all $p\in\Omega$. However, all truth values
are stable if and only if all of them are decidable; in that case $\Omega$ is
a (classically familiar) _Boolean lattice_.

A short intermezzo to clarify a point. Constructing an intuitionistic (or any
other, for that matter) model means constructing it in some ambient theory
(“meta-theory”), typically set theory. Reasoning within it is called
_external_ since it is outside the constructed model. But this model has a
logic on its own, and reasoning within it is called _internal_. Validity of
(syntactically) the same propositions may differ in the two interpretations.
For example, any complete Heyting lattice is the set of truth values of some
intuitionistic model, viewed externally, but most Heyting lattices have at
least three distinct elements. However, the point is that internally this is
not the case for $\Omega$ since the truth value of equality can be measured by
all elements in $\Omega$. This is even more pronounced in case $\Omega$ is a
Boolean lattice: internally it then has precisely two elements.

Just as classically one can reason intuitionistically by natural deduction. It
is an exercise in intuitionistic logic to show that the following holds for
all $p,q,r\in\Omega$ and $\phi\in\Omega^{X}$. Where there is only an
implication between the left and the right side, the converse does not hold in
general (as opposed to classical logic).

$p\Rightarrow(q\Rightarrow r)\ =\ (p\land q)\Rightarrow
r\qquad\qquad\lnot\lnot\lnot{p}\ =\ \lnot{p}\qquad\qquad\lnot\lnot(p\land q)\
=\ \lnot\lnot{p}\land\lnot\lnot{q}$ $\lnot{p}\land\lnot{q}\ =\ \lnot(p\lor
q)\qquad\qquad\lnot{p}\lor\lnot{q}\implies\lnot(p\land q)$
$\forall\,x\,{\in}\,X\,.\,\lnot\phi(x)\ =\
\lnot\exists\,x\,{\in}\,X\,.\,\phi(x)\qquad\qquad\exists\,x\,{\in}\,X\,.\,\lnot\phi(x)\implies\lnot\forall\,x\,{\in}\,X\,.\,\phi(x)$
$\lnot(p\Rightarrow q)\ =\ \lnot(\lnot p\lor q)\ =\
\lnot\lnot{p}\land\lnot{q}$ $\lnot\lnot(p\Rightarrow q)\ =\
p\Rightarrow\lnot\lnot{q}\ =\ \lnot\lnot{p}\Rightarrow\lnot\lnot{q}\ =\
\lnot{q}\Rightarrow\lnot{p}$

Let
${\Omega}_{\lnot\lnot}:=\left\\{p\in\Omega\;\middle|\;\lnot\lnot{p}=p\right\\}$
be the set of stable truth values, and let
$\lnot{A}:=\left\\{\lnot{p}\;\middle|\;p\in A\right\\}$ for
$A\subseteq\Omega$. We see that

$\mathbf{2}\subseteq{\Omega}_{\lnot\lnot}=\lnot\Omega=\lnot\lnot\Omega\subseteq\Omega.$

Suppose we have a subset $A\subseteq X$. In classical mathematics (where
$\Omega=\\{\top,\bot\\}$) we can define its _characteristic map_
$\chi_{A}\colon X\to\Omega$ by

$\chi_{A}(x):=\begin{cases}\top&\text{ if }x\in A,\\\ \bot&\text{ if }x\notin
A.\end{cases}$

But this just means that $x\in X$ maps to the truth value of its membership in
$A$, so we can define the characteristic map constructively as well by
$\chi_{A}(x):=(x\in A)$. In fact, any map $\chi\colon X\to\Omega$ is a
characteristic map of some subset of $X$, namely $\chi^{-1}(\top)$. This
defines a bijective correspondence between the powerset $\mathcal{P}(X)$ and
the set of characteristic maps (or predicates, if you will) $\Omega^{X}$.

An interesting special case is obtained by taking $X=\mathbf{1}$ since
$\Omega^{\mathbf{1}}\cong\Omega$. This means that truth values are in
bijective correspondence with subsets of a singleton (a truth value being the
measure to which extent the unique element $*\in\mathbf{1}$ belongs to a
subset). Explicitly, the bijections from one to the other are

$\displaystyle\Omega$ $\displaystyle\to\mathcal{P}(\mathbf{1})$
$\displaystyle\mathcal{P}(\mathbf{1})$ $\displaystyle\to\Omega$ $\displaystyle
p$ $\displaystyle\mapsto\left\\{*\in\mathbf{1}\;\middle|\;p\right\\},$
$\displaystyle A$ $\displaystyle\mapsto*\in A.$

We will often identify truth values and subsets of $\mathbf{1}$ via this
bijection.

The Heyting lattice structure of $\Omega$ induces the Heyting lattice
structure on $\Omega^{X}$ for all $X$ simply by exponentiation. On the level
of powersets, conjunction $\land$ induces the intersection $\cap$, disjunction
$\lor$ induces the union $\cup$, and negation $\lnot$ induces the
complementation $\text{---}^{C}$. We will also require the implication
$\Rightarrow$ on powersets; in analogy with curving the tip in the case of
conjunction and disjunction to obtain the induced operations, we’ll use the
symbol $\mathop{==\raisebox{0.94722pt}{\text{\scriptsize$)$}}}$ for the
implication on powersets.

Technically every powerset $\mathcal{P}(X)$ has its own intersection and
union, so it would be more precise to write something like $\cap_{X}$,
$\cup_{X}$. However, this is not the mathematical practice since the
intersection and union are “independent” of the superset in which we calculate
it, in the sense that if $X\subseteq Y$, then
$\mathcal{P}(X)\subseteq\mathcal{P}(Y)$, and the intersection and union of
$\mathcal{P}(Y)$ restrict to these operations on $\mathcal{P}(X)$. This is not
so in the case of the implication, so we diligently add the superset in the
index. Explicitly, for $A,B\subseteq X$ we define

$A\mathop{==\raisebox{0.94722pt}{\text{\scriptsize$)$}}_{X}}B:=\left\\{x\in
X\;\middle|\;x\in A\implies x\in B\right\\}.$

Because negative statements are $\lnot\lnot$-stable, they behave much like
classical statements; “they have the same content” classically and
constructively. For example, the definition (and meaning) of a subset being
empty is the same in both interpretations. Positive (more precisely, the
existence) statements have different content, though. For example, being non-
empty is not the same as actually possessing an element. Constructively if a
(sub)set contains an element, it is called _inhabited_. For example, non-empty
subsets of $\mathbf{1}$ are all those, represented by truth values
$p\in\Omega$ for which $\lnot\lnot{p}$ holds, but the only inhabited subset of
$\mathbf{1}$ is $\mathbf{1}$ (represented by $\top$). The two cases match if
and only if LEM holds.

The equality on a set $X$ is a map of the form $=\colon X\times X\to\Omega$.
When its image is contained in $\mathbf{2}$ (i.e. for every $x,y\in X$ the
statement $x=y$ is decidable), we say that $X$ _has decidable equality_.
Similarly, when its image is contained in ${\Omega}_{\lnot\lnot}$, we say that
$X$ _has stable equality_. Clearly if a set has decidable/stable equality, so
does its every subset. In a binary coproduct membership to an individual
summand is by definition decidable, so if summands have decidable/stable
equality, so does the binary coproduct. Obviously $\mathbf{1}$ has decidable
equality (it is always true), and then so do $\emptyset$ and $\mathbf{2}$.

As classically, so also constructively we call a set $\mathbb{N}$ the _set of
natural numbers_ when it satisfies Peano axioms. It can be proven by induction
that the relations $=$, $\leq$, $<$ on $\mathbb{N}$ are decidable.

We call a set $X$ _finite_ when there exists a surjective map
$\mathbb{N}_{<n}\to X$ for some $n\in\mathbb{N}$, i.e. we can enumerate the
elements of $X$ with the first few natural numbers. Note that the empty set
$\emptyset$ is finite by this definition since we can take $n=0$. In fact, any
finite set is either empty or inhabited; consider any surjection
$\mathbb{N}_{<n}\to X$, and decide whether $n$ equals or is greater than $0$.

If we fix a surjection $a\colon\mathbb{N}_{<n}\to X$, we can write a finite
set as $X=\\{a_{0},a_{1},\ldots,a_{n-1}\\}$ . However, in this list some
elements can potentially repeat since we only require $a$ to be a surjection,
not a bijection. Therefore, contrary to the classical intuition, for a finite
set $X$ there need not exist $n\in\mathbb{N}$ such that $X$ would have exactly
$n$ elements (in the sense that there is a bijection between $X$ and
$\mathbb{N}_{<n}$). In fact, this happens precisely when $X$ has decidable
equality (since in that case we can remove the repetitions of elements in the
list).222Some authors reserve the word ‘finite’ only for sets in bijection
with $\mathbb{N}_{<n}$ while what we call finite they term _finitely
enumerated_. Our definition of finiteness is equivalent to Kuratowski
finiteness.

Next, we call a set $X$ _infinite_ when there exists an injective map
$\mathbb{N}\to X$. Clearly if a set is infinite, it is also inhabited, and if
it contains an infinite subset, it is itself infinite. The dual notion, the
existence of a surjection $\mathbb{N}\to X$, means we have an enumeration of
elements of $A$ by natural numbers. Thus we might be tempted to call it
countability, but it turns out to be more convenient to include into
definition not necessarily inhabited sets (in particular, we want the empty
set $\emptyset$ to be countable). The general definition is: a set $X$ is
_countable_ when there exists a surjective map $\mathbb{N}\to\mathbf{1}+X$
(equivalently, when $X$ is an image of a decidable subset of natural numbers).
However, inhabitedness of $X$ is the only issue here; there is a surjection
$\mathbb{N}\to X$ if any only if $X$ is both inhabited and countable. In fact,
given a surjection $s\colon\mathbb{N}\to\mathbf{1}+X$ for such an $X$, there
is a canonical way of producing a surjection $\mathbb{N}\to X$: compose $s$
with the identity on $X$, plus map $*\in\mathbf{1}$ to the first element from
$X$ which $s$ enumerates.

Any finite set is countable; given a surjection $a\colon\mathbb{N}_{<n}\to X$,
we can produce the surjection $s\colon\mathbb{N}\to\mathbf{1}+X$ by

$s_{k}:=\begin{cases}a_{k}&\text{ if }k<n,\\\ *&\text{ if }k\geq
n.\end{cases}$

In the same vein, any decidable subset $D$ of a countable set $X$ is countable
since we can adjust the surjection $f\colon\mathbb{N}\to\mathbf{1}+X$ to
obtain the surjection $g\colon\mathbb{N}\to\mathbf{1}+D$, defined by

$g_{n}:=\begin{cases}f_{n}&\text{ if }f_{n}\in D,\\\ *&\text{ if }f_{n}\notin
D.\end{cases}$

Classically, if we have both an injection and a surjection from one set to
another, they must be in bijective correspondence. Constructively this does
not hold in general, but one special case in which it does is rather useful.

###### Lemma 1.1

If an infinite countable set has decidable equality, it is in bijection with
$\mathbb{N}$ (the converse obviously also holds). More precisely, if $X$ is an
infinite set with decidable equality, and a surjection
$s\colon\mathbb{N}\to\mathbf{1}+X$ is given, then there exists a canonical
choice of a bijection $\mathbb{N}\to X$.

###### Proof.

Define $b$ inductively as follows: $b(n)$ is the first element of $X$ in the
list $s_{0},s_{1},s_{2},\ldots$ which differs from all elements $b(k)$ for
$k\in\mathbb{N}_{<n}$. Decidable equality enables us to actually decide
whether the elements differ (and of course we use decidability of summands
$\mathbf{1}$ and $X$ to see whether an element is in $X$ in the first place).
Infiniteness of $X$ ensures that we can always find a candidate for $b(n)$. ∎

We specifically emphasize the existence of a bijective correspondence between
$\mathbb{N}$ and $\mathbb{N}\times\mathbb{N}$. A possible bijection
$\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ is $(n,m)\mapsto
2^{n}\cdot(2m+1)-1$. By induction $\mathbb{N}$ is in bijective correspondence
with $\mathbb{N}^{n}$ for any $n\in\mathbb{N}_{\geq 1}$.

Intuitionistically the axiom of choice AC is not assumed since it implies the
excluded middle. To see this, note that AC implies that every surjection is
split (indeed, AC is equivalent to this), i.e. has a section (and the
surjection is a retraction). For an arbitrary $p\in\Omega$ define a surjection
$f\colon\mathbf{2}\to\\{\top,p\\}$ by $f(\top):=\top$ and $f(\bot):=p$ (in
short, $f(x):=p\lor x$). If $f$ has a section
$s\colon\\{\top,p\\}\to\mathbf{2}$ which is necessarily injective, then
$\\{\top,p\\}$ has decidable equality because $\mathbf{2}$ does. This means
that $p$ is either equal to true or not. Since $p$ was arbitrary, we infer
LEM.

That said, weaker versions of the axiom of choice might still hold in an
intuitionistic model (even if it is non-classical). We introduce the following
notation.

###### Definition 1.2

  * •

For a set $A$ and a map $g\colon X\to Y$ the axiom $\text{{AC}}(A,g)$ means
that every map $f\colon A\to Y$ lifts along $g$ to some map $\bar{f}\colon
A\to X$ (meaning $g\circ\bar{f}=f$).

  * •

For sets $X$, $Y$ the axiom $\text{{AC}}(X,Y)$ means that every total relation
between elements of $X$ and elements of $Y$ has a choice function; spelling it
out,

$\forall\,R\,{\in}\,\mathcal{P}(X\times
Y)\,.\,\Big{(}\forall\,x\,{\in}\,X\,.\,\exists\,y\,{\in}\,Y\,.\,(x,y)\in
R\implies\exists\,f\,{\in}\,Y^{X}\,.\,\forall\,x\,{\in}\,X\,.\,(x,f(x))\in
R\Big{)}.$

Denoting by $p\colon X\times Y\to X$ the projection, this is equivalent to
$\left.{p}\right|_{R}\colon R\to X$ being split for every total relation
$R\subseteq X\times Y$ which is moreover equivalent to
$\text{{AC}}(X,\left.{p}\right|_{R}\colon R\to X)$ for every total relation
$R\subseteq X\times Y$.

  * •

For a set $X$ the axiom schema $\text{{AC}}(X)$ means that $\text{{AC}}(X,Y)$
holds for all sets $Y$.

  * •

The full axiom of choice AC (more precisely, the axiom schema) means that
$\text{{AC}}(X)$ holds for all sets $X$.

We also use a restricted version of these axioms. For $\Sigma\subseteq\Omega$
we define the axiom $\text{{AC}}_{\Sigma}(X,Y)$ to mean that every total
relation $R\subseteq X\times Y$, classified by $\Sigma$ (meaning that the
characteristic map of $R$ has the image in $\Sigma$), has a choice
function.333Later $\Sigma$ will denote the set of open truth values, so this
axiom will ensure choice functions for open relations. In particular
$\text{{AC}}(X,Y)=\text{{AC}}_{\Omega}(X,Y)$. The schemata
$\text{{AC}}_{\Sigma}(X)$ and $\text{{AC}}_{\Sigma}$ are derived as above.

Clearly in any of these axioms we can replace a set with one in a bijective
correspondence, and still obtain an equivalent axiom. More generally, the
following proposition holds.

###### Proposition 1.3

Suppose $\text{{AC}}_{\Sigma}(X,Y)$ holds for some $\Sigma\subseteq\Omega$.

  1. 1.

If $f\colon Y\to Y^{\prime}$ is a surjection, then
$\text{{AC}}_{\Sigma}(X,Y^{\prime})$ also holds.

  2. 2.

If $f\colon X\to X^{\prime}$ is a retraction (split by a section $s\colon
X^{\prime}\to X$), then $\text{{AC}}_{\Sigma}(X^{\prime},Y)$ also holds.

###### Proof.

  1. 1.

If $R\subseteq X\times Y^{\prime}$ is a total relation, classified by
$\Sigma$, then $(\textrm{Id}_{X}\times f)^{-1}(R)$ is also a total relation
(since $f$ is surjective), classified by $\Sigma$ (its characteristic map is
the characteristic map of $R$, precomposed by $\textrm{Id}_{X}\times f$). If
$g\colon X\to Y$ is a choice function for $(\textrm{Id}_{X}\times f)^{-1}(R)$,
then $f\circ g\colon X\to Y^{\prime}$ is a choice function for $R$.

  2. 2.

Similarly as in the previous item, if $R\subseteq X\times Y^{\prime}$ is a
total relation, classified by $\Sigma$, then
$(f\times\textrm{Id}_{Y})^{-1}(R)$ is also a total relation, classified by
$\Sigma$. From a choice function $g\colon X\to Y$ of
$(f\times\textrm{Id}_{Y})^{-1}(R)$ we obtain then a choice function for $R$ as
$g\circ s\colon X^{\prime}\to Y$.

∎

It can be proven by induction that $\text{{AC}}(\mathbb{N}_{<n})$ holds for
all $n\in\mathbb{N}$; this is called _finite choice_ (this does not mean that
$\text{{AC}}(X)$ holds for all finite sets $X$; indeed that would imply LEM,
as above). Many constructivists assume _countable choice_
$\text{{AC}}(\mathbb{N})$, or at least _number-number choice_
$\text{{AC}}(\mathbb{N},\mathbb{N})$. However we want to be as general as
possible, so whenever we assume any choice that does not automatically444To be
precise, we accept choice principles which automatically hold in a _topos_.
Beside finite choice we thus also silently assume the _axiom of unique choice_
(stating that for any $X$, $Y$, any relation $R\subseteq X\times Y$ which
satisfies $\forall\,x\,{\in}\,X\,.\,\exists!\,y\,{\in}\,Y\,.\,(x,y)\in R$ is a
graph of some map), something which some constructivists don’t. hold, we state
this explicitly.

We also mention a stronger version of countable choice, called _dependent
choice_. It states that we can obtain a sequence of elements by choosing one
from every set in a sequence of inhabited sets, even when each set (and the
choice of an element from it) depends on the previously chosen elements.

An important role in this thesis will be played by _semidecidable_ truth
values, i.e. countable joins of decidable ones.555Here we adopt the definition
of semidecidability for our purposes. In general, semidecidable statements are
those for which there exists an algorithm which returns ‘true’ when the
statement holds, and runs forever when it doesn’t. In (for example) Type I
computability the truth values of such statements are precisely countable
joins of decidable truth values. It is this property that will be important
for us, hence the change in the definition. More precisely, we denote and
define the set of semidecidable truth values as666In the context of number
sets we denote $\mathbf{2}=\\{0,1\\}$ instead of $\mathbf{2}=\\{\top,\bot\\}$,
and then
$\Sigma^{0}_{1}=\left\\{p\in\Omega\;\middle|\;\exists\,\alpha\,{\in}\,\mathbf{2}^{\mathbb{N}}\,.\left(p\iff\exists\,n\,{\in}\,\mathbb{N}\,.\,\alpha_{n}=0\right)\right\\}$.
Depending on style some switch $0$ with $1$ in this definition.

$\Sigma^{0}_{1}:=\left\\{p\in\Omega\;\middle|\;\exists\,\alpha\,{\in}\,\mathbf{2}^{\mathbb{N}}\,.\left(p\iff\exists\,n\,{\in}\,\mathbb{N}\,.\,\alpha_{n}\right)\right\\}.$

The notation $\Sigma^{0}_{1}$ comes from logic and recursion theory, as part
of the arithmetical hierarchy.

A subset is _semidecidable_ when it is classified by (a characteristic map
with its image in) $\Sigma^{0}_{1}$. It is obvious that countable and
semidecidable subsets of $\mathbf{1}$ match. Because of finite choice this is
true for all sets $\mathbb{N}_{<n}$ as well. As for $\mathbb{N}$, its any
countable subset is also semidecidable; if $A\subseteq\mathbb{N}$ and
$s\colon\mathbb{N}\to\mathbf{1}+A$ is a surjection, then for any
$m\in\mathbb{N}$ we have

$m\in A\iff\exists\,n\,{\in}\,\mathbb{N}\,.\,s_{n}=m$

(this works since the equality on $\mathbf{1}+\mathbb{N}$ is decidable). The
converse requires some amount of countable choice, though. Let
$\mathbf{2}^{\mathbb{N}}\twoheadrightarrow\Sigma^{0}_{1}$ denote the standard
surjection $\alpha\mapsto\exists\,n\,{\in}\,\mathbb{N}\,.\,\alpha_{n}$.

###### Proposition 1.4

The following statements are equivalent.

  1. 1.

Every semidecidable subset of $\mathbb{N}$ is countable (so semidecidable and
countable subsets of $\mathbb{N}$ match).

  2. 2.

$\text{{AC}}(\mathbb{N},\mathbf{2}^{\mathbb{N}}\twoheadrightarrow\Sigma^{0}_{1})$
holds.

###### Proof.

  * •

$(1\Rightarrow 2)$
Take any map $f\colon\mathbb{N}\to\Sigma^{0}_{1}$. This is then a
characteristic map of a semidecidable, hence countable, subset
$f^{-1}(\top)\subseteq\mathbb{N}$, so there exists a surjection
$s\colon\mathbb{N}\to\mathbf{1}+f^{-1}(\top)$. Define the lifting
$\bar{f}\colon\mathbb{N}\to\mathbf{2}^{\mathbb{N}}$ as

$\bar{f}(m)_{n}:=(s_{n}=m).$

  * •

$(2\Rightarrow 1)$
Let $A\subseteq\mathbb{N}$ be semidecidable. By
$\text{{AC}}(\mathbb{N},\mathbf{2}^{\mathbb{N}}\twoheadrightarrow\Sigma^{0}_{1})$
its characteristic map $\chi_{A}\colon\mathbb{N}\to\Sigma^{0}_{1}$ lifts to a
map $\bar{\chi}_{A}\colon\mathbb{N}\to\mathbf{2}^{\mathbb{N}}$. Let
$f\colon\mathbb{N}\times\mathbb{N}\to\mathbf{2}$ be its transposition, and
$b=(b_{0},b_{1})\colon\mathbb{N}\to\mathbb{N}\times\mathbb{N}$ a bijection. A
surjection $s\colon\mathbb{N}\to\mathbf{1}+A$ can be defined as

$s(n):=\begin{cases}b_{0}(n-1)&\text{ if }n\geq 1\text{ and }f(b(n-1)),\\\
*&\text{ otherwise.}\end{cases}$

∎

In general in constructive mathematics not all semidecidable truth values are
decidable; the statement that they are is called the _lesser principle of
omniscience_ (abbr. LPO). Explicitly, LPO is defined as

$\forall\,\alpha\,{\in}\,\mathbf{2}^{\mathbb{N}}\,.\,\big{(}\exists\,n\,{\in}\,\mathbb{N}\,.\,\alpha_{n}\lor\forall\,n\,{\in}\,\mathbb{N}\,.\,\lnot\alpha_{n}\big{)}.$

It is an instance of excluded middle, equivalent to the statement that the set
of binary sequences $\mathbf{2}^{\mathbb{N}}$ has decidable equality.

We continue the discussion about number sets. From natural numbers we can
construct the integers $\mathbb{Z}$ as formal differences of natural numbers,

$\mathbb{Z}=\mathbb{N}\times\mathbb{N}/_{\sim}\qquad\text{where}\quad(a,b)\sim(c,d)\iff
a+d=b+c,$

and rationals $\mathbb{Q}$ as formal quotients of integers,

$\mathbb{Q}=\mathbb{Z}\times(\mathbb{Z}\setminus\\{0\\})/_{\sim}\qquad\text{where}\quad(a,b)\sim(c,d)\iff
a\cdot d=b\cdot c,$

as usual. Since $\mathbb{N}\times\mathbb{N}$ is countable, so are $\mathbb{Z}$
and $\mathbb{Q}$, and clearly they are infinite with decidable equality, so
they are in bijection with $\mathbb{N}$ by Lemma 1.1.

The real numbers are more complicated. Classically there are many possible
definitions and constructions which are not constructively equivalent, so the
question arises which one to take. The two most common are the _Cauchy reals_
$\mathbb{R}_{c}$ and the _Dedekind reals_ $\mathbb{R}_{d}$.

The Cauchy reals are defined as the set of all Cauchy sequences of rational
numbers, quotiented out by the usual equivalence relation of “approaching the
same point”. Constructively, a Cauchy sequence is more that just the sequence
with the Cauchy property; we need to also supply the _modulus of convergence_
which is a rule how quickly the terms of the sequence get close together. The
Cauchy reals are popular among constructivists who assume countable choice
$\text{{AC}}(\mathbb{N})$ since then they behave “the same” as the classical
reals do; in fact even the modulus of convergence can be extracted with
countable choice from the Cauchy condition (though in practice constructivists
often prescribe the modulus of convergence in advance, and take only those
sequences which satisfy it). Without countable choice however the Cauchy reals
need not even be Cauchy complete (i.e. not all Cauchy sequences of reals
necessarily have a limit in reals) [40].

In a choiceless environment the Dedekind reals $\mathbb{R}_{d}$ prove better
behaved. They are defined as the set of all Dedekind cuts of rationals. A pair
$(L,U)\in\mathcal{P}(\mathbb{Q})\times\mathcal{P}(\mathbb{Q})$ is a _Dedekind
cut_ when $L$ is a _lower cut_ , $U$ is an _upper cut_ (which means
$\forall\,q\,{\in}\,\mathbb{Q}\,.\left(q\in
L\iff\exists\,x\,{\in}\,\mathbb{Q}_{>q}\,.\,x\in L\right)$ and
$\forall\,r\,{\in}\,\mathbb{Q}\,.\left(r\in
U\iff\exists\,x\,{\in}\,\mathbb{Q}_{<r}\,.\,x\in U\right)$, respectively), and
$L$, $U$ are inhabited, disjoint and _located_ which means
$\forall\,q,r\,{\in}\,\mathbb{Q}\,.\left(q<r\implies q\in L\lor r\in
U\right)$. The idea is that $(L,U)$ represents the unique real number such
that $L$ is the set of all smaller rationals, and $U$ is the set of all larger
rationals.

In general $\mathbb{R}_{c}\subseteq\mathbb{R}_{d}$; in the presence of
$\text{{AC}}(\mathbb{N})$ the two notions match, though.

We return to (and go more in depth into) this subject in Section 3.1.

###  1.2 Topoi

There are many equivalent definitions of topoi, the most concise one probably
being that they are categories with finite limits and powerobjects. We opt for
just a slightly longer definition.

###### Definition 1.5

A _topos_ is a category which has:

  * •

all finite limits,

  * •

all exponentials,777A category with finite limits and exponentials is called
_cartesian closed_ , so we can also say that a topos is a cartesian closed
category with a subobject classifier.

  * •

a subobject classifier.

We’ll assume familiarity with limits and exponentials888Just the intuition:
the exponential $B^{A}$ is an object of the category which represents (all)
morphisms from the object $A$ to the object $B$., but we’ll say something
about the subobject classifier. In a category with finite limits the object
$\Omega$, together with the so-called _truth map_
$\top\colon\mathbf{1}\to\Omega$, is a _subobject classifier_ when for every
monomorphism $f\colon A\to X$ in the category there exists a unique morphism
(the _characteristic map_ of $f$) $\chi\colon X\to\Omega$ such that the
following diagram is a pullback (i.e. $f$ is a pullback of the truth map along
$\chi$).

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathord{!}_{A}}$$\scriptstyle{f}$$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\chi}$$\textstyle{\Omega}$

This means that we have bijective correspondence between subobjects999Recall
that categorically a subobject of $X$ is an equivalence class of monomorphisms
with codomain $X$ where two such monos $f\colon A\to X$, $g\colon B\to X$ are
equivalent when they factor through each other via isomorphism, i.e. there
exists an isomorphism $h\colon A\to B$ such that $f=g\circ h$. of $X$ and maps
from $X$ to $\Omega$ (one direction is the definition of the subobject
classifier — hence it gets its name — and the other is the existence of
pullbacks), so we can view $\Omega$ as the “object of truth values”, and maps
$X\to\Omega$ as characteristic maps of subobjects of $X$, or predicates on
$X$. Furthermore, the exponential $\Omega^{X}$, representing predicates on
$X$, is the categorical powerobject of $X$ (intuitively, it represents the set
of subsets of $X$).

The categorical constructions, as is usually the case, are determined up to
isomorphism. However, in practice we require more than just their existence;
we need a canonical way of constructing them, so that they become functors
(for example, binary product in a category $\mathbf{\underline{C}}$ is a
functor
$\times\colon\mathbf{\underline{C}}\times\mathbf{\underline{C}}\to\mathbf{\underline{C}}$).
In case our background theory is classical with global choice (the axiom of
choice for classes), there is no problem, but constructively being functors is
a stronger assumption (see also [26]). For our purposes whenever we say that a
category has (a certain type of) limits, colimits, exponentials etc., we mean
it in the strong sense, that we have actual functors (and consequently, we can
also speak about _the_ product, and so on).

Beside the constructions from the definition, a topos also has all finite
colimits. The rigorous proof can be found in [41, 26], but the intuition is
simple. In any cartesian closed category $\mathbf{\underline{C}}$, for any
object $A\in\text{Obj}(\mathbf{\underline{C}})$ the exponentiation functor
$A^{\text{---}}\colon\mathbf{\underline{C}}\to\mathbf{\underline{C}}^{\mathrm{op}}$
is left adjoint to its opposite functor
$A^{\text{---}}\colon\mathbf{\underline{C}}^{\mathrm{op}}\to\mathbf{\underline{C}}$,
and as such preserves colimits. In other words, viewing it as a contravariant
functor, it maps colimits to limits. For $A=\Omega$ this means that a powerset
of a colimit is a limit of powersets, and if we can construct what ought to be
the powerset of an object in question, we should be able to reconstruct the
object in question up to isomorphism (it is the subset of singletons in the
powerset).

Since the domain of the truth map is the terminal object, it is a split mono,
and hence a regular mono; the following is an equalizer diagram.

$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top}$$\textstyle{\Omega\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top\circ\mathord{!}_{\Omega}}$$\scriptstyle{\textrm{Id}_{\Omega}}$$\textstyle{\Omega}$

A pullback of a regular mono is a regular mono, so in a category with a
subobject classifier (in particular in a topos) every mono is
regular.101010Even if in a category not all monos are regular, it might still
have $\Omega$ (and a truth map) which classifies all regular monos; this is
then called a _regular subobject classifier_. Moreover, it turns out that
every epimorphism is regular as well, and that every morphism has a unique
epi-mono factorization. Explicitly, for $f\colon X\to Y$, first form a
pullback

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{0}}$$\scriptstyle{p_{1}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{Y,}$

then a pushout

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{0}}$$\scriptstyle{p_{1}}$$\scriptstyle{q}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{1}}$$\scriptstyle{f}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{0}}$$\scriptstyle{f}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{Y.}$

The diagonal pushout map $q$ turns out to be epi, and the map $i$, induced by
the universal property of a pushout, is mono; it represents the inclusion of
the image of $f$ into the codomain.

Topoi have many different viewpoints [26]; for us they are important because
they are precisely categorical models of (higher-order) intuitionistic logic
which is to say that standard statements involving sets, relations, maps and
logical connectives all have the interpretation in the internal language of a
topos [41, 26], and they satisfy expected conditions. Thus working inside a
topos and doing intuitionistic mathematics amounts to the same thing. Later
models of synthetic topology will be topoi, but we’ll avoid heavy-duty
category theory by simply reasoning within intuitionistic set theory111111
_Bounded_ set theory, to be precise — i.e. no global $\in$, and all
quantifiers are bounded. (in particular, objects of the topos will be simply
called sets, and so on).

Here we recall only which morphisms in a topos represent logical connectives
and (unparameterized) quantifiers.

  * •

Truth is represented, not surprisingly, by the truth map
$\top\colon\mathbf{1}\to\Omega$; equivalently, it is the characteristic map of
$\textrm{Id}_{\mathbf{1}}$.

  * •

Falsehood $\bot\colon\mathbf{1}\to\Omega$ is the characteristic map of
$\emptyset\to\mathbf{1}$.

  * •

Conjunction $\land\colon\Omega\times\Omega\to\Omega$ is the characteristic map
of $(\top,\top)\colon\mathbf{1}\to\Omega\times\Omega$.

  * •

Make a pushout diagram of the truth map with itself.

$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\textstyle{\Omega\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\top,\textrm{Id}_{\Omega})}$$\textstyle{\Omega\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\textrm{Id}_{\Omega},\top)}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{\Omega\times\Omega}$

The inclined morphisms are to be understood in the sense
$\mathbf{1}\times\Omega\cong\Omega\cong\Omega\times\mathbf{1}$. The induced
map $i$ turns out to be mono, and disjunction
$\lor\colon\Omega\times\Omega\to\Omega$ is its characteristic map.

  * •

Let $p_{0}\colon\Omega\times\Omega\to\Omega$ be the projection onto the first
factor, and make the following equalizer.

$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\textstyle{\Omega\times\Omega\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\land}$$\scriptstyle{p_{0}}$$\textstyle{\Omega}$

Then the implication $\Rightarrow\colon\Omega\times\Omega\to\Omega$ is the
characteristic map of $e$.

  * •

Negation $\lnot\colon\Omega\to\Omega$ can in principle be calculated from
$\Rightarrow$ and $\bot$, but a simpler way to obtain it is as the
characteristic map of the falsehood map $\bot\colon\mathbf{1}\to\Omega$.

  * •

Equivalence is, of course, just the equality
$=\colon\Omega\times\Omega\to\Omega$ (which is the characteristic map of the
diagonal
$\Delta_{\Omega}=(\textrm{Id}_{\Omega},\textrm{Id}_{\Omega})\colon\Omega\to\Omega\times\Omega$).

  * •

Universal quantification on an object $X$ takes a predicate on $X$ and returns
a truth value which measures the extent to which the predicate holds overall;
thus it is a map $\forall_{X}\colon\Omega^{X}\to\Omega$. By
definition121212The more general definition allows parameters in which case a
quantifier is a map $\Omega^{X\times Y}\to\Omega^{Y}$, defined similarly, but
we won’t need its explicit construction. it is the right adjoint to the
_weakening_ $\Omega\to\Omega^{X}$, defined as the transpose of the projection
$\Omega\times X\to\Omega$. It can be constructed as the characteristic map of
the transpose $\mathbf{1}\to\Omega^{X}$ of the composition $\mathbf{1}\times
X\cong
X\stackrel{{\scriptstyle\mathord{!}_{X}}}{{\longrightarrow}}\mathbf{1}\stackrel{{\scriptstyle\top}}{{\longrightarrow}}\Omega$.

  * •

Existential quantification $\exists_{X}\colon\Omega^{X}\to\Omega$ is by
definition the left adjoint to the weakening. To construct it, let
$\in\colon\Omega^{X}\times X\to\Omega$ be the transpose of
$\textrm{Id}_{\Omega^{X}}$, i.e. the evaluation map (which is in this case the
_membership predicate_ — imagine $\Omega^{X}$ as the powerset of $X$). Let $P$
be the pullback of the truth map along it.

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathord{!}_{P}}$$\scriptstyle{p}$$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top}$$\textstyle{\Omega^{X}\times
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\in}$$\textstyle{\Omega}$

Make the epi-mono factorization of $p$, composed with the projection
$q\colon\Omega^{X}\times X\to\Omega^{X}$.

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q\circ
p}$$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{\Omega^{X}}$

Then $\exists_{X}$ is the characteristic map of $i$.131313However complicated
this construction may seem, the intuition is simple. $P$ is the set of pairs
$(A,x)$ where $x\in A\subseteq X$, so the image of its projection are
precisely inhabited subsets of $X$.

We already mentioned that topoi have finite limits and colimits, but in
general they need not be complete or cocomplete, i.e. have arbitrary set-
indexed (that is to say, external) (co)limits. However, they always have all
internal ones [26]. Here is a demonstration just for products and coproducts.
Suppose $(X_{i})_{i\in I}$ is an $I$-indexed family of objects where $I$ is
itself an object of the topos. This means that this family is given by a map
$p\colon X\to I$ where $X_{i}$s are its fibers. Then the internal coproduct of
this family is just $X$ itself while the product is given internally as
$\left\\{f\in X^{I}\;\middle|\;p\circ f=\textrm{Id}_{I}\right\\}$, or
diagrammatically as the equalizer

$\textstyle{\prod_{i\in
I}X_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{I}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p^{I}}$$\scriptstyle{\widehat{\textrm{Id}_{I}}\circ\mathord{!}_{X^{I}}}$$\textstyle{I^{I}}$

where $\widehat{\textrm{Id}_{I}}\colon\mathbf{1}\to I^{I}$ is the transpose of
$\mathbf{1}\times I\cong
I\stackrel{{\scriptstyle\textrm{Id}_{I}}}{{\longrightarrow}}I$.

A topos need not possess an object of natural numbers (for example, finite
sets and maps between them form a topos). A _natural numbers object_ is
concisely defined as the initial algebra for the functor
$\text{---}+\mathbf{1}$; with more words (and not requiring anything more from
the ambient category than a terminal object), an object $\mathbb{N}$, together
with maps $z\colon\mathbf{1}\to\mathbb{N}$, $s\colon\mathbb{N}\to\mathbb{N}$,
is a natural numbers object when it is initial among the diagrams of the form
$\mathbf{1}\stackrel{{\scriptstyle
q}}{{\longrightarrow}}A\stackrel{{\scriptstyle f}}{{\longrightarrow}}A$ in the
sense that there exists a unique $u\colon\mathbb{N}\to A$ such that the
diagram

$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{z}$$\scriptstyle{\textrm{Id}_{\mathbf{1}}}$$\textstyle{\mathbb{N}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{s}$$\scriptstyle{u}$$\textstyle{\mathbb{N}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{u}$$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{A}$

commutes. The map $z$ represents the element zero while $s$ represents the
successor map. It can be seen that this universal property precisely captures
the Peano axioms (and determines natural numbers up to isomorphism). Thus in a
topos with natural numbers object other number sets can be constructed as
well, as per previous section. We also note that the object ${A}^{*}$,
representing the set of finite sequences of $A$, i.e. the internal coproduct
$\coprod_{n\in\mathbb{N}}A^{n}$, then exists (it can be constructed for
example as
${A}^{*}=\left\\{\alpha\in(\mathbf{1}+A)^{\mathbb{N}}\;\middle|\;\exists\,n\,{\in}\,\mathbb{N}\,.\,\forall\,k\,{\in}\,\mathbb{N}\,.\left(\alpha_{k}\in
A\iff k<n\right)\right\\}$).

##  Chapter 2 Synthetic Topology

In this chapter we start with the actual subject of synthetic topology. We
redefine basic topological notions in synthetic and constructive manner, and
derive elementary results. Synthetic topology is given axiomatically, but we
defer this approach to the second part of the first section, preferring to
start with an introduction from the point of view of a classical topologist.

###  2.1 From Point-Set to Synthetic Topology

Recall that in classical set theory, the subsets of a set $X$ correspond to
the characteristic maps on $X$, i.e. maps $X\to\mathbf{2}$ where
$\mathbf{2}=\\{\top,\bot\\}$ is the set of truth values. Consider what
characteristic maps classify in the category of topological spaces. There are
four possible topologies on $\mathbf{2}$:

  * •

The topology $\\{\emptyset,\mathbf{2}\\}$. This is the trivial (= indiscrete)
topology, and we will use the symbol $\mathbf{T}$ for $\mathbf{2}$ equipped
with it. Every map $X\to\mathbf{T}$ (where $X$ is a topological space) is
continuous, so maps into $\mathbf{T}$ classify subspaces111This should not be
read that $\mathbf{T}$ is the subobject classifier in
$\mathbf{\underline{Top}}$. Subspace inclusions are a rather special kind of
injective continuous maps, namely the ones with the minimal possible topology
on the domain, such that the underlying map is still continuous (this property
can be translated into categorical terms, obtaining the general notion of a
_minimal morphism_ , used also outside topology). In fact,
$\mathbf{\underline{Top}}$ cannot possibly have a subobject classifier, as not
all its monomorphism are regular. However, since regular monomorphisms in
$\mathbf{\underline{Top}}$ are precisely subspace inclusions, $\mathbf{T}$ is
a regular subobject classifier. of $X$.

  * •

The topology $\\{\emptyset,\\{\top\\},\mathbf{2}\\}$. The set $\mathbf{2}$
with this topology is called the _Sierpiński space_ , and we denote it by
$\mathbf{S}$. A map $f\colon X\to\mathbf{S}$ is continuous if and only if
$f^{-1}(\top)$ is open in $X$. As such, maps into $\mathbf{S}$ classify open
subspaces. Let $\mathcal{O}(X)$ denote the topology on $X$, and
$\mathscr{C}(X,Y)$ the set of continuous maps between spaces $X$ and $Y$. Then
we have a bijective correspondence
$\mathcal{O}(X)\cong\mathscr{C}(X,\mathbf{S})$ for every topological space
$X$.

  * •

The topology $\\{\emptyset,\\{\bot\\},\mathbf{2}\\}$. We will call this
_inverted Sierpiński space_ , and denote it by $\tilde{\mathbf{S}}$. Observe
that continuous maps into $\tilde{\mathbf{S}}$ classify the complements of
open subspaces, i.e. closed subspaces. If we denote by $\mathcal{Z}(X)$ the
set of closed subspaces of a topological space $X$, we then have the bijection
$\mathcal{Z}(X)\cong\mathscr{C}(X,\tilde{\mathbf{S}})$.

  * •

The topology $\\{\emptyset,\\{\top\\},\\{\bot\\},\mathbf{2}\\}$. This is the
discrete topology, and we shall denote $\mathbf{2}$ equipped with it again by
$\mathbf{2}$ since this is the coproduct $\mathbf{1}+\mathbf{1}$ in
$\mathbf{\underline{Top}}$. The continuous maps into $\mathbf{2}$ classify
_clopen_ (= both closed and open) subsets. Alternatively, maps
$\mathscr{C}(X,\mathbf{2})$ represent _separations_ of the space $X$, i.e.
pairs of open subsets $(U,V)$ of $X$ such that $U\cap V=\emptyset$ and $U\cup
V=X$ (a continuous map $f\colon X\to\mathbf{2}$ induces the separation
$(f^{-1}(\top),f^{-1}(\bot))$). Recall that a space is connected when it has
no non-trivial separations (no separations in which $U$ and $V$ are both
inhabited).

However, note that the spaces $\mathbf{S}$ and $\tilde{\mathbf{S}}$ are
homeomorphic via the _twist map_ which interchanges $\top$ and $\bot$, so up
to homeomorphism there are three possible topologies on any two-element set.
The most interesting is the non-extremal one — the one homeomorphic to
$\mathbf{S}$. The importance of the Sierpiński space is that it allows us to
redefine topological notions in terms of spaces (read: objects) and continuous
maps (read: morphisms), as opposed to spaces and open subsets. This makes us
view topology through categorical glasses, and beside the whole subject of
synthetic topology which emerges, we also get an immediate pay-off in
classical topology since many standard theorems acquire a simpler and more
elegant proof. One can find more exposition and details in [14] and (for those
who understand Slovene) [45]; here we give an overview.

We identify open subsets in a topological space $X$ with continuous maps
$X\to\mathbf{S}$ which we call “open predicates” on $X$ because we view
$\mathbf{S}$ as a “topological space of open truth values” in this context.
Similarly, closed subsets in $X$ are identified with “closed predicates”
$X\to\tilde{\mathbf{S}}$.

Topological properties are also reinterpreted. Recall that classically a
topological space $X$ is Hausdorff if and only if the diagonal
$\Delta_{X}\subseteq X\times X$ is a closed subset of the topological product
$X\times X$. Since elements on the diagonal are precisely those with equal
components, we can say that $X$ is Hausdorff when its equality relation is a
closed predicate.

Consider the dual version, the diagonal being open in the product. It is
easily seen that this is the case precisely for discrete topological spaces,
so we interpret discreteness as the equality being an open predicate.

One of the most important topological properties is compactness.
Interestingly, its reinterpretation can be made _simpler_ than the classical
“every open cover has a finite subcover”. We need a little preparation,
though.

Topologists, and in particular analysts, have learnt from practice that the
most useful topology on the set $\mathscr{C}(X,Y)$ is compact-open topology,
i.e. the one generated by the subbase

$\big{\\{}V(K,U)\;\big{|}\;K\text{ compact}\subseteq X,\ U\text{
open}\subseteq Y\big{\\}}$

where

$V(K,U):=\left\\{f\in\mathscr{C}(X,Y)\;\middle|\;f(K)\subseteq U\right\\}.$

Category theory provides a theoretical reason for this: if $X$ is Hausdorff
and the exponential of $X$ and $Y$ in $\mathbf{\underline{Top}}$ exists, it is
the set $\mathscr{C}(X,Y)$, equipped with compact-open topology, and even when
the exponential does not exist, this is its closest approximation.222For
general topological spaces, a better approximation is the _Isbell topology_ ,
and the best is the so-called _natural topology_. Both match the exponential
topology when it exists (and in the case of Hausdorff spaces, they match the
compact-open topology). For more on the subject see [16, 18, 39], but since
this section is meant to be merely an introduction, overview and motivation
for synthetic topology for classical topologists, we do not go into further
details, and stick to the far better known compact-open topology.

In particular, this enables us to put a natural topology on topology itself
via the bijection $\mathcal{O}(X)\cong\mathscr{C}(X,\mathbf{S})$. Similarly,
we equip the set of closed subsets with topological structure via
$\mathcal{Z}(X)\cong\mathscr{C}(X,\tilde{\mathbf{S}})$. Also note that the
twist homeomorphism between $\mathbf{S}$ and $\tilde{\mathbf{S}}$ induces a
homeomorphism
$\mathscr{C}(X,\mathbf{S})\cong\mathscr{C}(X,\tilde{\mathbf{S}})$, namely the
postcomposition with the twist map. On the level of open and closed subsets,
this homeomorphism is (in both directions) just the complementation

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
15.31252pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathcal{O}(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
35.53073pt\raise 12.53331pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-3.075pt\hbox{$\scriptstyle{U\mapsto U^{C}}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
76.8157pt\raise 3.44685pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern
39.31252pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{{\cong}}$}}}}}}}{\hbox{\kern
76.81252pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\mathcal{Z}(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
32.97473pt\raise-13.2333pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.375pt\hbox{$\scriptstyle{F^{C}\mapsfrom F}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
15.31192pt\raise-3.60619pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces.$

Let us examine the topologies on $\mathcal{O}(X)$ and $\mathcal{Z}(X)$ closer.

###### Lemma 2.1

Let $X$ be a topological space.

  1. 1.

The family $\big{\\{}V(K,\\{\top\\})\;\big{|}\;K\text{ compact}\subseteq
X\big{\\}}$ is a basis for $\mathscr{C}(X,\mathbf{S})$. Transferring this to
$\mathcal{O}(X)$, its base is $\big{\\{}\mathord{\uparrow}K\;\big{|}\;K\text{
compact}\subseteq X\big{\\}}$ where
$\mathord{\uparrow}K:=\left\\{U\in\mathcal{O}(X)\;\middle|\;K\subseteq
U\right\\}$.

  2. 2.

Similarly, the topology on $\mathscr{C}(X,\tilde{\mathbf{S}})$ is generated by
the base $\left\\{V(K,\\{\bot\\})\;\middle|\;K\text{ compact}\subseteq
X\right\\}$ which yields a base
$\big{\\{}\left\\{F\in\mathcal{Z}(X)\;\middle|\;K\cap
F=\emptyset\right\\}\;\big{|}\;K\text{ compact}\subseteq X\big{\\}}$ for
$\mathcal{Z}(X)$.

###### Proof.

  1. 1.

Denote $\mathscr{B}=\left\\{V(K,\\{\top\\})\;\middle|\;K\text{
compact}\subseteq X\right\\}$. To see that $\mathscr{B}$ is a subbasis for
$\mathscr{C}(X,\mathbf{S})$, we still have to take care of subsets of the form
$V(K,\emptyset)$ and $V(K,\mathbf{S})$, but these are either $\emptyset$ which
we can drop from the (sub)basis, or the whole $\mathscr{C}(X,\mathbf{S})$
which can also be given as $V(\emptyset,\\{\top\\})$. To see that
$\mathscr{B}$ is in fact a basis, it is sufficient to verify that binary
intersections of elements in $\mathscr{B}$ are again in $\mathscr{B}$ which is
clear since $V(K,\\{\top\\})\cap V(L,\\{\top\\})=V(K\cup L,\\{\top\\})$ (and
binary unions of compact sets are compact).

As for the basis on $\mathcal{O}(X)$, just recall the bijection
$\mathscr{C}(X,\mathbf{S})\cong\mathcal{O}(X)$.

  2. 2.

Use the previous item, as well as the fact that $\mathscr{C}(X,\mathbf{S})$
and $\mathscr{C}(X,\tilde{\mathbf{S}})$ are homeomorphic via composition with
the twist map, and $\mathcal{O}(X)$ and $\mathcal{Z}(X)$ are homeomorphic via
complementation.

∎

This now allows us to classify compact spaces; see [13], [14], [15].

###### Theorem 2.2

The following statements are equivalent for any topological space $X$.

  1. 1.

$X$ is compact.

  2. 2.

The subset $\\{X\\}$ is open in $\mathcal{O}(X)$.

  3. 3.

The subset
$\big{\\{}F\in\mathcal{Z}(X)\;\big{|}\;\exists\,x\,{\in}\,X\,.\,x\in
F\big{\\}}$ of inhabited closed subsets of $X$ is closed in $\mathcal{Z}(X)$.

  4. 4.

For any topological space $Y$ the projection $p\colon X\times Y\to Y$ is a
closed map333Recall that a map is _closed_ when its image of every closed
subset of the domain is a closed subset of the codomain..

###### Proof.

In the following items keep in mind the results of Lemma 2.1.

  * •

$(1\Rightarrow 2)$
Since $\\{X\\}=\mathord{\uparrow}X$.

  * •

$(2\Rightarrow 1)$
Because $\\{X\\}$ is an open singleton, it must be a basic set, so there
exists a compact $K\subseteq X$ such that $\mathord{\uparrow}K=\\{X\\}$. This
means that any open subset of $X$ which contains $K$ must also contain $X$
(i.e. be equal to it). Take any open cover of $X$. Then it is in particular an
open cover of $K$ for which there exists a finite subcover. Its (open) union
covers $K$, and therefore $X$ as well.

  * •

$(2\Leftrightarrow 3)$
Use the homeomorphism $\mathcal{O}(X)\cong\mathcal{Z}(X)$, given by
complementation.

  * •

$(1\Rightarrow 4)$
Take any closed set $F\in\mathcal{Z}(X\times Y)$, and any $y\in
p(F)^{C}\subseteq Y$. For each $x\in X$ there exists a product basic open
neighbourhood of $(x,y)$ in $F^{C}$, i.e. there are open subsets $U\subseteq
X$ and $V\subseteq Y$ such that $(x,y)\in U\times V\subseteq F^{C}$. The $U$s
then form an open cover of $X$ which is compact, so there exist
$(U_{0},V_{0}),\ldots,(U_{n-1},V_{n-1})$ such that
$X=\bigcup_{k\in\mathbb{N}_{<n}}U_{k}$. Then
$\bigcap_{k\in\mathbb{N}_{<n}}V_{k}$ is an open neighbourhood of $y$ in
$p(F)^{C}$. Since $y\in p(F)^{C}$ was arbitrary, $p(F)^{C}$ is open, therefore
$p(F)$ is closed.

  * •

$(4\Rightarrow 1)$
This proof follows the one in [15]. Let $\mathcal{C}\subseteq\mathcal{O}(X)$
be an open cover of $X$. We define the following topology on $\mathcal{O}(X)$:
a subset $\mathcal{U}\subseteq\mathcal{O}(X)$ is open when it is an upper set
(if $U\in\mathcal{U}$ and $U\subseteq V\in\mathcal{O}(X)$, then
$V\in\mathcal{U}$) and when for every $\mathcal{A}\subseteq\mathcal{C}$ with
properties

$\forall\,U\,{\in}\,\mathcal{C}\,.\left(U\subseteq\bigcup\mathcal{A}\implies
U\in\mathcal{A}\right)\qquad\text{and}\qquad\bigcup\mathcal{A}\in\mathcal{U}$

there exists a finite subset $\mathcal{F}\subseteq\mathcal{A}$ such that
$\bigcup\mathcal{F}\in\mathcal{U}$. It is easy to see that this is indeed a
topology on $\mathcal{O}(X)$.444Compare it with the Scott topology [18].
Notice that for every $U\in\mathcal{C}$ the set

$\mathord{\uparrow}U:=\left\\{V\in\mathcal{O}(X)\;\middle|\;U\subseteq
V\right\\}$

is open in $\mathcal{O}(X)$.

Define

$\mathcal{V}:=\left\\{(x,U)\in
X\times\mathcal{O}(X)\;\middle|\;U\in\mathcal{C}\land x\in U\right\\}.$

This is an open subset of $X\times\mathcal{O}(X)$ since every
$(x,U)\in\mathcal{V}$ has a basic product open neighbourhood
$U\times\mathord{\uparrow}U$ which is contained in $\mathcal{V}$. By
assumption the projection $p\colon X\times\mathcal{O}(X)\to\mathcal{O}(X)$ is
a closed map, so $p(\mathcal{V}^{C})^{C}$ is open in $\mathcal{O}(X)$. Since
$\mathcal{C}$ is a cover, we have $p(\mathcal{V}^{C})^{C}=\\{X\\}$, openness
of which implies compactness of $X$ (by taking $\mathcal{A}=\mathcal{C}$).

∎

###### Corollary 2.3

The following statements are equivalent for a topological space $X$.

  1. 1.

$X$ is compact.

  2. 2.

The map $\forall_{X}\colon\mathcal{O}(X)\to\mathbf{S}$, given by the following
equivalent formulations

$\forall_{X}(U):=X\subseteq U\ =\ \forall\,x\,{\in}\,X\,.\,x\in U\ =\
\begin{cases}\top&\text{if }\forall\,x\,{\in}\,X\,.\,x\in U,\\\
\bot&\text{otherwise},\end{cases}$

is continuous.

  3. 3.

The map $\exists_{X}\colon\mathcal{Z}(X)\to\tilde{\mathbf{S}}$, given by

$\exists_{X}(F):=X\between F\ =\ \exists\,x\,{\in}\,X\,.\,x\in F\ =\
\begin{cases}\top&\text{if }\exists\,x\,{\in}\,X\,.\,x\in F,\\\
\bot&\text{otherwise},\end{cases}$

is continuous.

###### Proof.

Easy from Theorem 2.2. ∎

We can interpret this corollary in the following way. The identity maps
$\mathbf{S}\to\mathbf{T}$ and $\tilde{\mathbf{S}}\to\mathbf{T}$ are injective
and continuous, and so represent subobjects of $\mathbf{T}$ in the category of
topological spaces. The maps $\forall_{X}$ and $\exists_{X}$ from the
corollary can be extended to the whole powerset of $X$ which is equipped with
the trivial topology via $\mathcal{P}(X)\cong\mathscr{C}(X,\mathbf{T})$.
Replace $\mathbf{S}$ and $\tilde{\mathbf{S}}$ with $\mathbf{T}$ in the
codomain of $\forall_{X}$ and $\exists_{X}$ as well, to ensure that the
quantifiers are continuous. We can then characterize compactness of $X$ as the
ability to restrict these maps (in the category of topological spaces) in
either of the following diagrams.

$\textstyle{\mathcal{P}(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\forall_{X}}$$\textstyle{\mathbf{T}}$$\textstyle{\mathcal{P}(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists_{X}}$$\textstyle{\mathbf{T}}$$\textstyle{\mathcal{O}(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbf{S}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{Z}(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\tilde{\mathbf{S}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

With this preparation we give the definition of synthetic topology, following
[13]. We want a model in which sufficient amount of logic can be interpreted,
and in which we have a way of defining for every object what its topological
structure is.

###### Definition 2.4

A model of _synthetic topology_ is a topos $\mathbf{\underline{\mathcal{E}}}$
with a chosen subobject $\Sigma\subseteq\Omega$, called the _Sierpiński
object_. A subobject $U\subseteq X$ in $\mathbf{\underline{\mathcal{E}}}$ is
(_intrinsically_) _open_ when its characteristic map factors through (i.e. its
image is contained in) $\Sigma$. We define (in the internal language of the
topos) the set of open subsets of $X$

$\mathcal{O}(X):=\left\\{U\in\mathcal{P}(X)\;\middle|\;U\text{ intrinsically
open in }X\right\\}$

which we call the _intrinsic topology_ of $X$.

We do not emphasize topoi as categories, however, but rather view them as
models of constructive mathematics, and develop our theory in this sense.

The idea of the Sierpiński object $\Sigma$ is, of course, that it should play
the same role in $\mathbf{\underline{\mathcal{E}}}$ as the Sierpiński space
$\mathbf{S}$ does in the case of topological spaces, in the sense that open
subsets of $X$ are classified by maps $X\to\Sigma$. It follows that the
intrinsic topology $\mathcal{O}(X)$ is isomorphic to the exponent $\Sigma^{X}$
(in the same way as $\mathcal{P}(X)$ is isomorphic to $\Omega^{X}$). The
special case $X=\mathbf{1}$ provides an interesting insight: since
$\Sigma\cong\Sigma^{\mathbf{1}}$, we can interpret $\Sigma$ as the topology on
a one-element set. Thus, in words of Martín Escardó, to equip all objects with
the topology, it is sufficient to prescribe the topology only on
$\mathbf{1}$.555This clearly shows the importance of using constructive logic
in the case of synthetic topology, as classically the only subsets of
$\mathbf{1}$ are the empty set and the whole set. Constructively, the subsets
of $\mathbf{1}$ can be a lot more diverse and interesting.

Because $\Sigma$ is a subset of $\Omega$, we can describe openness also by
truth values. The elements of $\Sigma$ are called _open truth values_. Since
the characteristic map $\chi_{U}\colon X\to\Omega$ of a subset $U\subseteq X$
is given by $\chi_{U}(x)=x\in U$, we have that $U$ is open in $X$ if and only
if for every $x\in X$ the truth value of the statement $x\in U$ is open.

Using logical description of openness, one can often prove topological
theorems in a strikingly simple way. We demonstrate this here with examples,
and provide synthetic definitions of familiar topological properties along the
way.

For start, note that in any model of synthetic topology every map $f\colon
X\to Y$ is continuous, by which we mean the usual thing, namely that
$f$-preimages of open subsets of $Y$ are open subsets of $X$. For the proof we
need only to write the definition of the preimage,

$x\in f^{-1}(U)\iff f(x)\in U$

for all $x\in X$, $U\in\mathcal{O}(Y)$. One should understand this proof as
follows: to verify that $f^{-1}(U)$ is open in $X$, we have to see that for
every $x\in X$ the truth value of $x\in f^{-1}(U)$ is open. But this is
equivalent to $f(x)\in U$ which is an open statement since by assumption $U$
is open in $Y$, therefore for every $y\in Y$, in particular $y=f(x)$, the
statement $y\in U$ is open. This is the general strategy of synthetic
topological proofs: write a statement for which we have to verify openness,
and find an equivalent statement of which openness follows from assumptions.

Discussion about compactness above suggests what the synthetic definition of
compactness should be.

###### Definition 2.5

A set $X$ is _compact_ when its universal quantifier
$\forall_{X}\colon\mathcal{P}(X)\to\Omega$ restricts to a map
$\mathcal{O}(X)\to\Sigma$.666This is almost a transcription of the
characterization of compactness below Corollary 2.3. We note however that
there is actually a difference in detail: $\mathcal{P}(X)$ for a topological
space means the powerset of its underlying set while for an object
$X\in\text{Obj}(\mathbf{\underline{\mathcal{E}}})$ it means the set of all
subobjects of $X$. The category of topological spaces
$\mathbf{\underline{Top}}$ is not a topos, but the point is that subobjects in
$\mathbf{\underline{Top}}$ are represented by arbitrary continuous injections,
rather than just subspace embeddings. This difference is nicely seen in
Section 5.4 where (a small sub-)category of topological spaces is embedded
into a topos, and there the subobjects of a representable object, represented
by subspace inclusions, are just the stable ones. The logical formulation of
this condition is that for every $U\in\mathcal{O}(X)$ the truth value of the
statement $\forall\,x\,{\in}\,X\,.\,x\in U$ is open.

It is often convenient to replace the open subsets by their characteristic
maps, i.e. open predicates. An _open predicate_ on $X$ is a map $X\to\Sigma$
(or, if you will, it is a predicate on $X$ which restricts to such a map — its
range is contained among open truth values). The open subset, given by such a
predicate $\phi$, is of course reconstructed as $\phi^{-1}(\top)$. We see that
compactness can be equivalently reformulated as follows: $X$ is compact when
for every open predicate $\phi$ on $X$ the truth value of
$\forall\,x\,{\in}\,X\,.\,\phi(x)$ is open.

With this it is easy to prove an analogue of the classical theorem that finite
products of compact topological spaces are compact.777In general, arbitrary
products of compact sets need not be compact, however (e.g. in Section 5.2 we
see that $\mathbf{2}^{\mathbb{N}}$ is not compact in the effective topos).
This should not come as a surprise, as even classically the Tychonoff theorem
[12] is equivalent to the axiom of choice.

###### Proposition 2.6

Finite products of compact sets are compact.

###### Proof.

It is sufficient to prove the preservation of compactness by nullary and
binary products.

  * •

$\mathbf{1}$ is compact
Let $\phi\colon\mathbf{1}\to\Sigma$ be an open predicate on $\mathbf{1}$. Then

$\forall\,x\,{\in}\,\mathbf{1}\,.\,\phi(x)\iff\phi(*).$

  * •

if $X$ and $Y$ are compact, then so is $X\times Y$
Let $\phi\in\Sigma^{X\times Y}$. Then

$\forall\,a\,{\in}\,X\times
Y\,.\,\phi(a)\iff\forall\,x\,{\in}\,X\,.\,\forall\,y\,{\in}\,Y\,.\,\phi(x,y).$

∎

Here is another familiar proposition from classical topology, translated to
synthetic setting.

###### Proposition 2.7

An image of a compact set is compact.

###### Proof.

Let $X$ be compact, and $f\colon X\to Y$ surjective. Then for
$\phi\in\Sigma^{Y}$ we have

$\forall\,y\,{\in}\,Y\,.\,\phi(y)\iff\forall\,x\,{\in}\,X\,.\,\phi(f(x)).$

∎

Recall from the discussion above that classically a topological space $X$ is
Hausdorff if and only if the diagonal in $X\times X$ is closed, and is
discrete when this diagonal is open. We defer the discussion of synthetic
Hausdorffness until the next section where we introduce closed subsets, but we
can say something about discreteness. Synthetically, a set $X$ is called
_discrete_ when the diagonal $\Delta_{X}$ is an open subset of $X\times X$, or
equivalently, when its characteristic map, the equality, is an open predicate.
In logical formulation this means that $X$ is discrete when for every $x,y\in
X$ the truth value of the statement $x=y$ is open.

Classically, we are more used to discreteness to mean that singletons are
open, but it is all the same.

###### Proposition 2.8

A set is discrete if and only if all its singletons are open.

###### Proof.

Because for any $x,y\in X$

$x=y\iff x\in\\{y\\}.$

∎

Let us connect the two properties we have thus far.

###### Proposition 2.9

A compact product of discrete sets is discrete.

###### Proof.

Let $(X_{i})_{i\in K}$ be a family of discrete spaces, indexed by a compact
set $K$. Then for any $x=(x_{i})_{i\in K},y=(y_{i})_{i\in K}\in\prod_{i\in
K}X_{i}$

$x=y\iff\forall\,i\,{\in}\,K\,.\,x_{i}=y_{i}.$

∎

This can be seen as a generalization of the classical fact that finite
products of discrete spaces are discrete. Classically it is difficult to say
what a “compactly indexed family” of spaces is (but see [15]), however
synthetically there is no problem, as all sets come with topology included. A
hint that this has meaning in classical topology as well is a special case of
this proposition when all factors are the same, and the product is actually an
exponential. Indeed, recall that if $K$ is compact and $X$ is discrete, then
$\mathscr{C}(K,X)$, equipped with the compact-open topology, is a discrete
space.

Actually, this proposition is just a special case of the following one since a
singleton in a product is the intersection of preimages of singletons in
individual factors via projections.

###### Proposition 2.10

  1. 1.

Let $K$ be compact and $X$ arbitrary. Then any $K$-indexed intersection of
open subsets of $X$ is open.

  2. 2.

Conversely, let $K$ be such that any $K$-indexed intersection of open subsets
of $\mathbf{1}$ is again open. Then $K$ is compact.

###### Proof.

  1. 1.

Let $(U_{i})_{i\in K}$ be a family of open subsets of $X$. Then for any $x\in
X$

$x\in\bigcap_{i\in K}U_{i}\iff\forall\,i\,{\in}\,K\,.\,x\in U_{i}.$

  2. 2.

Tautological, as the intersection of subsets of $\mathbf{1}$ matches the
universal quantifier (via identification
$\mathcal{P}(\mathbf{1})\cong\Omega$).

∎

What this proposition tells us is that a set $K$ is compact if and only if all
$K$-indexed intersections of opens are open, and that it is sufficient to
check this condition already on the singleton $\mathbf{1}$.

In classical topology finite intersections and arbitrary unions of opens are
open. We saw that synthetically the first part generalizes to the fact that
compact intersections of opens are open. What happens with unions,
synthetically? It quickly turns out that requiring arbitrary unions of opens
to be open is a far too stringent condition; indeed $\top\in\Sigma$ (which
amounts to saying that a set is always open in itself, a very reasonable
condition) would then imply $\Sigma=\Omega$, i.e. arbitrary subset is open, as
any subset $A\subseteq\mathbf{1}$ can be written as a union $A=\bigcup_{*\in
A}\mathbf{1}$.

This suggests that the dual notion of compactness, one that captures the
property which unions of opens are open, should be scrutinized.

###### Definition 2.11

A set $X$ is _overt_ when any of the following equivalent statements hold.

  * •

The existential quantifier $\exists_{X}\colon\mathcal{P}(X)\to\Omega$
restricts to $\mathcal{O}(X)\to\Sigma$.

  * •

For every open subset $U\in\mathcal{O}(X)$ the statement
$\exists\,x\,{\in}\,X\,.\,x\in U$ (i.e. the statement “$U$ is inhabited”) is
open.

  * •

For every open predicate $\phi\in\Sigma^{X}$ the statement
$\exists\,x\,{\in}\,X\,.\,\phi(x)$ (“$\phi$ attains truth”) is open.

Just as for compactness we can prove that finite products and images of overt
sets are overt. As for two further example of the duality between compactness
and overtness, recall first that classically a compact subset of a Hausdorff
space is closed, and second that a space is compact precisely when projections
along it are closed maps (Theorem 2.2).

###### Proposition 2.12

An overt subset of a discrete set is open.

###### Proof.

Let $X$ be discrete and $U\subseteq X$ overt. Then for any $x\in X$

$x\in U\iff\exists\,y\,{\in}\,U\,.\,x=y.$

Alternatively, simply view $U$ as an overt union of its (open) singletons. ∎

###### Proposition 2.13

A set $X$ is overt if and only if for every $Y$ the projection $p\colon
X\times Y\to Y$ is an open map.

###### Proof.

  * •

$(\Rightarrow)$
Let $X$ be overt and $U\subseteq X\times Y$ open. Then for any $y\in Y$

$y\in p(U)\iff\exists\,x\,{\in}\,X\,.\,(x,y)\in U.$

  * •

$(\Leftarrow)$
Define

$V:=\left\\{(x,U)\in X\times\mathcal{O}(X)\;\middle|\;x\in U\right\\};$

since $x\in U$ is an open statement, $V$ is open in $X\times\mathcal{O}(X)$.
By assumption $p(V)$ is open in $\mathcal{O}(X)$, so for every
$U\in\mathcal{O}(X)$ the statement $U\in p(V)$, or equivalently
$\exists\,x\,{\in}\,X\,.\,x\in U$, is open.

∎

The notion of overtness comes from locale theory. Locales are, roughly
speaking, spaces, given by their lattice of open subsets, rather than as a set
of points with additional structure [27]. The point-free view of topology
lends itself far better to constructive mathematics and algebra whereas for
classical topology one relies on the excluded middle and the axiom of
choice.888For example, the Tychonoff theorem [27] and the Gelfand duality [11]
can be proven for locales without using the axiom of choice. It was observed
by Joyal, Tierney, Johnstone, Sambin, Martin-Löf and others [28, 25, 51] that
stating inhabitedness (“non-emptiness in a positive way”) of a locale is a
non-trivial property, and the locales for which this could be done in a
suitable way were called _open_ because this property is equivalent to the
unique map into $\mathbf{1}$ being an open map. Needless to say, with openness
being an overloaded term, confusion arose, and Paul Taylor renamed the notion
to ‘overt’ (and developed it in the framework of his ASD999Actually there is a
certain difference between his notion of overtness and ours. We define the
existential quantifier as a map $\Omega^{X}\to\Omega$ (if we use the predicate
version, as Taylor does) which is characterized as the left adjoint of the
transpose of the projection $\Omega\times X\to\Omega$, and we call $X$ overt
when this map restricts to $\Sigma^{X}\to\Sigma$ where it is again the left
adjoint to the transpose of the projection. However Taylor works in a
framework without powersets, and so defines that $X$ is overt when the left
adjoint $\Sigma^{X}\to\Sigma$ exists. It can happen that such an adjoint on a
subset of $\Omega$ exists, but is not the restriction of the usual existential
quantifier; for example, ${\Omega}_{\lnot\lnot}$ is a complete Boolean
lattice, but in general not a sublattice of $\Omega$. Taylor assumes some
further axioms in ASD though, and it is a matter of further research whether
they ensure that both notions of overtness coincide in cases which could be
reasonably called models of both ASD and synthetic topology. [54]).

###### Proposition 2.14

A set $X$ is overt if and only if $\mathord{!}_{X}\colon X\to\mathbf{1}$ is an
open map.

###### Proof.

Since for any $U\in\mathcal{O}(X)$ we have
$\mathord{!}_{X}(U)=\left\\{*\in\mathbf{1}\;\middle|\;\exists\,x\,{\in}\,X\,.\,x\in
U\right\\}$. (Compare also with the previous proposition.) ∎

Compactness is one of the most important topological properties while
overtness is unfamiliar to all but a few classical topologists. The reason for
this is because overtness, in whatever form we choose, is satisfied by all
topological spaces. Classically, arbitrary unions of open subsets are open.
Every map into $\mathbf{1}$ is open since all subsets of $\mathbf{1}$ are
open. For every $X$ the set
$\left\\{U\in\mathcal{O}(X)\;\middle|\;\exists\,x\,{\in}\,X\,.\,x\in
U\right\\}$ is open in $\mathcal{O}(X)$ (recall Lemma 2.1, and consider the
union $\bigcup_{x\in X}\mathord{\uparrow}\\{x\\}$). A projection from a
product to one of its factors is always an open map.

Even for compactness there is an issue which is classically invisible. For a
topological space $X$, when saying that every open cover has a finite
subcover, it does not matter whether the cover is open in $X$, or in some
larger space. This is because for a subset of a topological space it is
automatically assumed that it has the subspace (also called the relative, the
inherited, or the induced) topology, in the sense that if $X\subseteq Y$ and
$U\in\mathcal{O}(X)$, then there exists an open subset $V\in\mathcal{O}(Y)$
such that $U=X\cap V$. In other words, there is no difference in saying that a
space is compact in some larger space, or compact on its own. Synthetically
such difference exists, so we introduce new definitions.

###### Definition 2.15

A subset $X\subseteq Y$ is called

  * •

_subcompact_ 101010Usually it is simply called “compact in $Y$” while if $X$
is compact in the preceding sense, it is said that it is “compact in itself”,
or “on its own”. This terminology feels unwieldy to me, and as one quickly
starts replacing “open in this and this” simply with “open”, this can lead to
confusion in the case of compactness. For this reason I suggest the term
‘subcompact’ (to mean a “subset, compact in a given larger set”). in $Y$ when
for every $U\in\mathcal{O}(Y)$ the statement $\forall\,x\,{\in}\,X\,.\,x\in U$
(i.e. $X\subseteq U$) is open (equivalently, when for every open predicate
$\phi\colon Y\to\Sigma$ the statement $\forall\,x\,{\in}\,X\,.\,\phi(x)$ is
open);

  * •

_subovert_ in $Y$ when for every $U\in\mathcal{O}(Y)$ the statement
$\exists\,x\,{\in}\,X\,.\,x\in U$ (i.e. $X\between U$) is open (equivalently,
when for every open predicate $\phi\colon Y\to\Sigma$ the statement
$\exists\,x\,{\in}\,X\,.\,\phi(x)$ is open).

We denote the set of subcompact subsets of $X$ by $\mathrm{Comp}(X)$, and the
set of subovert subsets of $X$ by $\mathrm{Overt}(X)$.

As we will promptly see, subcompactness and subovertness are weaker properties
than compactness and overtness, but they usually suffice, so it makes sense to
use them to obtain more general propositions. To give an example how this
works in practice, we generalize Proposition 2.12.

###### Proposition 2.16

A subovert subset of a discrete set is open.

###### Proof.

Let $X$ be discrete and $U\subseteq X$ subovert. Take any $x\in X$. Then

$x\in U\iff\exists\,y\,{\in}\,U\,.\,x\in\\{y\\}.$

We see that the proof is exactly the same as in Proposition 2.12, we just had
to write it in such a way that it is clear that quantification goes over $x$
belonging to a set which is open in $X$, not just in $U$. ∎

Subovert and subcompact subsets have analogous properties to the ones above
shown for overt and compact sets.

###### Proposition 2.17

  1. 1.

The image of a subovert/subcompact subset is subovert/subcompact.

  2. 2.

Finite product of subovert/subcompact subsets is subovert/subcompact.

###### Proof.

  1. 1.

Let $f\colon X\to Y$ be a map, and $A\subseteq X$ subovert/subcompact. Take
any $\phi\in\Sigma^{Y}$. We have

$\exists\,y\,{\in}\,f(X)\,.\,\phi(y)\iff\exists\,x\,{\in}\,X\,.\,\phi(f(x)),$

and similarly,

$\forall\,y\,{\in}\,f(X)\,.\,\phi(y)\iff\forall\,x\,{\in}\,X\,.\,\phi(f(x)).$

  2. 2.

We have to verify the condition for nullary and binary products. Let $\phi$ be
an open predicate on $\mathbf{1}$. Then

$\exists\,x\,{\in}\,\mathbf{1}\,.\,\phi(x)\iff\phi(*)\iff\forall\,x\,{\in}\,\mathbf{1}\,.\,\phi(x).$

Now let $\phi$ be an open predicate on $X\times Y$, and let $A\subseteq X$,
$B\subseteq Y$ be subovert/subcompact subsets. Then

$\exists\,a\,{\in}\,A\times
B\,.\,\phi(a)\iff\exists\,x\,{\in}\,A\,.\,\exists\,y\,{\in}\,B\,.\,\phi(x,y),$

and likewise

$\forall\,a\,{\in}\,A\times
B\,.\,\phi(a)\iff\forall\,x\,{\in}\,A\,.\,\forall\,y\,{\in}\,B\,.\,\phi(x,y).$

∎

The consequence of the first item is that an overt/compact set is
subovert/subcompact in any larger set (as it is the image of its inclusion).
On the other hand, it is clear from the definition that a set is overt/compact
if and only if it is subovert/subcompact in itself. In these senses
subovertness/subcompactness generalize overtness/compactness.

For overtness the (sub)overtness of a dense subset is sufficient.

###### Definition 2.18

A subset $D\subseteq X$ is _dense_ in $X$ when every inhabited
$U\in\mathcal{O}(X)$ intersects it.

###### Proposition 2.19

Suppose $D\subseteq X$ is a subovert dense subset in $X$. Then $X$ is overt.

###### Proof.

By definition

$\exists\,x\,{\in}\,X\,.\,x\in U\iff\exists\,x\,{\in}\,D\,.\,x\in U$

for every $U\in\mathcal{O}(X)$. ∎

So far we have not made any assumptions on $\Sigma$; in principle it can be an
arbitrary subset of $\Omega$. In practice we need more information than that.
One of the basic assumptions on $\Sigma$ is that it is a bounded
$\land$-subsemilattice of $\Omega$, i.e. that it is closed under finite meets
(and consequently, that any topology $\mathcal{O}(X)$ is closed under finite
intersections). This is just saying that finite sets are compact.

###### Proposition 2.20

Assume that $\Sigma$ is closed under binary meets. Then the intersection of a
subovert subset and an open subset is subovert.

###### Proof.

Let $A\subseteq X$ be subovert, and $U,V\subseteq X$ open. Then

$\exists\,x\,{\in}\,A\cap U\,.\,x\in V\iff\exists\,x\,{\in}\,A\,.\,x\in U\cap
V.$

∎

###### Corollary 2.21

If $\Sigma$ is closed under binary meets, then an open subset of an overt set
is subovert.

###### Proof.

In (the proof of) the previous proposition take $A=X$. ∎

This corollary can be seen as the dual statement to the classical proposition
that a closed subset of a compact space is compact. The proof of this
proposition actually resorts to the fact that classically ‘compactness’ and
‘subcompactness’ are the same (so a more precise statement would in fact be
that a closed subset of a compact space is subcompact). We already mentioned
that this is because we assume subsets of a topological space to be equipped
with the subspace topology, something that synthetically we generally don’t
have. We consider this issue now.

First of all recall that all maps are continuous. Consider the following
special case: let $A\subseteq X$, and denote its inclusion $i\colon
A\hookrightarrow X$. Continuity of $i$ means that for every
$U\in\mathcal{O}(X)$ the set $i^{-1}(U)$, i.e. $A\cap U$, is open in $A$. The
subset $A$ is called a subspace in $X$ when all its opens are obtained in this
way. Here is the precise definition.

###### Definition 2.22

Let $A\subseteq X$. We say that

  * •

$A$ is a _subspace_ in $X$ (or _has the subspace topology_ , inherited from
$X$) when for every $U\in\mathcal{O}(A)$ there exists $V\in\mathcal{O}(X)$
such that $U=A\cap V$;

  * •

$A$ is a _well-embedded subspace_ in $X$ when there exists a map
$e\colon\mathcal{O}(A)\to\mathcal{O}(X)$ such that $U=A\cap e(U)$ for all
$U\in\mathcal{O}(A)$.111111This terminology is taken from Escardó’s [13].
Escardó also considers two stronger notions, with $e$ being a left or a right
adjoint to $i^{-1}\colon\mathcal{O}(X)\to\mathcal{O}(A)$, but we won’t need
these conditions.

Clearly a well-embedded subspace is also a subspace (for the converse we would
in general require some choice). Examples of (well-embedded) subspaces are
retracts: if $r\colon X\to A$ is a retraction and $U\in\mathcal{O}(A)$, then
$r^{-1}(U)\in\mathcal{O}(X)$ and $U=A\cap r^{-1}(U)$. In particular,
singletons are (well-embedded) subspaces. See Chapter 5 for examples of
subsets which are not subspaces (e.g. the reals $\mathbb{R}$ having the
Euclidean topology, and the rationals $\mathbb{Q}$ the discrete topology).

###### Proposition 2.23

A subovert/subcompact well-embedded subspace is overt/compact.

###### Proof.

Let $A\subseteq X$, and let $e\colon\mathcal{O}(A)\to\mathcal{O}(X)$ witness
that $A$ is well-embedded in $X$. Take any $U\in\mathcal{O}(A)$. The
proposition follows from equivalences

$\exists\,x\,{\in}\,A\,.\,x\in U\iff\exists\,x\,{\in}\,A\,.\,x\in
e(U)\quad\text{and}\quad\forall\,x\,{\in}\,A\,.\,x\in
U\iff\forall\,x\,{\in}\,A\,.\,x\in e(U).$

∎

From this analysis we see that if we want an open subset of an overt set to be
overt, it makes sense to require that open subsets are well-embedded
subspaces. The following notion is due to Rosolini [50].

###### Definition 2.24

$\Sigma$ is a _dominance_ when $\top\in\Sigma$ and the following _dominance
axiom_ holds:

$\forall\,u\,{\in}\,\Sigma\,.\,\forall\,p\,{\in}\,\Omega\,.\,\Big{(}\big{(}u\implies(p\in\Sigma)\big{)}\implies(u\land
p)\in\Sigma\Big{)}.$

This might seem a complicated condition, but what it says is that if the part
where $p$ meets $u$ is open in $u$, then it is open; in other words, it
captures the notion of _transitivity of openness_ (subset, open in an open
subset, is open in the whole space), restricted to truth values, or subsets of
$\mathbf{1}$ if you will. Since they determine the topology on all sets, we
may wager that it is enough. Indeed, we have the following proposition.

###### Proposition 2.25

The following statements are equivalent.

  1. 1.

$\Sigma$ is a dominance.

  2. 2.

$\top\in\Sigma$ and openness is transitive.

  3. 3.

Finite sets are compact and open subsets are well-embedded subspaces.

  4. 4.

$\Sigma$ is a closed under finite meets and open subsets are subspaces.

###### Proof.

  * •

$(1\Rightarrow 2)$
We have $\top\in\Sigma$ by assumption. Let $V\subseteq U\subseteq X$ so that
$U$ is open in $X$ and $V$ is open in $U$. Take any $x\in X$. Then the
statement $x\in U$ is open, and it implies openness of $x\in V$, so by the
dominance axiom the statement $(x\in U)\land(x\in V)$ — which is just $x\in V$
— is open.

  * •

$(2\Rightarrow 3)$
We know that compactness of finite sets means that $\Sigma$ is a bounded
$\land$-subsemilattice of $\Omega$. The assumption $\top\in\Sigma$ takes care
of nullary meets. As for binary meets, take any $u,v\in\Sigma$, and view them
as open subsets of $\mathbf{1}$. Recall that continuity of inclusion
$u\hookrightarrow\mathbf{1}$ implies that $u\land v$ is open in $u$, and hence
by transitivity also open in $\mathbf{1}$.

Let now $U\subseteq X$ be an open subset. Transitivity of openness implies
that the map $e\colon\mathcal{O}(U)\to\mathcal{O}(X)$, defined by $e(V):=V$,
witnesses that $U$ is a well-embedded subspace.

  * •

$(3\Rightarrow 4)$
Immediate.

  * •

$(4\Rightarrow 1)$
We obtain $\top\in\Sigma$ because $\Sigma$ is closed under nullary meets. Take
now any $u\in\Sigma$ and $p\in\Omega$ such that $u$ implies openness of $p$.
If we interpret truth values as subsets of $\Sigma$, this amounts to saying
that $u\land p$ is an open subset of $u$, so by assumption there exists
$v\in\Sigma$ such that $u\land p=u\land v$. Because $\Sigma$ is closed under
binary meets, $u\land v$ is open, and then so is $u\land p$.

∎

###### Corollary 2.26

If $\Sigma$ is a dominance, then open subsets of overt sets are overt.

###### Proof.

By the previous proposition $\Sigma$ is closed under binary meets, and open
subsets are well-embedded subspaces. Now use Corollary 2.21 and Proposition
2.23. ∎

Results such as this corollary put a certain issue into perspective. There are
statements which hold in all models of synthetic topology (such as Proposition
2.17). Generally though we deal with statements which hold only with some
additional assumptions. One way to cope with this is to consider a specific
model of synthetic topology (we do this in Chapter 5), but when a property is
common enough, it is better to identify suitable sufficient conditions under
which we can prove it, the benefit being that this holds for a larger class of
models, and gives us a deeper insight. Such conditions are given as
_principles_ , a common occurrence in constructive mathematics. The Sierpiński
object $\Sigma$ being a dominance is one example, and there are others
scattered throughout the thesis. Here we recall just one more (and some of its
consequences); we won’t need it later, but it deserves a mention in its own
right.

###### Definition 2.27

A model of synthetic topology satisfies _Phoa’s principle_ [44] when $\Sigma$
is a bounded sublattice of $\Omega$, and for every map
$f\colon\Sigma\to\Sigma$ and $u\in\Sigma$ the condition

$f(u)=(f(\top)\land u)\lor f(\bot),\quad\text{or equivalently,}\quad
f(u)=(f(\bot)\lor u)\land f(\top),$

holds.

The Sierpiński set $\Sigma\subseteq\Omega$ can in general be arbitrarily
bizarre; Phoa’s principle states however, that it actually behaves the way the
Sierpiński space $\mathbf{S}$ does (examine the continuous maps
$\mathbf{S}\to\mathbf{S}$).

###### Proposition 2.28

If Phoa’s principle holds, then every map $\Sigma\to\Sigma$ is monotone.

###### Proof.

Take any $f\colon\Sigma\to\Sigma$ and any $u,v\in\Sigma$ such that
$u\Rightarrow v$ which is equivalent to $u\lor v=v$. By Phoa’s principle

$f(u)\lor f(v)=(f(\top)\land u)\lor f(\bot)\lor(f(\top)\land v)\lor f(\bot)=$
$=\big{(}f(\top)\land(u\lor v)\big{)}\lor f(\bot)=(f(\top)\land v)\lor
f(\bot)=f(v),$

so $f(u)\Rightarrow f(v)$. ∎

We used the $f(u)=(f(\top)\land u)\lor f(\bot)$ version of Phoa’s principle,
but the proof from $f(u)=(f(\bot)\lor u)\land f(\top)$ is analogous. This
enables us to see that the two versions are indeed equivalent since

$(f(\top)\land u)\lor f(\bot)=\big{(}f(\top)\lor
f(\bot)\big{)}\land\big{(}u\lor f(\bot)\big{)}=(f(\bot)\lor u)\land f(\top)$

because $f(\bot)\Rightarrow f(\top)$.

###### Proposition 2.29

If Phoa’s principle holds, then for any $X$ the set
$\mathcal{O}(X)\cong\Sigma^{X}$ is overt and compact (in particular, $\Sigma$
itself is overt and compact).

###### Proof.

Take any $U\in\mathcal{O}(\Sigma^{X})$ (with the characteristic map
$\chi_{U}\colon\Sigma^{X}\to\Sigma$).

Let $\psi\in U$. Define a map $g\colon\Sigma\to\Sigma^{X}$ by
$g(u)(x):=u\lor\psi(x)$, and let $f\colon\Sigma\to\Sigma$ be $f:=\chi_{U}\circ
g$. By the previous proposition $f(\bot)\Rightarrow f(\top)$, but
$f(\bot)=\chi_{U}(g(\bot))=\chi_{U}(\psi)=\top$ which means

$\top=f(\top)=\chi_{U}(g(\top))=\chi_{U}(x\mapsto\top).$

Therefore $U$ is inhabited if and only if $(x\mapsto\top)\in U$ which is an
open statement, thus proving overtness of $\Sigma^{X}$.

Assume now that $(x\mapsto\bot)\in U$, and take arbitrary $\psi\in\Sigma^{X}$.
Define $g\colon\Sigma\to\Sigma^{X}$ by $g(u)(x):=u\land\psi(x)$, and
$f\colon\Sigma\to\Sigma$ again by $f:=\chi_{U}\circ g$. We have
$f(\bot)=\chi_{U}(g(\bot))=\chi_{U}(x\mapsto\bot)=\top$ and
$f(\bot)\Rightarrow f(\top)$, so

$\top=f(\top)=\chi_{U}(g(\top))=\chi_{U}(\psi).$

So as soon as $U$ contains the characteristic map of the empty subset of $X$,
it contains all of $\Sigma^{X}$. Since $(x\mapsto\bot)\in U$ is an open
statement, $\Sigma^{X}$ is compact. ∎

We close the section by considering some examples of $\Sigma$. We restrict to
cases when $\Sigma$ is closed under finite $\land$.

  * •

$\Sigma=\Omega$
This is the largest possible $\Sigma$, and in this case every subset (and
every predicate) is open. This corresponds classically to discrete topology.
We see that every set is overt and compact, and $\Sigma$ is trivially a
dominance.

  * •

$\Sigma=\\{\top\\}$
This is the smallest possible $\Sigma$ (if we require it to contain finite, in
particular nullary, meets). In every set $X$ only $X$ itself is open. This
corresponds classically to trivial (indiscrete) topology. Every set is
compact, and precisely inhabited ones are overt. It is easily seen that this
$\Sigma$ is a dominance.

  * •

$\Sigma=\mathbf{2}$
In this case precisely decidable subsets are open, and at least finite sets
are overt and compact. This $\Sigma$, and more generally every one contained
in $\mathbf{2}$, is a dominance.

  * •

$\Sigma=\left\\{p\in\Omega\;\middle|\;\lnot{p}\lor\lnot\lnot{p}\right\\}$
This is a little relaxed previous case: open subsets are those of which
membership satisfies weak law of excluded middle (as opposed to the previous
case where it had to satisfy the full one). Consider what it means for this
$\Sigma$ to be a dominance. In this case the dominance axiom states

$\forall\,u\,{\in}\,\Sigma\,.\,\forall\,p\,{\in}\,\Omega\,.\,\Big{(}\big{(}u\implies(\lnot{p}\lor\lnot\lnot{p})\big{)}\implies\big{(}\lnot(u\land
p)\lor\lnot\lnot(u\land p)\big{)}\Big{)}.$

It is easily seen that the condition is satisfied when $\lnot{u}$. Assume now
$\lnot\lnot{u}$. Since then

$\lnot(u\land p)=\lnot\lnot\lnot(u\land
p)=\lnot(\lnot\lnot{u}\land\lnot\lnot{p})=\lnot\lnot\lnot{p}=\lnot{p},$

the dominance condition amounts to

$\forall\,u,p\,{\in}\,\Omega\,.\,\Big{(}\big{(}\lnot\lnot{u}\land\big{(}u\implies(\lnot{p}\lor\lnot\lnot{p})\big{)}\big{)}\implies(\lnot{p}\lor\lnot\lnot{p})\Big{)}.$

We see that this $\Sigma$ is a dominance if and only if the weak law of
excluded middle WLEM holds (in which case $\Sigma=\Omega$): for the left-to-
right direction take $u=(\lnot{p}\lor\lnot\lnot{p})$, and the other direction
is trivial.

  * •

$\Sigma={\Omega}_{\lnot\lnot}$
In this case the open subsets are the stable ones. (At least) finite sets are
compact, and the empty set and the singletons are overt. As for the overtness
of other finite sets, it is easy to see that the following statements are
equivalent:

    * –

$\Sigma$ is a bounded sublattice of $\Omega$,

    * –

WLEM holds,

    * –

${\Omega}_{\lnot\lnot}=\mathbf{2}$.

We also show that this $\Sigma$ is a dominance. Take any $u\in\Sigma$ and
$p\in\Omega$ such that $u\implies(p\in{\Omega}_{\lnot\lnot})$, or
equivalently, $u\land\lnot\lnot{p}\implies p$. Then

$\lnot\lnot(u\land
p)=\lnot\lnot{u}\land\lnot\lnot{p}=u\land\lnot\lnot{p}=u\land p.$

  * •

$\Sigma=\Sigma^{0}_{1}$
In this case the open subsets are the semidecidable ones, i.e. those of which
membership is in the so-called _Rosolini dominance_

$\Sigma^{0}_{1}=\left\\{u\in\Omega\;\middle|\;\exists\,\alpha\,{\in}\,\mathbf{2}^{\mathbb{N}}\,.\,\big{(}u\iff\exists\,n\,{\in}\,\mathbb{N}\,.\,\alpha_{n}=0\big{)}\right\\}.$

As the name suggests, this is indeed a dominance which was proven by Rosolini
[50]. Here is the idea of the proof. Take any $u\in\Sigma^{0}_{1}$ and
$p\in\Omega$ such that $u\implies(p\in\Sigma^{0}_{1})$. There exists
$\alpha\in\mathbf{2}^{\mathbb{N}}$ for which
$u\iff\exists\,n\,{\in}\,\mathbb{N}\,.\,\alpha_{n}=0$. We need to find
$\beta\in\mathbf{2}^{\mathbb{N}}$ such that $u\land
p\iff\exists\,n\,{\in}\,\mathbb{N}\,.\,\beta_{n}=0$. Define $\beta$ to be all
$1$s as long as the terms of $\alpha$ are $1$. If however we ever come across
a term of $\alpha$ which is $0$, then $u$ holds, so there exists
$\gamma\in\mathbf{2}^{\mathbb{N}}$ such that
$p\iff\exists\,n\,{\in}\,\mathbb{N}\,.\,\gamma_{n}=0$. We take this $\gamma$
for the rest of $\beta$.

We’ll spend a few more words about the Rosolini dominance.

###### Lemma 2.30

For any $\Sigma$ if $\mathbb{N}$ and $\emptyset$ are overt, then all countable
sets are overt.

###### Proof.

Let $X$ be countable which means we have a surjection
$\mathbb{N}\to\mathbf{1}+X$. If $\mathbb{N}$ is overt, then so is its image
$\mathbf{1}+X$. Take any $U\in\mathcal{O}(X)$ and an arbitrary
$x\in\mathbf{1}+X$. If $x\in\mathbf{1}$, then $x\in U$ equals $\bot$ which is
an open truth value because $\emptyset$ is overt. If $x\in X$, then $x\in U$
is open. We conclude that $U$ is open also in $\mathbf{1}+X$, and since

$\exists\,x\,{\in}\,X\,.\,x\in U\iff\exists\,x\,{\in}\,\mathbf{1}+X\,.\,x\in
U$

and $\mathbf{1}+X$ is overt, the result follows. ∎

###### Lemma 2.31

  1. 1.

$\Sigma^{0}_{1}$ is a bounded sublattice of $\Omega$.

  2. 2.

If $\Sigma\subseteq\Omega$ is closed under finite meets and countable joins,
then $\Sigma^{0}_{1}\subseteq\Sigma$.

  3. 3.

Assuming
$\text{{AC}}(\mathbb{N},\mathbf{2}^{\mathbb{N}}\twoheadrightarrow\Sigma^{0}_{1})$,
$\Sigma^{0}_{1}$ is closed under countable joins.

###### Proof.

  1. 1.

The nullary meet $\top$ and join $\bot$ are represented by the constant
sequences of $0$s and $1$s respectively. Now take $u,v\in\Sigma^{0}_{1}$,
represented by $\alpha,\beta\in\mathbf{2}^{\mathbb{N}}$. Then $u\land v$ is
represented by $(\sup\\{\alpha_{m},\beta_{n}\\})_{m,n\in\mathbb{N}}$
(precomposed by a bijection $\mathbb{N}\cong\mathbb{N}\times\mathbb{N}$ to
obtain a sequence), and to represent $u\lor v$, interleave $\alpha$ and
$\beta$.

  2. 2.

Since $\Sigma$ contains nullary meet and join, $\mathbf{2}\subseteq\Sigma$.
Countable joins of the decidable truth values are precisely the semidecidable
ones, so $\Sigma^{0}_{1}\subseteq\Sigma$.

  3. 3.

We already know $\bot\in\Sigma^{0}_{1}$, so by Lemma 2.30 it is sufficient to
see that $\Sigma^{0}_{1}$ is closed under $\mathbb{N}$-indexed joins. Let
$(u_{i})_{i\in\mathbb{N}}$ be a sequence of semidecidable truth values; this
gives a map $u\colon\mathbb{N}\to\Sigma^{0}_{1}$. By
$\text{{AC}}(\mathbb{N},\mathbf{2}^{\mathbb{N}}\twoheadrightarrow\Sigma^{0}_{1})$
this map lifts to $\tilde{u}\colon\mathbb{N}\to\mathbf{2}^{\mathbb{N}}$.
Transpose it and precompose with $\mathbb{N}\cong\mathbb{N}\times\mathbb{N}$
to obtain a sequence which represents $\bigvee_{i\in\mathbb{N}}u_{i}$.

∎

The consequence of this lemma is that (given sufficient countable choice)
$\Sigma^{0}_{1}$ is the smallest subset of $\Omega$ (and the smallest
dominance), closed under finite meets and countable joins.

###  2.2 Redefinition of Basic Notions in Synthetic Topology

The introduction of the Sierpiński object $\Sigma$ equips all sets with an
intrinsic topology, in the sense that it determines what open sets are (in a
natural way, i.e. all maps are continuous). However, we know from classical
topology that closed sets play an important role as well, something about
which $\Sigma$ stays silent. The question what closed subsets in synthetic
topology should be was posed by Martín Escardó in [13].

One would naturally first try the classical definition, and if that does not
work, some definitions which are classically equivalent to it. Escardó
considers the following possibilities:

  * •

a subset is closed when it contains all its adherent points ($x\in X$ is an
_adherent point_ of $A\subseteq X$ when every open set containing $x$
intersects $A$),

  * •

a subset is closed when it is the complement of an open subset,

  * •

a subset is closed when its complement is open.

He argues however that none of these options seem to suit in general. Indeed,
they don’t satisfy expected theorems, e.g. that closed subsets of compact sets
are (sub)compact (in classical analogy and analogy with Corollary 2.21), or
behave analogously to synthetically open subsets. In view of this Escardó
argues for the following definition:

  * •

a subset $F\subseteq X$ is closed in $X$ when the set
$F\mathop{==\raisebox{0.94722pt}{\text{\scriptsize$)$}}_{X}}U=\left\\{x\in
X\;\middle|\;x\in F\implies x\in U\right\\}$ is open in $X$ for every
$U\subseteq F$ open in $F$.

We will call such subsets _Escardó closed_.