A Foundation for Synthetic Stone Duality

Cherubini, Felix; Coquand, Thierry; Geerligs, Freek; Moeneclaey, Hugo

doi:10.4230/LIPIcs.TYPES.2024.3

A Foundation for Synthetic Stone Duality

Felix Cherubini

University of Gothenburg, Sweden
Chalmers University of Technology, Gothenburg, Sweden Thierry Coquand

University of Gothenburg, Sweden
Chalmers University of Technology, Gothenburg, Sweden Freek Geerligs

University of Gothenburg, Sweden
Chalmers University of Technology, Gothenburg, Sweden Hugo Moeneclaey

University of Gothenburg, Sweden
Chalmers University of Technology, Gothenburg, Sweden

Abstract

The language of homotopy type theory has proved to be an appropriate internal language for various higher toposes, for example for the Zariski topos in Synthetic Algebraic Geometry. This paper aims to do the same for the higher topos of light condensed anima of Dustin Clausen and Peter Scholze. This seems to be an appropriate setting for synthetic topology in the style of Martín Escardó.

We use homotopy type theory extended with 4 axioms. We prove Markov’s principle, LLPO and the negation of WLPO. Then we define a type of open propositions, inducing a topology on any type such that any map is continuous. We give a synthetic definition of second countable Stone and compact Hausdorff spaces, and show that their induced topologies are as expected. This means that any map from e.g. the unit interval $\mathbb{I}$ to itself is continuous in the usual epsilon-delta sense.

With the usual definition of cohomology in homotopy type theory, we show that $H^{1}(S,\mathbb{Z})=0$ for $S$ Stone and that $H^{1}(X,\mathbb{Z})$ for $X$ compact Hausdorff can be computed using Čech cohomology. We use this to prove $H^{1}(\mathbb{I}^{1},\mathbb{Z})=0$ and $H^{1}(\mathbb{S}^{1},\mathbb{Z})=\mathbb{Z}$ where $\mathbb{S}^{1}$ is the set $\mathbb{R}/\mathbb{Z}$ . As an application, we give a synthetic proof of Brouwer’s fixed-point theorem.

Keywords and phrases:

Homotopy Type Theory, Synthetic Topology, Cohomology

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Type theory

Acknowledgements:

The idea of proving Theorem 4.18 by using the topological characterization of Stone spaces as totally disconnected compact Hausdorff spaces was explained to us by Martín Escardó. We profited a lot from a discussion with Reid Barton and Johann Commelin. The fact that Markov’s principle (Corollary 1.16) holds was noticed by David Wärn. We had an interesting discussion with Bas Spitters on the topic of the article at TYPES 2024.

Funding:

ForCUTT project, ERC advanced grant 101053291.

DOI:

10.4230/LIPIcs.TYPES.2024.3

Event:

30th International Conference on Types for Proofs and Programs (TYPES 2024)

Editors:

Rasmus Ejlers Møgelberg and Benno van den Berg

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Introduction

The language of homotopy type theory consists of dependent type theory enriched with the univalence axiom and higher inductive types. It has proven exceptionnally well-suited to a synthetic development of homotopy theory [13]. It also provides a framework precise enough to analyze categorical models of type theory [20]. Moreover, arguments in this language can be represented in proof assistants rather directly. In this article we use homotopy type theory to give a synthetic development of topology, analogous to the synthetic development of algebraic geometry in [4].

We introduce four axioms inspired by the light condensed sets introduced in [5]. Interestingly, our axioms have strong connections with constructive mathematics [3], in particular constructive reverse mathematics [11, 7]. Indeed they imply several of Brouwer’s principles (e.g. any real function on the unit interval is continuous, the celebrated fan theorem), as well as not intuitionistically valid principles (Markov’s Principle, the so-called Lesser Limited Principle of Omniscience).

Our axioms also closely align with the program of Synthetic Topology [9, 12, 19, 10, 21]. Indeed we have a dominance of open propositions, so that any type comes with an induced topology. Using this induced topology, we manage to capture synthetically the notion of second-countable compact Hausdorff spaces. While working on our axioms, we learnt about [2], which provides a similar axiomatisation in extensional type theory. We show that some of their axioms are consequences of ours. For example¹¹1We can actually prove all of their axioms, from which their directed univalence follows. This will be presented in a following paper., we can define in our setting the notion of overtly discrete types, which is dual to the notion of compact Hausdorff spaces.

A central theme of homotopy type theory is that the notion of type is more general than the notion of set. We illustrate this theme in this work. Indeed we can form the types of Stone spaces and of compact Hausdorff spaces, which are not sets but rather a groupoids. Moreover these spaces are closed under $\Sigma$ -type types, which would be impossible to formulate in the traditional setting. Additionally, we can leverage higher types by using the elegant definition of cohomology groups in homotopy type theory [13]. We then prove a special case of a theorem of Dyckhoff [8] describing the cohomology of compact Hausdorff spaces. As an application, we give a synthetic proof of Brouwer’s fixed point theorem, similar to the proof of an approximated form in [16].

We expect our axioms to be validated by the interpretation of homotopy type theory into the higher topos of light condensed anima [17], although checking this rigorously is still work in progress. We even expect this to be valid in a constructive metatheory, using [6]. It is important to stress that our axioms only capture the properties of light condensed anima that are internally valid. Since David Wärn [23] has proved that an important property of condensed abelian groups is not valid internally, this means that we cannot prove it in our setting. We also conjecture that the present axiom system is complete for the properties that are internally valid.

1 Stone duality

1.1 Preliminaries

$\blacktriangleright$ Remark 1.1.

For $X$ any type, a subtype $U$ of $X$ is a family of propositions over $X$ . We write $U\subseteq X$ . If $X$ is a set, we call $U$ a subset. Given $x : X$ we sometimes write $x\in U$ instead of $U(x)$ . For subtypes $A,B\subseteq X$ , we write $A\subseteq B$ for pointwise implication. We will freely switch between a subtype $U\subseteq X$ and the corresponding embedding $\sum_{x:X}U(x)\hookrightarrow X.$ In particular, if we write $x : U$ we mean $x : X$ such that $U(x)$ .

Definition 1.2.

A type is countable if and only if it is merely equal to some decidable subset of $\mathbb{N}$ .

Definition 1.3.

For $I$ a set we write $2[I]$ for the free Boolean algebra on $I$ . A Boolean algebra $B$ is countably presented if there exist countable sets $I, J$ with generators $g:I\to B$ and relations $f:J\to 2[I]$ such that $g$ induces an equivalence between $2[I]/(f_{j})_{j:J}$ and $B$ .

$\blacktriangleright$ Remark 1.4.

Any countably presented algebra is merely of the form $2[\mathbb{N}]/(r_{n})_{n:\mathbb{N}}$ .

$\blacktriangleright$ Remark 1.5.

We denote the type of countably presented Boolean algebras by $\mathsf{Boole}_{\omega}$ . This type does not depend on a choice of universe. Moreover $\mathsf{Boole}_{\omega}$ has a natural category structure.

Example 1.6.

If both the set of generators and relations are empty, we get the Boolean algebra $2$ . Its underlying set is $\{0,1\}$ with $0\neq 1$ . We have that $2$ is initial in $\mathsf{Boole}_{\omega}$ .

Definition 1.7.

For $B$ a countably presented Boolean algebra, we define the spectrum $\operatorname{Sp}(B)$ as the set $\mathrm{Hom}(B,2)$ of Boolean morphisms from $B$ to $2$ . Any type which is merely equivalent to some spectrum is called a Stone space.

Example 1.8.

(i)

There is only one Boolean morphism from $2$ to $2$ , thus $\operatorname{Sp}(2)$ is the singleton type $\top$ .
(ii)

The trivial Boolean algebra is presented as $2/(1)$ . We have $0=1$ in the trivial Boolean algebra, so there cannot be a map from it into $2$ preserving both $0$ and $1$ . Therefore the corresponding Stone space is the empty type $\bot$ .
(iii)

The type $\operatorname{Sp}(2[\mathbb{N}])$ is called the Cantor space. It is equivalent to the set of binary sequences $2^{\mathbb{N}}$ . Given $\alpha:\operatorname{Sp}(2[\mathbb{N}])$ and $n:\mathbb{N}$ , we write $\alpha_{n}$ for $\alpha(g_{n})$ , the $n$ -th bit of the corresponding binary sequence.
(iv)

We denote by $B_{\infty}$ the Boolean algebra generated by $(g_{n})_{n:\mathbb{N}}$ quotiented by the relations $g_{m}\wedge g_{n}=0$ for ${n\neq m}$ . A morphism $B_{\infty}\to 2$ corresponds to a function $\mathbb{N}\to 2$ that hits $1$ at most once. We denote $\operatorname{Sp}(B_{\infty})$ by $\mathbb{N}_{\infty}$ . For $\alpha:\mathbb{N}_{\infty}$ and $n:\mathbb{N}$ we write $\alpha_{n}$ for $\alpha(g_{n})$ . For $n:\mathbb{N}$ , we define $n:\mathbb{N}_{\infty}$ as the unique $\alpha:\mathbb{N}_{\infty}$ such that $\alpha_{n}=1$ . We define $\infty:\mathbb{N}_{\infty}$ as the unique $\alpha:\mathbb{N}_{\infty}$ such that $\alpha_{n}=0$ for all $n:\mathbb{N}$ .

By conjunctive normal form, any element of $B_{\infty}$ can be written uniquely as $\bigvee_{i:I}g_{n}$ or as $\bigwedge_{i:I}\neg g_{n}$ for some finite $I\subseteq\mathbb{N}$ .

Lemma 1.9.

Given $\alpha:2^{\mathbb{N}}$ , we have an equivalence of propositions:

(\forall_{n:\mathbb{N}}\ \alpha_{n}=0)\leftrightarrow\operatorname{Sp}(2/(% \alpha_{n})_{n:\mathbb{N}}).

Proof.

There is only one Boolean morphism $x:2\to 2$ , and it satisfies $x(\alpha_{n})=0$ for all $n:\mathbb{N}$ if and only if $\alpha_{n}=0$ for all $n:\mathbb{N}$ . $\hfill\blacktriangleleft$

1.2 Axioms

Axiom 1 (Stone duality).

For all $B:\mathsf{Boole}_{\omega}$ , the evaluation map $B\rightarrow 2^{\operatorname{Sp}(B)}$ is an isomorphism.

Axiom 2 (Surjections are formal surjections).

For all morphism $g:B\to C$ in $\mathsf{Boole}_{\omega}$ , we have that $g$ is injective if and only if $(-)\circ g:\operatorname{Sp}(C)\to\operatorname{Sp}(B)$ is surjective.

Axiom 3 (Local choice).

For all $B:\mathsf{Boole}_{\omega}$ and type family $P$ over $\operatorname{Sp}(B)$ such that $\Pi_{s:\operatorname{Sp}(B)}\lVert P(s)\rVert$ , there merely exists some $C:\mathsf{Boole}_{\omega}$ and surjection $q:\operatorname{Sp}(C)\to\operatorname{Sp}(B)$ such that $\Pi_{t:\operatorname{Sp}(C)}P(q(t))$ .

Axiom 4 (Dependent choice).

For all types $(E_{n})_{n:\mathbb{N}}$ with surjections $E_{n+1}\twoheadrightarrow E_{n}$ for all $n:\mathbb{N}$ , the projection from the sequential limit $\lim_{k}E_{k}$ to $E_{0}$ is surjective.

1.3 Anti-equivalence of $\mathsf{Boole}_{\omega}$ and $\mathsf{Stone}$

By Axiom 1, the map $\operatorname{Sp}$ is an embedding of $\mathsf{Boole}_{\omega}$ into any universe of types. We denote its image by $\mathsf{Stone}$ .

$\blacktriangleright$ Remark 1.10.

Stone spaces will take over the role of the affine schemes from [4], so let us repeat some results here. Analogously to Lemma 3.1.2 of [4], for $X:\mathsf{Stone}$ , Axiom 1 tells us that $X=\operatorname{Sp}(2^{X})$ . Proposition 2.2.1 of [4] now says that $\operatorname{Sp}$ gives a natural equivalence

\mathrm{Hom}(A,B)=(\operatorname{Sp}(B)\to\operatorname{Sp}(A))

By the above and Lemma 9.4.5 of [13], the map $\operatorname{Sp}$ defines a dual equivalence of categories between $\mathsf{Boole}_{\omega}$ and $\mathsf{Stone}$ . In particular the spectrum of any colimit in $\mathsf{Boole}_{\omega}$ is the limit of the spectrum of the opposite diagram.

$\blacktriangleright$ Remark 1.11.

Axiom 3 can also be formulated as follows: Given $S:\mathsf{Stone}$ with $E, F$ arbitrary types, a map $f:S\to F$ and a surjection $e:E\twoheadrightarrow F$ , there exists a Stone space $T$ , a surjective map $T\twoheadrightarrow S$ and an arrow $T\to E$ making the following diagram commute:

Lemma 1.12.

For $B:\mathsf{Boole}_{\omega}$ , we have $0=_{B}1$ if and only if $\neg\operatorname{Sp}(B)$ .

Proof.

If $0=_{B}1$ , there is no map in $B\to 2$ preserving both $0$ and $1$ , thus $\neg\operatorname{Sp}(B)$ . Conversely, if $\neg\operatorname{Sp}(B)$ then $\operatorname{Sp}(B)=\bot$ . Since $\bot$ is the spectrum of the trivial Boolean algebra and $\operatorname{Sp}$ is an embedding, we conclude that $B$ is the trivial Boolean algebra, hence $0=_{B}1$ . $\hfill\blacktriangleleft$

Corollary 1.13.

For $S:\mathsf{Stone}$ , we have that $\neg\neg S\to\lVert S\rVert$

Proof.

Let $B:\mathsf{Boole}_{\omega}$ and suppose $\neg\neg\operatorname{Sp}(B)$ . By Lemma 1.12 we have that $0\not=_{B}1$ , therefore the morphism $2\to B$ is injective. By Axiom 2 the map $\operatorname{Sp}(B)\to\operatorname{Sp}(2)$ is surjective, thus $\operatorname{Sp}(B)$ is merely inhabited. $\hfill\blacktriangleleft$

1.4 Principles of omniscience

The so-called principles of omniscience are all weaker than the law of excluded middle (LEM), and help measure how close a logical system is to satisfying LEM [7, 11]. In this section, we will show that two such principles hold (MP and LLPO), and that another one fails (WLPO).

Theorem 1.14 (The negation of the weak lesser principle of omniscience ( $\neg$ WLPO)).

\neg\forall_{\alpha:2^{\mathbb{N}}}((\forall_{n:\mathbb{N}}\,\alpha_{n}=0)\vee% \neg(\forall_{n:\mathbb{N}}\,\alpha_{n}=0))

Proof.

We will prove that any decidable property of binary sequences is determined by a finite prefix of fixed length, contradicting $\forall_{n:\mathbb{N}}\,\alpha_{n}=0$ being decidable for all $\alpha$ . Indeed assume $f:2^{\mathbb{N}}\to 2$ such that $f(\alpha)=0$ if and only if $\forall_{n:\mathbb{N}}\ \alpha_{n}=0$ . By Axiom 1, there is some $c:2[\mathbb{N}]$ with $f(\alpha)=0$ if and only if $\alpha(c)=0$ . There exists $k:\mathbb{N}$ such that $c$ is expressed in terms of the generators $(g_{n})_{n\leq k}$ . Now consider $\beta,\gamma:2^{\mathbb{N}}$ given by $\beta(g_{n})=0$ for all $n:\mathbb{N}$ and $\gamma(g_{n})=0$ if and only if $n\leq k$ . As $\beta$ and $\gamma$ are equal on $(g_{n})_{n\leq k}$ , we have $\beta(c)=\gamma(c)$ . However, $f(\beta)=0$ and $f(\gamma)=1$ , giving a contradiction. $\hfill\blacktriangleleft$

Theorem 1.15.

For all $\alpha:\mathbb{N}_{\infty}$ , we have that

(\neg(\forall_{n:\mathbb{N}}\,\alpha_{n}=0))\to\Sigma_{n:\mathbb{N}}\,\alpha_{% n}=1

Proof.

By Lemma 1.9, we have that $\neg(\forall_{n:\mathbb{N}}\,\alpha_{n}=0)$ implies that $\operatorname{Sp}(2/(\alpha_{n})_{n:\mathbb{N}})$ is empty. Hence $2/(\alpha_{n})_{n:\mathbb{N}}$ is trivial by Lemma 1.12. Then there exists $k:\mathbb{N}$ such that $\bigvee_{i\leq k}\alpha_{i}=1$ . As $\alpha_{i}=1$ for at most one $i:\mathbb{N}$ , there exists a unique $n:\mathbb{N}$ with $\alpha_{n}=1$ . $\hfill\blacktriangleleft$

Corollary 1.16 (Markov’s principle (MP)).

For all $\alpha:2^{\mathbb{N}}$ , we have that

(\neg(\forall_{n:\mathbb{N}}\,\alpha_{n}=0))\to\Sigma_{n:\mathbb{N}}\,\alpha_{% n}=1

Proof.

Given $\alpha:2^{\mathbb{N}}$ , consider the sequence $\alpha^{\prime}:\mathbb{N}_{\infty}$ satisfying $\alpha^{\prime}_{n}=1$ if and only if $n$ is minimal with $\alpha_{n}=1$ . Then apply the above theorem. $\hfill\blacktriangleleft$

Theorem 1.17 (The lesser limited principle of omniscience (LLPO)).

For all $\alpha:\mathbb{N}_{\infty}$ , we have that

(\forall_{k:\mathbb{N}}\,\alpha_{2k}=0)\vee(\forall_{k:\mathbb{N}}\,\alpha_{2k% +1}=0)

Proof.

Define $f:B_{\infty}\to B_{\infty}\times B_{\infty}$ on generators as follows

f(g_{n})=\begin{cases}(g_{k},0)\text{ if }n=2k\\ (0,g_{k})\text{ if }n=2k+1\\ \end{cases}

Note that $f$ is a well-defined morphism in $\mathsf{Boole}_{\omega}$ as $f(g_{n})\wedge f(g_{m})=0$ whenever $m\neq n$ . We claim that $f$ is injective. If $I\subseteq\mathbb{N}$ , write $I_{0}=\{k\ |\ 2k\in I\},I_{1}=\{k\ |\ 2k+1\in I\}$ . Recall that any $x:B_{\infty}$ is of the form $\bigvee_{i\in I}g_{i}$ or $\bigwedge_{i\in I}\neg g_{i}$ for some finite set $I$ .

$\blacksquare$

If $x=\bigvee_{i\in I}g_{i}$ , then $f(x)=(\bigvee_{i\in I_{0}}g_{i},\bigvee_{i\in I_{1}}g_{i})$ . So if $f(x)=0$ , then $I_{0}=I_{1}=I=\emptyset$ and $x=0$ .
$\blacksquare$

Suppose $x=\bigwedge_{i\in I}\neg g_{i}$ . Then $f(x)=(\bigwedge_{i\in I_{0}}\neg g_{i},\bigwedge_{i\in I_{1}}\neg g_{i})$ , so $f(x)\neq 0$ .

By Axiom 2, we have that $f$ corresponds to a surjection $s:\mathbb{N}_{\infty}+\mathbb{N}_{\infty}\to\mathbb{N}_{\infty}$ . Thus for $\alpha:\mathbb{N}_{\infty}$ , there exists some $x:\mathbb{N}_{\infty}+\mathbb{N}_{\infty}$ such that $s(x)=\alpha$ . If $x=\mathrm{inl}(\beta)$ , then for any $k:\mathbb{N}$ we have that

\alpha_{2k+1}=s(x)_{2k+1}=x(f(g_{2k+1}))=\mathrm{inl}(\beta)(0,g_{k})=\beta(0)% =0.

Similarly, if $x=\mathrm{inr}(\beta)$ , we have that $\alpha_{2k}=0$ for all $k:\mathbb{N}$ . $\hfill\blacktriangleleft$ The surjection $s:\mathbb{N}_{\infty}+\mathbb{N}_{\infty}\to\mathbb{N}_{\infty}$ above does not have a section. Indeed:

Lemma 1.18.

The function $f$ defined above does not have a retraction.

Proof.

Suppose $r:B_{\infty}\times B_{\infty}\to B_{\infty}$ is a retraction of $f$ . Then $r(0,g_{k})=g_{2k+1}$ and $r(g_{k},0)=g_{2k}$ . Note that $r(0,1)\geq r(0,g_{k})=g_{2k+1}$ for all $k:\mathbb{N}$ . As a consequence, $r(0,1)$ is of the form $\bigwedge_{i\in I}\neg g_{i}$ for some finite set $I$ . By similar reasoning so is $r(1,0)$ . But then

r(0,1)\wedge r(1,0)=r((1,0)\wedge(0,1))=r(0,0)=0.

This is a contradiction. $\hfill\blacktriangleleft$

1.5 Open and closed propositions

Open (resp. closed) propositions are defined as countable disjunctions (resp. conjunctions) of decidable propositions. In this section we will study their logical properties.

Definition 1.19.

A proposition $P$ is open (resp. closed) if there exists some $\alpha:2^{\mathbb{N}}$ such that $P\leftrightarrow\exists_{n:\mathbb{N}}\alpha_{n}=0$ (resp. $P\leftrightarrow\forall_{n:\mathbb{N}}\alpha_{n}=0$ ). We denote by $\mathsf{Open}$ and $\mathsf{Closed}$ the types of open and closed propositions.

$\blacktriangleright$ Remark 1.20.

The negation of an open proposition is closed, and by MP (Corollary 1.16), the negation of a closed proposition is open. Moreover both open and closed propositions are $\neg\neg$ -stable. By $\neg$ WLPO (Theorem 1.14), not every closed proposition is decidable. Therefore, not every open proposition is decidable. Every decidable proposition is both open and closed.

Lemma 1.21.

We have the following:

$\blacksquare$

Closed propositions are stable under countable conjunctions and finite disjunctions.
$\blacksquare$

Open propositions are stable under countable disjunctions and finite conjunctions.

Proof.

All statements but the one about finite disjunctions have similar proofs, so we only present the proof that closed propositions are stable under countable conjunctions. Let $(P_{n})_{n:\mathbb{N}}$ be a countable family of closed propositions. By countable choice, for each $n:\mathbb{N}$ we have an $\alpha_{n}:2^{\mathbb{N}}$ such that $P_{n}\leftrightarrow\forall_{m:\mathbb{N}}\,\alpha_{n,m}=0$ . Consider a surjection $s:\mathbb{N}\twoheadrightarrow\mathbb{N}\times\mathbb{N}$ , and let $\beta_{k}=\alpha_{s(k)}.$ Note that $\forall_{k:\mathbb{N}}\,\beta_{k}=0$ if and only if $\forall_{n:\mathbb{N}}P_{n}$ .

To prove that closed propositions are closed under finite disjunctions, we use the known fact that LLPO (Theorem 1.17) is equivalent to the statement that for $P$ and $Q$ open, we have that $(\neg P\vee\neg Q)\leftrightarrow\neg(P\wedge Q)$ . We conclude using that closed propositions are negations of open propositions, and that the conjunction of two open propositions is open. $\hfill\blacktriangleleft$

From now on we will use the above properties silently.

Corollary 1.22.

If a proposition is both open and closed, then it is decidable.

Proof.

If $P$ is open and closed, then $P\vee\neg P$ is open. So it is $\neg\neg$ -stable and we conclude from $\neg\neg(P\vee\neg P)$ . $\hfill\blacktriangleleft$

Lemma 1.23.

For $(P_{n})_{n:\mathbb{N}}$ a sequence of closed propositions, we have $\neg\forall_{n:\mathbb{N}}P_{n}\leftrightarrow\exists_{n:\mathbb{N}}\neg P_{n}$ .

Proof.

Both $\neg\forall_{n:\mathbb{N}}P_{n}$ and $\exists_{n:\mathbb{N}}\neg P_{n}$ are open, hence $\neg\neg$ -stable. The equivalence follows. $\hfill\blacktriangleleft$

Lemma 1.24.

If $P$ is open and $Q$ is closed then $P\to Q$ is closed. If $P$ is closed and $Q$ open, then $P\to Q$ is open.

Proof.

Note that $\neg P\vee Q$ is closed. Using $\neg\neg$ -stability we conclude that $(P\to Q)\leftrightarrow(\neg P\vee Q)$ . The other proof is similar. $\hfill\blacktriangleleft$

1.6 Types as spaces

The subset $\mathsf{Open}$ of the set of propositions induces a topology on every type. This is the viewpoint taken in synthetic topology, from which we borrow terminology [9, 12].

Definition 1.25.

Let $T$ be a type, and let $A\subseteq T$ be a subtype. We call $A\subseteq T$ open (resp. closed) if $A(t)$ is open (resp. closed) for all $t : T$ .

$\blacktriangleright$ Remark 1.26.

It follows immediately that the pre-image of an open by any map is open, so that any map is continuous. In Theorem 3.11, we will see that the resulting topology is as expected for Stone spaces. In Lemma 4.27, we will see that the same holds for the unit interval.

2 Overtly discrete spaces

Definition 2.1.

We call a type overtly discrete if it is a sequential colimit of finite sets.

$\blacktriangleright$ Remark 2.2.

It follows from Corollary 7.7 of [18] that overtly discrete types are sets, and that the sequential colimit can be defined as in set theory. We write $\mathsf{ODisc}$ for the type of overtly discrete types.

Using dependent choice, we have the following results:

Lemma 2.3.

A map between overtly discrete sets is a sequential colimit of maps between finite sets.

Lemma 2.4.

For $f:A\to B$ a sequential colimit of maps of finite sets $f_{n}:A_{n}\to B_{n}$ , we have that the factorisation $A\twoheadrightarrow Im(f)\hookrightarrow B$ is the sequential colimit of the factorisations $A_{n}\twoheadrightarrow Im(f_{n})\hookrightarrow B_{n}$ .

Corollary 2.5.

An injective (resp. surjective) map between overtly discrete types is a sequential colimit of injective (resp. surjective) maps between finite sets.

2.1 Closure properties of $\mathsf{ODisc}$

We can get the following result using Lemma 2.3 and dependent choice.

Lemma 2.6.

Overtly discrete types are stable under sequential colimits.

We have that $\Sigma$ -types, identity types and propositional truncation commute with sequential colimits (Theorem 5.1, Theorem 7.4 and Corollary 7.7 in [18]). Then by closure of finite sets under these constructors, we can get the following:

Lemma 2.7.

Overtly discrete types are stable under $\Sigma$ -types, identity types and propositional truncations.

2.2 $\mathsf{Open}$ and $\mathsf{ODisc}$

Lemma 2.8.

A proposition is open if and only if it is overtly discrete.

Proof.

If $P$ is overtly discrete, then $P\leftrightarrow\exists_{n:\mathbb{N}}\lVert F_{n}\rVert$ with $F_{n}$ finite sets. But a finite set being inhabited is decidable, hence $P$ is a countable disjunction of decidable propositions, so it is open. Suppose $P\leftrightarrow\exists_{n:\mathbb{N}}\alpha_{n}=1$ . Let $P_{n}=\exists_{n\leq k}(\alpha_{n}=1)$ , which is a decidable proposition, hence a finite set. Then the colimit of $P_{n}$ is $P$ . $\hfill\blacktriangleleft$

Corollary 2.9.

Open propositions are stable under $\Sigma$ -types.

Corollary 2.10 (transitivity of openness).

Let $T$ be a type, let $V\subseteq T$ open and let $W\subseteq V$ open. Then $W\subseteq T$ is open as well.

$\blacktriangleright$ Remark 2.11.

It follows from Proposition 2.25 of [12] that $\mathsf{Open}$ is a dominance in the setting of Synthetic Topology.

Lemma 2.12.

A type $B$ is overtly discrete if and only if it is the quotient of a countable set by an open equivalence relation.

Proof.

If $B:\mathsf{ODisc}$ is the sequential colimit of finite sets $B_{n}$ , then $B$ is an open quotient of $(\Sigma_{n:\mathbb{N}}B_{n})$ . Conversely, assume $B=D/R$ with $D\subseteq\mathbb{N}$ decidable and $R$ open. By dependent choice we get $\alpha:D\to D\to 2^{\mathbb{N}}$ such that $R(x,y)\leftrightarrow\exists_{k:\mathbb{N}}\alpha_{x,y}(k)=1$ . Define $D_{n}=(D\cap\mathbb{N}_{\leq n})$ , and define $R_{n}:D_{n}\to D_{n}\to 2$ as the equivalence relation generated by the relation $\exists_{k\leq n}\,\alpha_{x,y}(k)=1$ . Then the $B_{n}=D_{n}/R_{n}$ are finite sets, and their colimit is $B$ . $\hfill\blacktriangleleft$

2.3 Relating $\mathsf{ODisc}$ and $\mathsf{Boole}_{\omega}$

Lemma 2.13.

Every countably presented Boolean algebra is a sequential colimit of finite Boolean algebras.

Proof.

Consider a countably presented Boolean algebra of the form $B=2[\mathbb{N}]/(r_{n})_{n:\mathbb{N}}$ . For each $n:\mathbb{N}$ , let $G_{n}$ be the union of $\{g_{i}\ |\ {i\leq n}\}$ and the finite set of generators occurring in $r_{i}$ for some $i\leq n$ . Denote $B_{n}=2[G_{n}]/(r_{i})_{i\leq n}$ . Each $B_{n}$ is a finite Boolean algebra, and there are canonical maps $B_{n}\to B_{n+1}$ . Then $B$ is the colimit of this sequence. $\hfill\blacktriangleleft$

Corollary 2.14.

A Boolean algebra $B$ is overtly discrete if and only if it is countably presented.

Proof.

Assume $B:\mathsf{ODisc}$ . By Lemma 2.12, we get a surjection $\mathbb{N}\twoheadrightarrow B$ and that $B$ has open equality. Consider the induced surjective morphism $f:2[\mathbb{N}]\twoheadrightarrow B$ . By countable choice, we get for each $b:2[\mathbb{N}]$ a sequence $\alpha_{b}:2^{\mathbb{N}}$ such that $(f(b)=0)\leftrightarrow\exists_{k:\mathbb{N}}(\alpha_{b,k}=1)$ . Consider $r:2[\mathbb{N}]\to\mathbb{N}\to 2[\mathbb{N}]$ given by

r(b,k)=\begin{cases}b&\text{ if }\alpha_{b}(k)=1\\ 0&\text{ if }\alpha_{b}(k)=0\end{cases}

Then $B=2[\mathbb{N}]/(r(b,k))_{b:2[\mathbb{N}],k:\mathbb{N}}$ . The converse comes from Lemma 2.13. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 2.15.

By Lemma 2.7 and Corollary 2.14, it follows that any $g:B\to C$ in $\mathsf{Boole}_{\omega}$ has an overtly discrete kernel. As a consequence, the kernel is enumerable and $B/Ker(g)$ is in $\mathsf{Boole}_{\omega}$ . By uniqueness of epi-mono factorizations and Axiom 2, the factorization $B\twoheadrightarrow B/Ker(g)\hookrightarrow C$ corresponds to $\operatorname{Sp}(C)\twoheadrightarrow\operatorname{Sp}(B/Ker(g))% \hookrightarrow\operatorname{Sp}(B)$ .

$\blacktriangleright$ Remark 2.16.

Similarly to Lemma 2.3 and Lemma 2.4, a (resp. surjective, injective) morphism in $\mathsf{Boole}_{\omega}$ is a sequential colimit of (resp. surjective, injective) morphisms between finite Boolean algebras.

3 Stone spaces

3.1 Stone spaces as profinite sets

Here we present Stone spaces as sequential limits of finite sets. This is the perspective taken in Condensed Mathematics [15, 1, 5]. Some of the results in this section are versions of the axioms used in [2]. A full proof of all these axioms is part of future work.

Lemma 3.1.

Any $S:\mathsf{Stone}$ is a sequential limit of finite sets.

Proof.

Assume $B:\mathsf{Boole}_{\omega}$ . By Remark 1.10 and Lemma 2.13, we have that $\operatorname{Sp}(B)$ is a sequential limit of spectra of finite Boolean algebras, which are finite sets. $\hfill\blacktriangleleft$

Lemma 3.2.

A sequential limit of finite sets is a Stone space.

Proof.

By Remark 1.10 and Lemma 2.6, we have that $\mathsf{Stone}$ is closed under sequential limits, and finite sets are Stone. $\hfill\blacktriangleleft$

Corollary 3.3.

Stone spaces are stable under finite limits.

$\blacktriangleright$ Remark 3.4.

By Remark 2.16 and Axiom 2, maps (resp. surjections, injections) of Stone spaces are sequential limits of maps (resp. surjections, injections) of finite sets.

Lemma 3.5.

For $(S_{n})_{n:\mathbb{N}}$ a sequence of finite types with $S=\lim_{n}S_{n}$ and $k:\mathbb{N}$ , we have that $\operatorname{Fin}(k)^{S}$ is the sequential colimit of $\operatorname{Fin}(k)^{S_{n}}$ .

Proof.

By Remark 1.10 we have $\operatorname{Fin}(k)^{S}=\mathrm{Hom}(2^{k},2^{S})$ . Since $2^{k}$ is finite, we have that $\mathrm{Hom}(2^{k},\_)$ commutes with sequential colimits, therefore $\mathrm{Hom}(2^{k},2^{S})$ is the sequential colimit of $\mathrm{Hom}(2^{k},2^{S_{n}})$ . By applying Remark 1.10 again, the latter type is $\operatorname{Fin}(k)^{S_{n}}$ . $\hfill\blacktriangleleft$

Lemma 3.6.

For $S:\mathsf{Stone}$ and $f:S\to\mathbb{N}$ , there exists some $k:\mathbb{N}$ such that $f$ factors through $\operatorname{Fin}(k)$ .

Proof.

For each $n:\mathbb{N}$ , the fiber of $f$ over $n$ is a decidable subset $f_{n}:S\to 2$ . We must have that $\operatorname{Sp}(2^{S}/(f_{n})_{n:\mathbb{N}})=\bot$ , hence there exists some $k:\mathbb{N}$ with $\bigvee_{n\leq k}f_{n}=_{2^{S}}1$ . It follows that $f(s)\leq k$ for all $s : S$ as required. $\hfill\blacktriangleleft$

Corollary 3.7.

For $(S_{n})_{n:\mathbb{N}}$ a sequence of finite types with $S=\lim_{n}S_{n}$ , we have that $\mathbb{N}^{S}$ is the sequential colimit of $\mathbb{N}^{S_{n}}$ .

Proof.

By Lemma 3.6 we have that $\mathbb{N}^{S}$ is the sequential colimit of $\operatorname{Fin}(k)^{S}$ . By Lemma 3.5, $\operatorname{Fin}(k)^{S}$ is the sequential colimit of the $\operatorname{Fin}(k)^{S_{n}}$ and we can swap the sequential colimits to conclude. $\hfill\blacktriangleleft$

3.2 $\mathsf{Closed}$ and $\mathsf{Stone}$

Corollary 3.8.

For all $S:\mathsf{Stone}$ , the proposition $\lVert S\rVert$ is closed.

Proof.

By Lemma 1.12, $\neg S$ is equivalent to $0=_{2^{S}}1$ , which is open by Lemma 2.13 and Lemma 2.12. Hence $\neg\neg S$ is a closed proposition, and by Corollary 1.13, so is $\lVert S\rVert$ . $\hfill\blacktriangleleft$

Corollary 3.9.

A proposition $P$ is closed if and only if it is a Stone space.

Proof.

By the above, if $S$ is both a Stone space and a proposition, it is closed. By Lemma 1.9, any closed proposition is Stone. $\hfill\blacktriangleleft$

Lemma 3.10.

For all $S:\mathsf{Stone}$ and $s, t : S$ , the proposition $s=t$ is closed.

Proof.

Suppose $S=\operatorname{Sp}(B)$ and let $G$ be a countable set of generators for $B$ . Then $s=t$ if and only if $s(g)=t(g)$ for all $g : G$ . So $s=t$ is a countable conjunction of decidable propositions, hence closed. $\hfill\blacktriangleleft$

3.3 The topology on Stone spaces

Theorem 3.11.

Let $A\subseteq S$ be a subset of a Stone space. The following are equivalent:

(i)

There exists a map $\alpha:S\to 2^{\mathbb{N}}$ such that $A(x)\leftrightarrow\forall_{n:\mathbb{N}}\,\alpha_{x,n}=0$ for any $x : S$ .
(ii)

There exists a family $(D_{n})_{n:\mathbb{N}}$ of decidable subsets of $S$ such that $A=\bigcap_{n:\mathbb{N}}D_{n}$ .
(iii)

There exists a Stone space $T$ and some embedding $T\to S$ whose image is $A$ .
(iv)

There exists a Stone space $T$ and some map $T\to S$ whose image is $A$ .
(v)

$A$ is closed.

Proof.

$\blacksquare$

$(i)\leftrightarrow(ii)$ . $D_{n}$ and $\alpha$ can be defined from each other by $D_{n}(x)\leftrightarrow(\alpha_{x,n}=0)$ . Then observe that

$x\in\bigcap_{n:\mathbb{N}}D_{n}\leftrightarrow\forall_{n:\mathbb{N}}(\alpha_{x% ,n}=0).$
$\blacksquare$

$(ii)\to(iii)$ . Let $S=\operatorname{Sp}(B)$ . By Axiom 1, we have $(d_{n})_{n:\mathbb{N}}$ in $B$ such that $D_{n}=\{x:S\ |\ x(d_{n})=0\}$ . Let $C=B/(d_{n})_{n:\mathbb{N}}$ . Then $\operatorname{Sp}(C)\to S$ is as desired because:

$\operatorname{Sp}(C)=\{x:S\ |\ \forall_{n:\mathbb{N}}\,x(d_{n})=0\}=\bigcap_{n% :\mathbb{N}}D_{n}.$
$\blacksquare$

$(iii)\to(iv)$ . Immediate.
$\blacksquare$

$(iv)\to(ii)$ . Assume $f:T\to S$ corresponds to $g:B\to C$ in $\mathsf{Boole}_{\omega}$ . By Remark 2.15, $f(T)=\operatorname{Sp}(B/Ker(g))$ and there exists a surjection $d:\mathbb{N}\to Ker(g)$ . For $n:\mathbb{N}$ , we denote by $D_{n}$ the decidable subset of $S$ corresponding to $d_{n}$ . Then we have that $\operatorname{Sp}(B/Ker(g))=\bigcap_{n:\mathbb{N}}D_{n}$ .
$\blacksquare$

$(i)\to(v)$ . By definition.
$\blacksquare$

$(v)\to(iv)$ . We have a surjection $2^{\mathbb{N}}\twoheadrightarrow\mathsf{Closed}$ defined by $\alpha\mapsto\forall_{n:\mathbb{N}}\,\alpha_{n}=0.$ Remark 1.11 gives us that there merely exists $T,e,\beta_{\cdot}$ as follows:

Define $B(x)\leftrightarrow\forall_{n:\mathbb{N}}\,\beta_{x,n}=0$ . As $(i)\to(iii)$ by the above, $B$ is the image of some Stone space. Note that $A$ is the image of $B$ , thus $A$ is the image of some Stone space.

$\hfill\blacktriangleleft$

Corollary 3.12.

Closed subtypes of Stone spaces are Stone.

Corollary 3.13.

For $S:\mathsf{Stone}$ and $A\subseteq S$ closed, we have that $\exists_{x:S}A(x)$ is closed.

Proof.

By Corollary 3.12, we have that $\Sigma_{x:S}A(x)$ is Stone, so its truncation is closed by Corollary 3.8. $\hfill\blacktriangleleft$

Corollary 3.14.

Closed propositions are closed under sigma types.

Proof.

Let $P:\mathsf{Closed}$ and $Q:P\to\mathsf{Closed}$ . Then $\Sigma_{p:P}Q(p)\leftrightarrow\exists_{p:P}Q(p)$ . As $P$ is Stone by Corollary 3.9, Corollary 3.13 gives that $\Sigma_{p:P}Q(p)$ is closed. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 3.15.

Analogously to Corollary 2.10 and Remark 2.11, it follows that closedness is transitive and $\mathsf{Closed}$ forms a dominance.

Lemma 3.16.

Assume $S:\mathsf{Stone}$ with $F,G:S\to\mathsf{Closed}$ such that $F\cap G=\emptyset$ . Then there exists a decidable subset $D:S\to 2$ such $F\subseteq D,G\subseteq\neg D$ .

Proof.

Assume $S=\operatorname{Sp}(B)$ . By Theorem 3.11, for all $n:\mathbb{N}$ there is $f_{n},g_{n}:B$ such that $x\in F$ if and only if $\forall_{n:\mathbb{N}}\,x(f_{n})=0$ and $y\in G$ if and only if $\forall_{n:\mathbb{N}}\,y(g_{n})=0$ . Denote by $h$ the sequence defined by $h_{2k}=f_{k}$ and $h_{2k+1}=g_{k}$ . Then $\operatorname{Sp}(B/(h_{k})_{k:\mathbb{N}})=F\cap G=\emptyset$ , so by Lemma 1.12 there exists finite sets $I,J\subseteq\mathbb{N}$ such that $1=_{B}((\bigvee_{i:I}f_{i})\vee(\bigvee_{j:J}g_{j})).$ If $y\in F$ , then $y(f_{i})=0$ for all $i : I$ , hence $y(\bigvee_{j:J}g_{j})=1$ If $x\in G$ , we have $x(\bigvee_{j:J}g_{j})=0$ . Thus we can define the required $D$ by $D(x)\leftrightarrow x(\bigvee_{j:J}g_{j})=1$ . $\hfill\blacktriangleleft$

4 Compact Hausdorff spaces

Definition 4.1.

A type $X$ is called a compact Hausdorff space if its identity types are closed propositions and there exists some $S:\mathsf{Stone}$ with a surjection $S\twoheadrightarrow X$ . We write $\mathsf{CHaus}$ for the type of compact Hausdorff spaces.

4.1 Topology on compact Hausdorff spaces

Lemma 4.2.

Let $X:\mathsf{CHaus}$ , $S:\mathsf{Stone}$ and $q:S\twoheadrightarrow X$ surjective. Then $A\subseteq X$ is closed if and only if it is the image of a closed subset of $S$ by $q$ .

Proof.

As $q$ is surjective, we have $q(q^{-1}(A))=A$ . If $A$ is closed, so is $q^{-1}(A)$ and hence $A$ is the image of a closed subset of $S$ . Conversely, let $B\subseteq S$ be closed. Then $x\in q(B)$ if and only if

\exists_{s:S}(B(s)\wedge q(s)=x).

Hence by Corollary 3.13, $q(B)$ is closed. $\hfill\blacktriangleleft$

The next two corollaries mean that compact Hausdorff spaces are compact in the sense of Synthetic Topology.

Corollary 4.3.

Assume given $X:\mathsf{CHaus}$ with $A\subseteq X$ closed. Then $\exists_{x:X}A(x)$ is closed, and equivalent to $A\neq\emptyset$ .

Proof.

From Lemma 4.2 and Theorem 3.11, it follows that $A\subseteq X$ is closed if and only if it is the image of a map $T\to X$ for some $T:\mathsf{Stone}$ . Then $\exists_{x:X}A(x)$ if and only $\lVert T\rVert$ , which is closed by Corollary 3.8. Therefore $\exists_{x:X}A(x)$ is $\neg\neg$ -stable and equivalent to $A\neq\emptyset$ . $\hfill\blacktriangleleft$

Corollary 4.4.

Assume given $X:\mathsf{CHaus}$ with $U\subseteq X$ open. Then $\forall_{x:X}U(x)$ is open.

The next lemma means that compact Hausdorff spaces are not too far from being compact in the classical sense.

Lemma 4.5.

Given $X:\mathsf{CHaus}$ and $C_{n}:X\to\mathsf{Closed}$ closed subsets such that $\bigcap_{n:\mathbb{N}}C_{n}=\emptyset$ , there is some $k:\mathbb{N}$ with $\bigcap_{n\leq k}C_{n}=\emptyset$ .

Proof.

By Lemma 4.2 it is enough to prove the result when $X$ is Stone, and by Theorem 3.11 we can assume $C_{n}$ decidable. So assume $X=\operatorname{Sp}(B)$ and $c_{n}:B$ such that

C_{n}=\{x:B\to 2\ |\ x(c_{n})=0\}.

Then we have that

\operatorname{Sp}(B/(c_{n})_{n:\mathbb{N}})\simeq\bigcap_{n:\mathbb{N}}C_{n}=\emptyset.

Hence $0=1$ in $B/(c_{n})_{n:\mathbb{N}}$ and there is some $k:\mathbb{N}$ with $\bigvee_{n\leq k}c_{n}=1$ , which means that

\emptyset=\operatorname{Sp}(B/(c_{n})_{n\leq k})\simeq\bigcap_{n\leq k}C_{n}

as required. $\hfill\blacktriangleleft$

Corollary 4.6.

Let $X,Y:\mathsf{CHaus}$ and $f:X\to Y$ . Suppose $(G_{n})_{n:\mathbb{N}}$ is a decreasing sequence of closed subsets of $X$ . Then $f(\bigcap_{n:\mathbb{N}}G_{n})=\bigcap_{n:\mathbb{N}}f(G_{n})$ .

Proof.

It is always the case that $f(\bigcap_{n:\mathbb{N}}G_{n})\subseteq\bigcap_{n:\mathbb{N}}f(G_{n})$ . For the converse direction, suppose that $y\in f(G_{n})$ for all $n:\mathbb{N}$ . We define $F\subseteq X$ closed by $F=f^{-1}(y)$ . Then for all $n:\mathbb{N}$ we have that $F\cap G_{n}$ is non-empty. By Lemma 4.5 this implies that $\bigcap_{n:\mathbb{N}}(F\cap G_{n})\neq\emptyset$ . By Corollary 4.3, we have that $\bigcap_{n:\mathbb{N}}(F\cap G_{n})$ is merely inhabited. Thus $y\in f(\bigcap_{n:\mathbb{N}}G_{n})$ as required. $\hfill\blacktriangleleft$

Corollary 4.7.

Let $A\subseteq X$ be a subset of a compact Hausdorff space and $p:S\twoheadrightarrow X$ be a surjective map with $S:\mathsf{Stone}$ . Then $A$ is closed (resp. open) if and only if there exists a sequence $(D_{n})_{n:\mathbb{N}}$ of decidable subsets of $S$ such that $A=\bigcap_{n:\mathbb{N}}p(D_{n})$ (resp. $A=\bigcup_{n:\mathbb{N}}\neg p(D_{n})$ ).

Proof.

The characterization of closed subsets follows from characterization (ii) in Theorem 3.11, Lemma 4.2 and Corollary 4.6. To deduce the characterization of open subsets we use Remark 1.20 and Lemma 1.23. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 4.8.

For $S:\mathsf{Stone}$ , there is a surjection $\mathbb{N}\twoheadrightarrow 2^{S}$ . It follows that for any $X:\mathsf{CHaus}$ there is a surjection from $\mathbb{N}$ to a basis of $X$ . Classically this means that $X$ is second countable.

The next lemma means that compact Hausdorff spaces are normal.

Lemma 4.9.

Assume $X:\mathsf{CHaus}$ and $A,B\subseteq X$ closed such that $A\cap B=\emptyset$ . Then there exist $U,V\subseteq X$ open such that $A\subseteq U$ , $B\subseteq V$ and $U\cap V=\emptyset$ .

Proof.

Let $q:S\twoheadrightarrow X$ be a surjective map with $S:\mathsf{Stone}$ . As $q^{-1}(A)$ and $q^{-1}(B)$ are closed, by Lemma 3.16, there is some $D:S\to 2$ such that $q^{-1}(A)\subseteq D$ and $q^{-1}(B)\subseteq\neg D$ . Note that $q(D)$ and $q(\neg D)$ are closed by Lemma 4.2. As $q^{-1}(A)\cap\neg D=\emptyset$ , we have that $A\subseteq\neg q(\neg D):=U$ . Similarly $B\subseteq\neg q(D):=V$ . Then $U$ and $V$ are disjoint because $\neg q(D)\cap\neg q(\neg D)=\neg(q(D)\cup q(\neg D))=\neg X=\emptyset$ . $\hfill\blacktriangleleft$

4.2 Compact Hausdorff spaces are stable under sigma types

Lemma 4.10.

A type $X$ is Stone if and only if it is merely a closed subset of $2^{\mathbb{N}}$ .

Proof.

By Remark 1.4, any $B:\mathsf{Boole}_{\omega}$ can be written as $2[\mathbb{N}]/(r_{n})_{n:\mathbb{N}}$ . By Remark 2.15, the quotient map induces an embedding $\operatorname{Sp}(B)\hookrightarrow\operatorname{Sp}(2[\mathbb{N}])=2^{\mathbb% {N}}$ , which is closed by Theorem 3.11. $\hfill\blacktriangleleft$

Lemma 4.11.

Compact Hausdorff spaces are stable under $\Sigma$ -types.

Proof.

Assume $X:\mathsf{CHaus}$ and $Y:X\to\mathsf{CHaus}$ . By Corollary 3.14 we have that identity types in $\Sigma_{x:X}Y(x)$ are closed. By Lemma 4.10 we know that for any $x : X$ there merely exists a closed $C\subseteq 2^{\mathbb{N}}$ with a surjection $\Sigma_{\alpha:2^{\mathbb{N}}}C(\alpha)\twoheadrightarrow Y(x)$ . By local choice we merely get $S:\mathsf{Stone}$ with a surjection $p:S\twoheadrightarrow X$ such that for all $s : S$ we have $C_{s}\subseteq 2^{\mathbb{N}}$ closed and a surjection $\Sigma_{2^{\mathbb{N}}}C_{s}\twoheadrightarrow Y(p(s))$ . This gives a surjection $\Sigma_{s:S,\alpha:2^{\mathbb{N}}}C_{s}(\alpha)\twoheadrightarrow\Sigma_{x:X}Y% _{x}$ and the source is Stone by Remark 3.4 and Corollary 3.12. $\hfill\blacktriangleleft$

4.3 Stone spaces are stable under sigma types

We will show that Stone spaces are precisely totally disconnected compact Hausdorff spaces. We will use this to prove that a sigma type of Stone spaces is Stone.

Lemma 4.12.

Assume $X:\mathsf{CHaus}$ , then $2^{X}$ is countably presented.

Proof.

There is some surjection $q:S\twoheadrightarrow X$ with $S:\mathsf{Stone}$ . This induces an injection of Boolean algebras $2^{X}\hookrightarrow 2^{S}$ . Note that $a:S\to 2$ lies in $2^{X}$ if and only if:

\forall_{s,t:S}\ q(s)=_{X}q(t)\to a(s)=a(t).

As equality in $X$ is closed and equality in $2$ is decidable, the implication is open for every $s, t : S$ . By Corollary 4.4, we conclude that $2^{X}$ is an open subalgebra of $2^{S}$ . Therefore, it is in $\mathsf{ODisc}$ by Lemma 2.8 and Lemma 2.7 and in $\mathsf{Boole}_{\omega}$ by Corollary 2.14. $\hfill\blacktriangleleft$

Definition 4.13.

For all $X:\mathsf{CHaus}$ and $x : X$ , we define $Q_{x}$ the connected component of $x$ as the intersection of all $D\subseteq X$ decidable such that $x\in D$ .

Lemma 4.14.

For all $X:\mathsf{CHaus}$ with $x : X$ , we have that $Q_{x}$ is a countable intersection of decidable subsets of $X$ .

Proof.

By Lemma 4.12, we can enumerate the elements of $2^{X}$ , say as $(D_{n})_{n:\mathbb{N}}$ . For $n:\mathbb{N}$ we define $E_{n}$ as $D_{n}$ if $x\in D_{n}$ and $X$ otherwise. Then $\cap_{n:\mathbb{N}}E_{n}=Q_{x}$ . $\hfill\blacktriangleleft$

Lemma 4.15.

Assume $X:\mathsf{CHaus}$ with $x : X$ and suppose $U\subseteq X$ open with $Q_{x}\subseteq U$ . Then we have some decidable $E\subseteq X$ with $x\in E$ and $E\subseteq U$ .

Proof.

By Lemma 4.14, we have $Q_{x}=\bigcap_{n:\mathbb{N}}D_{n}$ with $D_{n}\subseteq X$ decidable. If $Q_{x}\subseteq U$ , then

Q_{x}\cap\neg U=\bigcap_{n:\mathbb{N}}(D_{n}\cap\neg U)=\emptyset.

By Lemma 4.5 there is some $k:\mathbb{N}$ with

(\bigcap_{n\leq k}D_{n})\cap\neg U=\bigcap_{n\leq k}(D_{n}\cap\neg U)=\emptyset.

Therefore $\bigcap_{n\leq k}D_{n}\subseteq\neg\neg U$ . As $U$ is open, $\neg\neg U=U$ and $E:=\bigcap_{n\leq k}D_{n}$ is as desired. $\hfill\blacktriangleleft$

Lemma 4.16.

Assume $X:\mathsf{CHaus}$ with $x : X$ . Then any map in $Q_{x}\to 2$ is constant.

Proof.

Assume $Q_{x}=A\cup B$ with $A, B$ decidable and disjoint subsets of $Q_{x}$ . Assume $x\in A$ . By Lemma 4.14, $Q_{x}\subseteq X$ is closed. Using Remark 3.15, it follows that $A,B\subseteq X$ are closed and disjoint. By Lemma 4.9 there exist $U, V$ disjoint open such that $A\subseteq U$ and $B\subseteq V$ . By Lemma 4.15 we have a decidable $D$ such that $Q_{x}\subseteq D\subseteq U\cup V$ . Note that $E:=D\cap U=D\cap(\neg V)$ is clopen, hence decidable by Corollary 1.22. But $x\in E$ , hence $B\subseteq Q_{x}\subseteq E$ but $B\cap E=\emptyset$ , hence $B=\emptyset$ . $\hfill\blacktriangleleft$

Lemma 4.17.

Let $X:\mathsf{CHaus}$ , then $X$ is Stone if and only $\forall_{x:X}\,Q_{x}=\{x\}$ .

Proof.

By Axiom 1, it is clear that for all $x : S$ with $S:\mathsf{Stone}$ we have that $Q_{x}=\{x\}$ . Conversely, assume $X:\mathsf{CHaus}$ such that $\forall_{x:X}\,Q_{x}=\{x\}$ . We claim that the evaluation map $e:X\to\operatorname{Sp}(2^{X})$ is both injective and surjective, hence an equivalence. Let $x, y : X$ be such that $e(x)=e(y)$ , i.e. such that $f(x)=f(y)$ for all $f:2^{X}$ . Then $y\in Q_{x}$ , hence $x=y$ by assumption. Thus $e$ is injective. Let $q:S\twoheadrightarrow X$ be a surjective map. It induces an injection $2^{X}\hookrightarrow 2^{S}$ , which by Axiom 2 induces a surjection $p:\operatorname{Sp}(2^{S})\twoheadrightarrow\operatorname{Sp}(2^{X})$ . Note that $e\circ q$ is equal to $p$ so $e$ is surjective. $\hfill\blacktriangleleft$

Theorem 4.18.

Assume $S:\mathsf{Stone}$ and $T:S\to\mathsf{Stone}$ . Then $\Sigma_{x:S}T(x)$ is Stone.

Proof.

By Lemma 4.11 we have that $\Sigma_{x:S}T(x)$ is a compact Hausdorff space. By Lemma 4.17 it is enough to show that for all $x : S$ and $y:T(x)$ we have that $Q_{(x,y)}$ is a singleton. Assume $(x^{\prime},y^{\prime})\in Q_{(x,y)}$ , then for any map $f:S\to 2$ we have that:

f(x)=f\circ\pi_{1}(x,y)=f\circ\pi_{1}(x^{\prime},y^{\prime})=f(x^{\prime})

so that $x^{\prime}\in Q_{x}$ and since $S$ is Stone, by Lemma 4.17 we have that $x=x^{\prime}$ . Therefore we have $Q_{(x,y)}\subseteq\{x\}\times T(x)$ . Assume $z,z^{\prime}:Q_{(x,y)}$ , then for any map $g:T(x)\to 2$ we have that $g(z)=g(z^{\prime})$ by Lemma 4.16. Since $T(x)$ is Stone, we conclude $z=z^{\prime}$ by Lemma 4.17. $\hfill\blacktriangleleft$

4.4 The unit interval as a compact Hausdorff space

Since we have dependent choice, the unit interval $\mathbb{I}=[0,1]$ can be defined using Cauchy reals or Dedekind reals. We can freely use results from constructive analysis [3]. As we have $\neg$ WLPO, MP and LLPO, we can use the results from constructive reverse mathematics that follow from these principles [11, 7].

Definition 4.19.

We define for each $n:\mathbb{N}$ the Stone space $2^{n}$ of binary sequences of length $n$ . And we define $cs_{n}:2^{n}\to\mathbb{Q}$ by $cs_{n}(\alpha)=\sum_{i<n}\frac{\alpha(i)}{2^{i+1}}.$ Finally we write $\sim_{n}$ for the binary relation on $2^{n}$ given by $\alpha\sim_{n}\beta\leftrightarrow\left|cs_{n}(\alpha)-cs_{n}(\beta)\right|% \leq\frac{1}{2^{n}}$ .

$\blacktriangleright$ Remark 4.20.

The inclusion $\operatorname{Fin}(n)\hookrightarrow\mathbb{N}$ induces a restriction $\_|_{n}:2^{\mathbb{N}}\to 2^{n}$ for each $n:\mathbb{N}$ .

Definition 4.21.

We define $cs:2^{\mathbb{N}}\to\mathbb{I}$ as $cs(\alpha)=\sum_{i=0}^{\infty}\frac{\alpha(i)}{2^{i+1}}.$

Theorem 4.22.

The type $\mathbb{I}$ is a compact Hausdorff space.

Proof.

By LLPO, we have that $c s$ is surjective. Note that $cs(\alpha)=cs(\beta)$ if and only if for all $n:\mathbb{N}$ we have $\alpha|_{n}\sim_{n}\beta|_{n}$ . This is a countable conjunction of decidable propositions, so that equality in $\mathbb{I}$ is closed. $\hfill\blacktriangleleft$

The following is also given by Definitions 2.7 and 2.10 of [3].

Definition 4.23.

Assume given $x,y:\mathbb{I}$ and $\alpha,\beta:2^{\mathbb{N}}$ such that $x=cs(\alpha),y=cs(\beta)$ . Then $x<y$ is the proposition $\exists_{n:\mathbb{N}}\,cs_{n}(\alpha)+\frac{1}{2^{n}}<_{\mathbb{Q}}cs_{n}(\beta)$ , which is independent of the choice of $\alpha,\beta$ .

$\blacktriangleright$ Remark 4.24.

For all $x,y:\mathbb{I}$ , we have that $x<y$ is an open proposition and that $x\neq y$ is equivalent to $(x<y)\vee(y<x)$ .

Lemma 4.25.

For all $D\subseteq 2^{\mathbb{N}}$ decidable, we have that $cs(D)$ is a finite union of closed intervals.

Proof.

If $D$ is contains precisely the $\alpha:2^{\mathbb{N}}$ with a fixed initial segment, $cs(D)$ is a closed interval. Any decidable subset of $2^{\mathbb{N}}$ is a finite union of such subsets. $\hfill\blacktriangleleft$

Lemma 4.26.

The complement of a finite union of closed intervals is a finite union of open intervals.

By Corollary 4.7 we can thus conclude:

Lemma 4.27.

Every open $U\subseteq\mathbb{I}$ can be written as a countable union of open intervals.

It follows that the topology of $\mathbb{I}$ is generated by open intervals, which corresponds to the standard topology on $\mathbb{I}$ . Hence our notion of continuity agrees with the $\epsilon,\delta$ -definition of continuity one would expect and we get the following:

Theorem 4.28.

Every function $f:\mathbb{I}\to\mathbb{I}$ is continuous in the $\epsilon,\delta$ -sense.

5 Cohomology

In this section we compute $H^{1}(S,\mathbb{Z})=0$ for all $S$ Stone, and show that $H^{1}(X,\mathbb{Z})$ for $X$ compact Hausdorff can be computed using Čech cohomology. We use this to compute $H^{1}(\mathbb{I},\mathbb{Z})=0$ .

$\blacktriangleright$ Remark 5.1.

We only work with the first cohomology group with coefficients in $\mathbb{Z}$ as it is sufficient for the proof of Brouwer’s fixed-point theorem, but the results could be extended to $H^{n}(X,A)$ for $A$ any family of countably presented abelian groups indexed by $X$ .

$\blacktriangleright$ Remark 5.2.

We write $\mathrm{Ab}$ for the type of abelian groups and if $G:\mathrm{Ab}$ we write $\mathrm{B}G$ for the delooping of $G$ [13, 22]. This means that $H^{1}(X,G)$ is the set truncation of $X\to\mathrm{B}G$ .

5.1 Čech cohomology

Definition 5.3.

Given a type $S$ , types $T_{x}$ for $x : S$ and $A:S\to\mathrm{Ab}$ , we define $\check{C}(S,T,A)$ as the chain complex

where the boundary maps are defined as

	$\displaystyle d_{0}(\alpha)_{x}(u,v)=$	$\displaystyle\ \alpha_{x}(v)-\alpha_{x}(u)$
	$\displaystyle d_{1}(\beta)_{x}(u,v,w)=$	$\displaystyle\ \beta_{x}(v,w)-\beta_{x}(u,w)+\beta_{x}(u,v)$

Definition 5.4.

Given a type $S$ , types $T_{x}$ for $x : S$ and $A:S\to\mathrm{Ab}$ , we define its Čech cohomology groups by

\check{H}^{0}(S,T,A)=\mathrm{ker}(d_{0})\quad\quad\quad\check{H}^{1}(S,T,A)=% \mathrm{ker}(d_{1})/\mathrm{im}(d_{0})

We call elements of $\mathrm{ker}(d_{1})$ cocycles and elements of $\mathrm{im}(d_{0})$ coboundaries.

This means that $\check{H}^{1}(S,T,A)=0$ if and only if $\check{C}(S,T,A)$ is exact at the middle term. Now we give three general lemmas about Čech complexes.

Lemma 5.5.

Assume a type $S$ , types $T_{x}$ for $x : S$ and $A:S\to\mathrm{Ab}$ with $t:\prod_{x:S}T_{x}$ . Then $\check{H}^{1}(S,T,A)=0$ .

Proof.

Assume given a cocycle, i.e. $\beta:\prod_{x:S}A_{x}^{T_{x}^{2}}$ such that for all $x : S$ and $u,v,w:T_{x}$ we have that $\beta_{x}(u,v)+\beta_{x}(v,w)=\beta_{x}(u,w)$ . We define $\alpha:\prod_{x:S}A_{x}^{T_{x}}$ by $\alpha_{x}(u)=\beta_{x}(t_{x},u)$ . Then for all $x : S$ and $u,v:T_{x}$ we have that $d_{0}(\alpha)_{x}(u,v)=\beta_{x}(t_{x},v)-\beta_{x}(t_{x},u)=\beta_{x}(u,v)$ so that $\beta$ is a coboundary. $\hfill\blacktriangleleft$

Lemma 5.6.

Given a type $S$ , types $T_{x}$ for $x : S$ and $A:S\to\mathrm{Ab}$ , we have that $\check{H}^{1}(S,T,\lambda x.A_{x}^{T_{x}})=0$ .

Proof.

Assume given a cocycle, i.e. $\beta:\prod_{x:S}A_{x}^{T_{x}^{3}}$ such that for all $x : S$ and $u,v,w,t:T_{x}$ we have that $\beta_{x}(u,v,t)+\beta_{x}(v,w,t)=\beta_{x}(u,w,t)$ . We define $\alpha:\prod_{x:S}A_{x}^{T_{x}^{2}}$ by $\alpha_{x}(u,t)=\beta_{x}(t,u,t)$ . Then for all $x : S$ and $u,v,t:T_{x}$ we have that $d_{0}(\alpha)_{x}(u,v,t)=\beta_{x}(t,v,t)-\beta_{x}(t,u,t)=\beta_{x}(u,v,t)$ so that $\beta$ is a coboundary. $\hfill\blacktriangleleft$

Lemma 5.7.

Assume a type $S$ and types $T_{x}$ for $x : S$ such that $\prod_{x:S}\lVert T_{x}\rVert$ and $A:S\to\mathrm{Ab}$ such that $\check{H}^{1}(S,T,A)=0$ . Then given $\alpha:\prod_{x:S}\mathrm{B}A_{x}$ with $\beta:\prod_{x:S}(\alpha(x)=*)^{T_{x}}$ , we can conclude $\alpha=*$ .

Proof.

We define $g:\prod_{x:S}A_{x}^{T_{x}^{2}}$ by $g_{x}(u,v)=\beta_{x}(v)-\beta_{x}(u)$ . It is a cocycle in the Čech complex, so that by exactness there is $f:\prod_{x:S}A_{x}^{T_{x}}$ such that for all $x : S$ and $u,v:T_{x}$ we have that $g_{x}(u,v)=f_{x}(v)-f_{x}(u)$ . Then we define $\beta^{\prime}:\prod_{x:S}(\alpha(x)=*)^{T_{x}}$ by $\beta^{\prime}_{x}(u)=\beta_{x}(u)-f_{x}(u)$ so that for all $x : S$ and $u,v:T_{x}$ we have that $\beta^{\prime}_{x}(u)=\beta^{\prime}_{x}(v)$ is equivalent to $f_{x}(v)-f_{x}(u)=\beta_{x}(v)-\beta_{x}(u)$ , which holds by definition. So $\beta^{\prime}$ is constant on each $T_{x}$ and therefore gives $\prod_{x:S}(\alpha(x)=*)^{\lVert T_{x}\rVert}$ . By $\prod_{x:S}\lVert T_{x}\rVert$ we conclude $\alpha=*$ . $\hfill\blacktriangleleft$

5.2 Cohomology of Stone spaces

Lemma 5.8.

Assume given $S:\mathsf{Stone}$ and $T:S\to\mathsf{Stone}$ such that $\prod_{x:S}\lVert T(x)\rVert$ . Then there exists a sequence of finite types $(S_{k})_{k:\mathbb{N}}$ with limit $S$ and a compatible sequence of families of finite types $T_{k}$ over $S_{k}$ with $\prod_{x:S_{k}}\lVert T_{k}(x)\rVert$ and $\mathrm{lim}_{k}\left(\sum_{x:S_{k}}T_{k}(x)\right)=\sum_{x:S}T(x)$ .

Proof.

By theorem Theorem 4.18 and the usual correspondence between surjections and families of inhabited types, a family of inhabited Stone spaces over $S$ correspond to a Stone space $T$ with a surjection $T\to S$ . Then we conclude using Remark 3.4. $\hfill\blacktriangleleft$

Lemma 5.9.

Assume given $S:\mathsf{Stone}$ with $T:S\to\mathsf{Stone}$ such that $\prod_{x:S}\lVert T_{x}\rVert$ . Then we have that $\check{H}^{1}(S,T,\mathbb{Z})=0$ .

Proof.

We apply Lemma 5.8 to get $S_{k}$ and $T_{k}$ finite. Then by Corollary 3.7 we have that $\check{C}(S,T,\mathbb{Z})$ is the sequential colimit of the $\check{C}(S_{k},T_{k},\mathbb{Z})$ . By Lemma 5.5 we have that each of the $\check{C}(S_{k},T_{k},\mathbb{Z})$ is exact, and a sequential colimit of exact sequences is exact. $\hfill\blacktriangleleft$

Lemma 5.10.

Given $S:\mathsf{Stone}$ , we have that $H^{1}(S,\mathbb{Z})=0$ .

Proof.

Assume given a map $\alpha:S\to\mathrm{B}\mathbb{Z}$ . We use local choice to get $T:S\to\mathsf{Stone}$ such that $\prod_{x:S}\lVert T_{x}\rVert$ with $\beta:\prod_{x:S}(\alpha(x)=*)^{T_{x}}$ . Then we conclude by Lemma 5.9 and Lemma 5.7. $\hfill\blacktriangleleft$

Corollary 5.11.

For any $S:\mathsf{Stone}$ the canonical map $\mathrm{B}(\mathbb{Z}^{S})\to(\mathrm{B}\mathbb{Z})^{S}$ is an equivalence.

Proof.

This map is always an embedding. To show it is surjective it is enough to prove that $(\mathrm{B}\mathbb{Z})^{S}$ is connected, which is precisely Lemma 5.10. $\hfill\blacktriangleleft$

5.3 Čech cohomology of compact Hausdorff spaces

Definition 5.12.

A Čech cover consists of $X:\mathsf{CHaus}$ and $S:X\to\mathsf{Stone}$ such that $\prod_{x:X}\lVert S_{x}\rVert$ and $\sum_{x:X}S_{x}:\mathsf{Stone}$ .

By definition any compact Hausdorff space $X$ is part of a Čech cover $(X,S)$ .

Lemma 5.13.

Given a Čech cover $(X,S)$ and $A:X\to\mathrm{Ab}$ , we have an isomorphism $H^{0}(X,A)=\check{H}^{0}(X,S,A)$ natural in $A$ .

Proof.

By definition an element in $\check{H}^{0}(X,S,A)$ is a map $f:\prod_{x:X}A_{x}^{S_{x}}$ such that for all $u,v:S_{x}$ we have $f(u)=f(v)$ . Since $A_{x}$ is a set and the $S_{x}$ are merely inhabited, this is equivalent to $\prod_{x:X}A_{x}$ . Naturality in $A$ is immediate. $\hfill\blacktriangleleft$

Lemma 5.14.

Given a Čech cover $(X,S)$ we have an exact sequence

H^{0}(X,\lambda x.\mathbb{Z}^{S_{x}})\to H^{0}(X,\lambda x.\mathbb{Z}^{S_{x}}/% \mathbb{Z})\to H^{1}(X,\mathbb{Z})\to 0

Proof.

We use the long exact cohomology sequence associated to

0\to\mathbb{Z}\to\mathbb{Z}^{S_{x}}\to\mathbb{Z}^{S_{x}}/\mathbb{Z}\to 0

We just need $H^{1}(X,\lambda x.\mathbb{Z}^{S_{x}})=0$ to conclude. But by Corollary 5.11 we have that $H^{1}(X,\lambda x.\mathbb{Z}^{S_{x}})=H^{1}\left(\sum_{x:X}S_{x},\mathbb{Z}\right)$ which vanishes by Lemma 5.10. $\hfill\blacktriangleleft$

Lemma 5.15.

Given a Čech cover $(X,S)$ we have an exact sequence

\check{H}^{0}(X,S,\lambda x.\mathbb{Z}^{S_{x}})\to\check{H}^{0}(X,S,\lambda x.% \mathbb{Z}^{S_{x}}/\mathbb{Z})\to\check{H}^{1}(X,S,\mathbb{Z})\to 0

Proof.

For $n=1,2,3$ , we have that $\Sigma_{x:X}S_{x}^{n}$ is Stone so that $H^{1}(\Sigma_{x:X}S_{x}^{n},\mathbb{Z})=0$ by Lemma 5.10, giving short exact sequences

0\to\Pi_{x:X}\mathbb{Z}^{S_{x}^{n}}\to\Pi_{x:X}(\mathbb{Z}^{S_{x}})^{S_{x}^{n}% }\to\Pi_{x:X}(\mathbb{Z}^{S_{x}}/\mathbb{Z})^{S_{x}^{n}}\to 0

They fit together in a short exact sequence of complexes

0\to\check{C}(X,S,\mathbb{Z})\to\check{C}(X,S,\lambda x.\mathbb{Z}^{S_{x}})\to% \check{C}(X,S,\lambda x.\mathbb{Z}^{S_{x}}/\mathbb{Z})\to 0

But since $\check{H}^{1}(X,\lambda x.\mathbb{Z}^{S_{x}})=0$ by Lemma 5.6, we conclude using the associated long exact sequence. $\hfill\blacktriangleleft$

Theorem 5.16.

Given a Čech cover $(X,S)$ , we have that $H^{1}(X,\mathbb{Z})=\check{H}^{1}(X,S,\mathbb{Z})$

Proof.

By applying Lemma 5.13, Lemma 5.14 and Lemma 5.15 we get that $H^{1}(X,\mathbb{Z})$ and $\check{H}^{1}(X,S,\mathbb{Z})$ are cokernels of isomorphic maps, so they are isomorphic. $\hfill\blacktriangleleft$

This means that Čech cohomology does not depend on $S$ .

5.4 Cohomology of the interval

$\blacktriangleright$ Remark 5.17.

Recall from Definition 4.19 that there is a binary relation $\sim_{n}$ on $2^{n}=:\mathbb{I}_{n}$ such that $(2^{n},\sim_{n})$ is equivalent to $(\operatorname{Fin}(2^{n}),\lambda x,y.\ |x-y|\leq 1)$ and for $\alpha,\beta:2^{\mathbb{N}}$ we have $(cs(\alpha)=cs(\beta))\leftrightarrow\left(\forall_{n:\mathbb{N}}\alpha|_{n}% \sim_{n}\beta|_{n}\right)$ .

We define $\mathbb{I}_{n}^{\sim 2}=\Sigma_{x,y:\mathbb{I}_{n}}x\sim_{n}y$ and $\mathbb{I}_{n}^{\sim 3}=\Sigma_{x,y,z:\mathbb{I}_{n}}x\sim_{n}y\land y\sim_{n}% z\land x\sim_{n}z$ .

Lemma 5.18.

For any $n:\mathbb{N}$ we have an exact sequence

0\to\mathbb{Z}\overset{d_{0}}{\longrightarrow}\mathbb{Z}^{\mathbb{I}_{n}}% \overset{d_{1}}{\longrightarrow}\mathbb{Z}^{\mathbb{I}_{n}^{\sim 2}}\overset{d% _{2}}{\longrightarrow}\mathbb{Z}^{\mathbb{I}_{n}^{\sim 3}}

where $d_{0}(k)=(\_\mapsto k)$ and

	$\displaystyle d_{1}(\alpha)(u,v)$	$\displaystyle=$	$\displaystyle\alpha(v)-\alpha(u)$
	$\displaystyle d_{2}(\beta)(u,v,w)$	$\displaystyle=$	$\displaystyle\beta(v,w)-\beta(u,w)+\beta(u,v).$

Proof.

It is clear that the map $\mathbb{Z}\to\mathbb{Z}^{\mathbb{I}_{n}}$ is injective as $\mathbb{I}_{n}$ is inhabited, so the sequence is exact at $\mathbb{Z}$ . Assume a cocycle $\alpha:\mathbb{Z}^{\mathbb{I}_{n}}$ , meaning that for all $u,v:\mathbb{I}_{n}$ , if $u\sim_{n}v$ then $\alpha(u)=\alpha(v)$ . Then by Remark 5.17 we see that $\alpha$ is constant, so the sequence is exact at $\mathbb{Z}^{\mathbb{I}_{n}}$ .

Assume a cocycle $\beta:\mathbb{Z}^{\mathbb{I}_{n}^{\sim 2}}$ , meaning that for all $u,v,w:\mathbb{I}_{n}$ such that $u\sim_{n}v$ , $v\sim_{n}w$ and $u\sim_{n}w$ we have that $\beta(u,v)+\beta(v,w)=\beta(u,w)$ . Using Remark 5.17 to pass along the equivalence between $2^{n}$ and $\operatorname{Fin}(2^{n})$ , we define $\alpha(k)=\beta(0,1)+\cdots+\beta(k-1,k)$ . We can check that $\beta(k,l)=\alpha(l)-\alpha(k)$ , so that $\beta$ is indeed a coboundary and the sequence is exact at $\mathbb{Z}^{\mathbb{I}_{n}^{\sim 2}}$ . $\hfill\blacktriangleleft$

Proposition 5.19.

We have that $H^{0}(\mathbb{I},\mathbb{Z})=\mathbb{Z}$ and $H^{1}(\mathbb{I},\mathbb{Z})=0$ .

Proof.

Consider $cs:2^{\mathbb{N}}\to\mathbb{I}$ and the associated Čech cover $T$ of $\mathbb{I}$ defined by:

T_{x}=\Sigma_{y:2^{\mathbb{N}}}(x=_{\mathbb{I}}cs(y))

Then for $l=2,3$ we have that $\mathrm{lim}_{n}\mathbb{I}_{n}^{\sim l}=\sum_{x:\mathbb{I}}T_{x}^{l}$ . By Lemma 5.18 and stability of exactness under sequential colimit, we have an exact sequence

0\to\mathbb{Z}\to\mathrm{colim}_{n}\mathbb{Z}^{\mathbb{I}_{n}}\to\mathrm{colim% }_{n}\mathbb{Z}^{\mathbb{I}_{n}^{\sim 2}}\to\mathrm{colim}_{n}\mathbb{Z}^{% \mathbb{I}_{n}^{\sim 3}}

By Corollary 3.7 this sequence is equivalent to

0\to\mathbb{Z}\to\Pi_{x:\mathbb{I}}\mathbb{Z}^{T_{x}}\to\Pi_{x:\mathbb{I}}% \mathbb{Z}^{T_{x}^{2}}\to\Pi_{x:\mathbb{I}}\mathbb{Z}^{T_{x}^{3}}

So it being exact implies that $\check{H}^{0}(\mathbb{I},T,\mathbb{Z})=\mathbb{Z}$ and $\check{H}^{1}(\mathbb{I},T,\mathbb{Z})=0$ . We conclude by Lemma 5.13 and Theorem 5.16. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 5.20.

We could carry a similar computation for $\mathbb{S}^{1}$ , by approximating it with $2^{n}$ with $0^{n}\sim_{n}1^{n}$ added. We would find $H^{1}(\mathbb{S}^{1},\mathbb{Z})=\mathbb{Z}$ . We will give an alternative, more conceptual proof in the next section.

5.5 Brouwer’s fixed-point theorem

Here we consider the modality defined by localising at $\mathbb{I}$ as explained in [14]. It is denoted by $L_{\mathbb{I}}$ . We say that $X$ is $\mathbb{I}$ -local if $L_{\mathbb{I}}(X)=X$ and that it is $\mathbb{I}$ -contractible if $L_{\mathbb{I}}(X)=1$ .

Lemma 5.21.

$\mathbb{Z}$ and $2$ are $\mathbb{I}$ -local.

Proof.

By Proposition 5.19, from $H^{0}(\mathbb{I},\mathbb{Z})=\mathbb{Z}$ we get that the map $\mathbb{Z}\to\mathbb{Z}^{\mathbb{I}}$ is an equivalence, so $\mathbb{Z}$ is $\mathbb{I}$ -local. We see that $2$ is $\mathbb{I}$ -local as it is a retract of $\mathbb{Z}$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 5.22.

Since $2$ is $\mathbb{I}$ -local, we have that any Stone space is $\mathbb{I}$ -local.

Lemma 5.23.

$\mathrm{B}\mathbb{Z}$ is $\mathbb{I}$ -local.

Proof.

Any identity type in $\mathrm{B}\mathbb{Z}$ is a $\mathbb{Z}$ -torsor, so it is $\mathbb{I}$ -local by Lemma 5.21. So the map $\mathrm{B}\mathbb{Z}\to\mathrm{B}\mathbb{Z}^{\mathbb{I}}$ is an embedding. From $H^{1}(\mathbb{I},\mathbb{Z})=0$ we get that it is surjective, hence an equivalence. $\hfill\blacktriangleleft$

Lemma 5.24.

Assume $X$ a type with $x : X$ such that for all $y : X$ we have $f:\mathbb{I}\to X$ such that $f(0)=x$ and $f(1)=y$ . Then $X$ is $\mathbb{I}$ -contractible.

Proof.

For all $y : X$ we get a map $g:\mathbb{I}\to L_{\mathbb{I}}(X)$ such that $g(0)=[x]$ and $g(1)=[y]$ . Since $L_{\mathbb{I}}(X)$ is $\mathbb{I}$ -local this means that $\prod_{y:X}[x]=[y]$ . We conclude $\prod_{y:L_{\mathbb{I}}(X)}[x]=y$ by applying the elimination principle for the modality. $\hfill\blacktriangleleft$

Corollary 5.25.

We have that $\mathbb{R}$ and $\mathbb{D}^{2}=\{(x,y):\mathbb{R}^{2}\ |\ x^{2}+y^{2}\leq 1\}$ are $\mathbb{I}$ -contractible.

Proposition 5.26.

$L_{\mathbb{I}}(\mathbb{R}/\mathbb{Z})=\mathrm{B}\mathbb{Z}$ .

Proof.

As for any group quotient, the fibers of the map $\mathbb{R}\to\mathbb{R}/\mathbb{Z}$ are $\mathbb{Z}$ -torsors, so we have an induced pullback square

Now we check that the bottom map is an $\mathbb{I}$ -localisation. Since $\mathrm{B}\mathbb{Z}$ is $\mathbb{I}$ -local by Lemma 5.23, it is enough to check that its fibers are $\mathbb{I}$ -contractible. Since $\mathrm{B}\mathbb{Z}$ is connected it is enough to check that $\mathbb{R}$ is $\mathbb{I}$ -contractible. This is Corollary 5.25. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 5.27.

By Lemma 5.23, for any $X$ we have that $H^{1}(X,\mathbb{Z})=H^{1}(L_{\mathbb{I}}(X),\mathbb{Z})$ , so that by Proposition 5.26 we have that $H^{1}(\mathbb{R}/\mathbb{Z},\mathbb{Z})=H^{1}(\mathrm{B}\mathbb{Z},\mathbb{Z})% =\mathbb{Z}$ .

We omit the proof that $\mathbb{S}^{1}=\{(x,y):\mathbb{R}^{2}\ |\ x^{2}+y^{2}=1\}$ is equivalent to $\mathbb{R}/\mathbb{Z}$ . The equivalence can be constructed using trigonometric functions, which exist by Proposition 4.12 in [3].

Proposition 5.28.

The map $\mathbb{S}^{1}\to\mathbb{D}^{2}$ has no retraction.

Proof.

By Corollary 5.25 and Proposition 5.26 we would get a retraction of $\mathrm{B}\mathbb{Z}\to 1$ , so $\mathrm{B}\mathbb{Z}$ would be contractible. $\hfill\blacktriangleleft$

Theorem 5.29 (Intermediate value theorem).

For any $f:\mathbb{I}\to\mathbb{I}$ and $y:\mathbb{I}$ such that $f(0)\leq y$ and $y\leq f(1)$ , there exists $x:\mathbb{I}$ such that $f(x)=y$ .

Proof.

By Corollary 4.3, the proposition $\exists_{x:\mathbb{I}}\,f(x)=y$ is closed and therefore $\neg\neg$ -stable, so we can proceed with a proof by contradiction. If there is no such $x:\mathbb{I}$ , we have $f(x)\neq y$ for all $x:\mathbb{I}$ . By Remark 4.24 we have that $a<b$ or $b<a$ for all distinct numbers $a,b:\mathbb{I}$ . So the following two sets cover $\mathbb{I}$

U_{0}:=\{x:\mathbb{I}\mid f(x)<y\}\quad\quad U_{1}:=\{x:\mathbb{I}\mid y<f(x)\}

Since $U_{0}$ and $U_{1}$ are disjoint, we have $\mathbb{I}=U_{0}+U_{1}$ which allows us to define a non-constant function $\mathbb{I}\to 2$ , which contradicts Lemma 5.21. $\hfill\blacktriangleleft$

Theorem 5.30 (Brouwer’s fixed-point theorem).

For all $f:\mathbb{D}^{2}\to\mathbb{D}^{2}$ there exists $x:\mathbb{D}^{2}$ such that $f(x)=x$ .

Proof.

As above, by Corollary 4.3, we can proceed with a proof by contradiction, so we assume $f(x)\neq x$ for all $x:\mathbb{D}^{2}$ . For any $x:\mathbb{D}^{2}$ we set $d_{x}=x-f(x)$ , so we have that one of the coordinates of $d_{x}$ is invertible. Let $H_{x}(t)=f(x)+t\cdot d_{x}$ be the line through $x$ and $f(x)$ . The intersections of $H_{x}$ and $\partial\mathbb{D}^{2}=\mathbb{S}^{1}$ are given by the solutions of an equation quadratic in $t$ . By invertibility of one of the coordinates of $d_{x}$ , there is exactly one solution with $t>0$ . We denote this intersection by $r(x)$ and the resulting map $r:\mathbb{D}^{2}\to\mathbb{S}^{1}$ has the property that it preserves $\mathbb{S}^{1}$ . Then $r$ is a retraction from $\mathbb{D}^{2}$ onto its boundary $\mathbb{S}^{1}$ , which is a contradiction by Proposition 5.28. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 5.31.

In constructive reverse mathematics [7], it is known that both the intermediate value theorem and Brouwer’s fixed-point theorem are equivalent to LLPO. But LLPO does not hold in real cohesive homotopy type theory, so [16] prove a variant of the statement involving a double negation.

References

[1] Dagur Ásgeirsson. The foundations of condensed mathematics. Master’s thesis, Université de Paris, 2021. URL: https://dagur.sites.ku.dk/condensed-foundations/.
[2] Reid Barton and Johan Commelin. Lean-ctt-snapshot. URL: https://github.com/jcommelin/lean-ctt-snapshot.
[3] Errett Bishop and Douglas Bridges. Constructive analysis, volume 279 of Grundlehren der mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences]. Springer-Verlag, Berlin, 1985. doi:10.1007/978-3-642-61667-9.
[4] Felix Cherubini, Thierry Coquand, and Matthias Hutzler. A foundation for synthetic algebraic geometry, 2023. arXiv:2307.00073.
[5] Dustin Clausen and Peter Scholze. Analytic stacks, 2023-2024. Lecture series. URL: https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO.
[6] Thierry Coquand, Fabian Ruch, and Christian Sattler. Constructive sheaf models of type theory. Math. Struct. Comput. Sci., 31(9):979–1002, 2021. doi:10.1017/S0960129521000359.
[7] Hannes Diener. Constructive reverse mathematics : Habilitationsschrift, 2018. URL: https://dspace.ub.uni-siegen.de/handle/ubsi/1306.
[8] Roy Dyckhoff. Categorical methods in dimension theory. Categor. Topol., Proc. Conf. Mannheim 1975, Lect. Notes Math. 540, 220-242 (1976)., 1976.
[9] Martín Escardó. Synthetic topology: of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87:21–156, 2004. Proceedings of the Workshop on Domain Theoretic Methods for Probabilistic Processes. doi:10.1016/j.entcs.2004.09.017.
[10] Florian Faissole and Bas Spitters. Synthetic topology in homotopy type theory for probabilistic programming. In Proc, page 2017, 2017.
[11] Hajime Ishihara. Reverse Mathematics in Bishop’s Constructive Mathematics. Philosophia Scientiae, 6:43–59, September 2006. doi:10.4000/philosophiascientiae.406.
[12] Davorin Lešnik. Synthetic Topology and Constructive Metric Spaces. PhD thesis, University of Ljubljana, 2021. arXiv:2104.10399.
[13] The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. https://homotopytypetheory.org/book, 2013.
[14] Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. doi:10.23638/LMCS-16(1:2)2020.
[15] Peter Scholze. Lectures on condensed mathematics, 2019. URL: https://people.mpim-bonn.mpg.de/scholze/Condensed.pdf.
[16] Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856–941, 2018. doi:10.1017/S0960129517000147.
[17] Michael Shulman. All $(\infty,1)$ -toposes have strict univalent universes. arXiv preprint, 2019. arXiv:1904.07004.
[18] Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential colimits in homotopy type theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), page 14. ACM, New York, [2020] ©2020. doi:10.1145/3373718.3394801.
[19] Paul Taylor. Abstract Stone duality, 2011. URL: https://www.paultaylor.eu/ASD/.
[20] Niels van der Weide. The internal languages of univalent categories, 2024. doi:10.48550/arXiv.2411.06636.
[21] Steven Vickers. Locales and toposes as spaces. In Handbook of spatial logics, pages 429–496. Springer, 2007. doi:10.1007/978-1-4020-5587-4_8.
[22] David Wärn. Eilenberg-Maclane spaces and stabilisation in homotopy type theory. J. Homotopy Relat. Struct., 18(2-3):357–368, 2023. doi:10.1007/s40062-023-00330-5.
[23] David Wärn. On internally projective sheaves of groups, 2024. arXiv:2409.12835.

[bib.bib1] [1] Dagur Ásgeirsson. The foundations of condensed mathematics. Master’s thesis, Université de Paris, 2021. URL: https://dagur.sites.ku.dk/condensed-foundations/.

[bib.bib2] [2] Reid Barton and Johan Commelin. Lean-ctt-snapshot. URL: https://github.com/jcommelin/lean-ctt-snapshot.

[bib.bib3] [3] Errett Bishop and Douglas Bridges. Constructive analysis, volume 279 of Grundlehren der mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences]. Springer-Verlag, Berlin, 1985. doi:10.1007/978-3-642-61667-9.

[bib.bib4] [4] Felix Cherubini, Thierry Coquand, and Matthias Hutzler. A foundation for synthetic algebraic geometry, 2023. arXiv:2307.00073.

[bib.bib5] [5] Dustin Clausen and Peter Scholze. Analytic stacks, 2023-2024. Lecture series. URL: https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO.

[bib.bib6] [6] Thierry Coquand, Fabian Ruch, and Christian Sattler. Constructive sheaf models of type theory. Math. Struct. Comput. Sci., 31(9):979–1002, 2021. doi:10.1017/S0960129521000359.

[bib.bib7] [7] Hannes Diener. Constructive reverse mathematics : Habilitationsschrift, 2018. URL: https://dspace.ub.uni-siegen.de/handle/ubsi/1306.

[bib.bib8] [8] Roy Dyckhoff. Categorical methods in dimension theory. Categor. Topol., Proc. Conf. Mannheim 1975, Lect. Notes Math. 540, 220-242 (1976)., 1976.

[bib.bib9] [9] Martín Escardó. Synthetic topology: of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87:21–156, 2004. Proceedings of the Workshop on Domain Theoretic Methods for Probabilistic Processes. doi:10.1016/j.entcs.2004.09.017.

[bib.bib10] [10] Florian Faissole and Bas Spitters. Synthetic topology in homotopy type theory for probabilistic programming. In Proc, page 2017, 2017.

[bib.bib11] [11] Hajime Ishihara. Reverse Mathematics in Bishop’s Constructive Mathematics. Philosophia Scientiae, 6:43–59, September 2006. doi:10.4000/philosophiascientiae.406.

[bib.bib12] [12] Davorin Lešnik. Synthetic Topology and Constructive Metric Spaces. PhD thesis, University of Ljubljana, 2021. arXiv:2104.10399.

[bib.bib13] [13] The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. https://homotopytypetheory.org/book, 2013.

[bib.bib14] [14] Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. doi:10.23638/LMCS-16(1:2)2020.

[bib.bib15] [15] Peter Scholze. Lectures on condensed mathematics, 2019. URL: https://people.mpim-bonn.mpg.de/scholze/Condensed.pdf.

[bib.bib16] [16] Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856–941, 2018. doi:10.1017/S0960129517000147.

[bib.bib17] [17] Michael Shulman. All $(\infty,1)$ -toposes have strict univalent universes. arXiv preprint, 2019. arXiv:1904.07004.

[bib.bib18] [18] Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential colimits in homotopy type theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), page 14. ACM, New York, [2020] ©2020. doi:10.1145/3373718.3394801.

[bib.bib19] [19] Paul Taylor. Abstract Stone duality, 2011. URL: https://www.paultaylor.eu/ASD/.

[bib.bib20] [20] Niels van der Weide. The internal languages of univalent categories, 2024. doi:10.48550/arXiv.2411.06636.

[bib.bib21] [21] Steven Vickers. Locales and toposes as spaces. In Handbook of spatial logics, pages 429–496. Springer, 2007. doi:10.1007/978-1-4020-5587-4_8.

[bib.bib22] [22] David Wärn. Eilenberg-Maclane spaces and stabilisation in homotopy type theory. J. Homotopy Relat. Struct., 18(2-3):357–368, 2023. doi:10.1007/s40062-023-00330-5.

[bib.bib23] [23] David Wärn. On internally projective sheaves of groups, 2024. arXiv:2409.12835.

A Foundation for Synthetic Stone Duality

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

Introduction

1 Stone duality

1.1 Preliminaries

▶ Remark 1.1.

Definition 1.2.

Definition 1.3.

▶ Remark 1.4.

▶ Remark 1.5.

Example 1.6.

Definition 1.7.

Example 1.8.

Lemma 1.9.

Proof.

1.2 Axioms

Axiom 1 (Stone duality).

Axiom 2 (Surjections are formal surjections).

Axiom 3 (Local choice).

Axiom 4 (Dependent choice).

1.3 Anti-equivalence of 𝖡𝗈𝗈𝗅𝖾ω and 𝖲𝗍𝗈𝗇𝖾

▶ Remark 1.10.

▶ Remark 1.11.

Lemma 1.12.

Proof.

Corollary 1.13.

Proof.

1.4 Principles of omniscience

Theorem 1.14 (The negation of the weak lesser principle of omniscience (¬WLPO)).

Proof.

Theorem 1.15.

Proof.

Corollary 1.16 (Markov’s principle (MP)).

Proof.

Theorem 1.17 (The lesser limited principle of omniscience (LLPO)).

Proof.

Lemma 1.18.

Proof.

1.5 Open and closed propositions

Definition 1.19.

▶ Remark 1.20.

Lemma 1.21.

Proof.

Corollary 1.22.

Proof.

Lemma 1.23.

Proof.

Lemma 1.24.

Proof.

1.6 Types as spaces

Definition 1.25.

▶ Remark 1.26.

2 Overtly discrete spaces

Definition 2.1.

▶ Remark 2.2.

Lemma 2.3.

Lemma 2.4.

Corollary 2.5.

2.1 Closure properties of 𝖮𝖣𝗂𝗌𝖼

Lemma 2.6.

Lemma 2.7.

2.2 𝖮𝗉𝖾𝗇 and 𝖮𝖣𝗂𝗌𝖼

Lemma 2.8.

Proof.

Corollary 2.9.

Corollary 2.10 (transitivity of openness).

▶ Remark 2.11.

Lemma 2.12.

Proof.

2.3 Relating 𝖮𝖣𝗂𝗌𝖼 and 𝖡𝗈𝗈𝗅𝖾ω

Lemma 2.13.

$\blacktriangleright$ Remark 1.1.

$\blacktriangleright$ Remark 1.4.

$\blacktriangleright$ Remark 1.5.

1.3 Anti-equivalence of $\mathsf{Boole}_{\omega}$ and $\mathsf{Stone}$

$\blacktriangleright$ Remark 1.10.

$\blacktriangleright$ Remark 1.11.

Theorem 1.14 (The negation of the weak lesser principle of omniscience ( $\neg$ WLPO)).

$\blacktriangleright$ Remark 1.20.

$\blacktriangleright$ Remark 1.26.

$\blacktriangleright$ Remark 2.2.

2.1 Closure properties of $\mathsf{ODisc}$

2.2 $\mathsf{Open}$ and $\mathsf{ODisc}$

$\blacktriangleright$ Remark 2.11.

2.3 Relating $\mathsf{ODisc}$ and $\mathsf{Boole}_{\omega}$

$\blacktriangleright$ Remark 2.15.

$\blacktriangleright$ Remark 2.16.

$\blacktriangleright$ Remark 3.4.

3.2 $\mathsf{Closed}$ and $\mathsf{Stone}$

$\blacktriangleright$ Remark 3.15.

$\blacktriangleright$ Remark 4.8.