[004G] Subtoposes and modalities

Having [002Y] in mind, we only consider subtoposes of $\mathord {\textnormal {\textsf {1}}}$ . Subtoposes of a general topos $$X$$ are subtoposes of $\mathord {\textnormal {\textsf {1}}}$ in the type theory of spaces in $\mathord {\textnormal {\textsf {Sh}}}(X)$ .

[004H] Definition

Let $$T$$ be a base type theory. We work in $$T$$ . We say a topos $$X$$ is a subtopos (of $\mathord {\textnormal {\textsf {1}}}$ ) if the counit of the constant sheaf and global section adjunction for $$X$$ is an equivalence. We write $\mathord {\textnormal {\textsf {SubTop}}}$ for the type of subtoposes.

We refer the reader to [Rijke--Shulman--Spitters--2020-0000] for the theory of modalities in homotopy type theory.

[004I] Notation

Let $$T$$ be a base type theory. We work in $$T$$ . Let $$X$$ be a subtopos. Then the constant sheaf and global section adjunction for $$X$$ yields a lex modality on $\mathcal {U}(0)$ . We refer to the lex modality as $\mathord {\textnormal {\textsf {m}}}_{X}$ .

[004J] Exercise

Let $$T$$ be a base type theory. We work in $$T$$ . Let $$X$$ be a subtopos. Then the lex modality $\mathord {\textnormal {\textsf {m}}}_{X}$ is accessible. (This might require additional axioms.)

[004K] Notation

Let $$T$$ be a base type theory. We work in $$T$$ . We refer to the type of lex accessible modalities on $\mathcal {U}(0)$ as $\mathord {\textnormal {\textsf {LAM}}}$ .

[004L] Exercise

Let $$T$$ be a base type theory. We work in $$T$$ . Then the function $X\mapsto \mathord {\textnormal {\textsf {m}}}_{X}:\mathord {\textnormal {\textsf {SubTop}}}\rightarrow \mathord {\textnormal {\textsf {LAM}}}$ is an equivalence.