Homotopy Type Theory Sandbox (changes)

Topology, predicatively

We do not have power sets so we cannot define topological spaces. Instead, we have to use a dominance such as the initial $\sigma$-frame $\Sigma$.

• $\mathrm{LEM}_\Sigma$: The boolean domain is the initial $\sigma$-frame.

A predicative topological space consists of a set $X$ and a sub-$\sigma$-frame $\tau \subseteq X^\Sigma$ of the set of functions into the initial $\sigma$-frame.

A base or basis for (or “of”) $X$ (or $\tau$) is a collection $B \subseteq \tau$ – whose members are called basic open subsets or generating open subsets – such that every open subset is a countable union of basic ones.

A predicative topological space is second-countable if $B$ is a countable set.