## Idea ## Since a [[dense strict order]] has an order topology associated with it, one could create the locale with the open sets of a dense strict order, which are the open intervals in the dense strict order. ## Definition ## er, better Let $T$ be a type with a [[dense strict order]] $\lt$. Let $(a, b)$ and $(c, d)$ be bounded [[open interval]]s in $T$, $(e, \infty)$ be a [[lower bounded open interval]] in $T$, and $(-\infty, f)$ be an [[upper bounded open interval]] in $T$. $T$ is the unbounded open interval in $T$, and is denoted as $(-\infty, \infty)$. Then $(a, b) \subseteq (c, d)$ if $c \leq a$ and $b \leq d$, $(a, b) \subseteq (e, \infty)$ if $e \leq a$, and $(a, b) \subseteq (-\infty, f)$ if $b \leq f$. By defintion, every bounded open interval $(a, b) \subseteq (-\infty, \infty)$, every lower bounded open interval $(a, \infty) \subseteq (-\infty, \infty)$, every upper bounded open interval $(-\infty, b) \subseteq (-\infty, \infty)$, and $(-\infty, \infty) \subseteq (-\infty, \infty)$, which means that $(-\infty, \infty)$ is the top element in the large poset of open intervals in $T$. The intersection of two open intervals $(a, b)$ and $(c, d)$ is simply $(a, b) \cap (c, d)$ of the two subtypes. The empty interval $\emptyset$ is any interval where $a \geq b$, and by definition it is the bottom element in the large poset of open intervals in $T$. The union of two open intervals $(a, b)$ and $(c, d)$, $(a, b) \cup (c, d)$, exists and is equal to $(a, d)$ if and only if $c \lt b$. In fact, for any family of open intervals $((a_n,b_n))_{[0, n]}$ for $n:\mathbb{N}$, $a_{i+1} \lt b_i$ for $i:[0, n-1]$ if and only if the union of the family of open intervals exist and is equal to $(a_0, b_n)$ $$\left(\prod_{i:[0, n-1]} (a_{i+1} \lt b_i)\right) \to \left(\bigcup_{i:[0, n]} (a_i, b_i) = (a_0, b_n)\right)$$ The union of an arbitrary family of open intervals $((a_j, b_j))_{j:J}$ is defined such that for every open interval $$(c, d) \subseteq \bigcup_{j:J} (a_j, b_j)$$ if and only if (1) $(c, d)$ is the empty interval or (2) there exists a family of open intervals $((c_n,d_n))_{[0, n]}$ for $n:\mathbb{N}$ such that $$\left(\prod_{i:[0, n-1]} (c_{i+1} \lt d_i)\right) \to \left(\bigcup_{i:[0, n]} (c_i, d_i) = (c_0, d_n)\right)$$ and $$\prod_{i:[0, n]} \left[\sum_{j:J} (c_i,d_i) \subseteq (a_j, b_j)\right]$$ to be continued... I'm probably going to use Steve Vicker's presentation rather than Toby Bartel's. ## See also ## * [[localic real numbers]]