[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \section{In dependent type theory} In [[dependent type theory]], given a type $X$, the type of [[subtypes]] of $X$ is the [[function type]] $X \to \Omega$, where $\Omega$ is the [[type of all propositions]] with the type reflector type family $P:\Omega \vdash \mathrm{El}_\Omega(P) \; \mathrm{type}$. A **[[topological space]]** is a type $X$ with a type of subtypes $O(X) \subseteq (X \to \Omega)$ with canonical embedding $i_O:O(X) \hookrightarrow (X \to \Omega)$, called the open sets of $X$, which are closed under finite intersections and arbitrary unions. Given a topological space $(X, O(X))$, the [[specialization order]] is given by the type $$\prod_{U:O(X)} \mathrm{El}_\Omega((i_O(U))(x)) \to \mathrm{El}_\Omega((i_O(U))(y))$$ and for all elements $x:X$, there is an element $$\mathrm{refl}_{SpecOrd}(x):\prod_{U:O(X)} T((i_O(U))(x)) \to T((i_O(U))(x))$$ defined by the [[identity function]] on $T((i_O(U))(x))$ $$\mathrm{refl}_{SpecOrd}(x, U) \coloneqq \mathrm{id}_{T((i_O(U))(x))}$$ Since $\mathrm{El}_\Omega((i_O(U))(x))$ and $\mathrm{El}_\Omega((i_O(U))(y))$ are both [[h-propositions]] and h-propositions are closed under [[function types]] and [[dependent product types]], the specialization order is valued in propositions. A **Kolmogorov topological space** or **$T_0$-space** is a topological space where the canonical function $$\mathrm{idToSpecOrd}(x, y):x =_X y \to \left(\prod_{U:O(X)} \mathrm{El}_\Omega((i_O(U))(x)) \to \mathrm{El}_\Omega((i_O(U))(y))\right) \times \left(\prod_{U:O(X)} \mathrm{El}_\Omega((i_O(U))(y)) \to \mathrm{El}_\Omega((i_O(U))(x))\right)$$ defined by $$\mathrm{idToSpecOrd}(x, x)(\mathrm{id}_X(x)) \coloneqq \mathrm{refl}_{SpecOrd}(x)$$ is an [[equivalence of types]] for all $x:X$ and $y:X$: $$T_0(x, y):\mathrm{isEquiv}(\mathrm{idToSpec}(x, y))$$ Since the specialization order is valued in propositions, the $T_0$ separation axiom ensures that the type is a [[set]]. category: redirected to nlab