# Homotopy Type Theory locale of open intervals > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

## 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 intervals 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.