Homotopy Type Theory locale of open intervals > history (Rev #2)


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.


er, better

Let TT be a type with a dense strict order <\lt. Let (a,b)(a, b) and (c,d)(c, d) be bounded open intervals in TT, (e,)(e, \infty) be a lower bounded open interval in TT, and (,f)(-\infty, f) be an upper bounded open interval in TT. TT is the unbounded open interval in TT, and is denoted as (,)(-\infty, \infty). Then (a,b)(c,d)(a, b) \subseteq (c, d) if cac \leq a and bdb \leq d, (a,b)(e,)(a, b) \subseteq (e, \infty) if eae \leq a, and (a,b)(,f)(a, b) \subseteq (-\infty, f) if bfb \leq f.

By defintion, every bounded open interval (a,b)(,)(a, b) \subseteq (-\infty, \infty), every lower bounded open interval (a,)(,)(a, \infty) \subseteq (-\infty, \infty), every upper bounded open interval (,b)(,)(-\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 TT.

The intersection of two open intervals (a,b)(a, b) and (c,d)(c, d) is simply (a,b)(c,d)(a, b) \cap (c, d) of the two subtypes.

The empty interval \emptyset is any interval where aba \geq b, and by definition it is the bottom element in the large poset of open intervals in TT.

The union of two open intervals (a,b)(a, b) and (c,d)(c, d), (a,b)(c,d)(a, b) \cup (c, d), exists and is equal to (a,d)(a, d) if and only if c<bc \lt b.

In fact, for any family of open intervals ((a n,b n)) [0,n]((a_n,b_n))_{[0, n]} for n:n:\mathbb{N}, a i+1<b ia_{i+1} \lt b_i for i:[0,n1]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)(a_0, b_n)

( i:[0,n1](a i+1<b i))( i:[0,n](a i,b i)=(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((a_j, b_j))_{j:J} is defined such that for every open interval

(c,d) j:J(a j,b j)(c, d) \subseteq \bigcup_{j:J} (a_j, b_j)

if and only if (1) (c,d)(c, d) is the empty interval or (2) there exists a family of open intervals ((c n,d n)) [0,n]((c_n,d_n))_{[0, n]} for n:n:\mathbb{N} such that

( i:[0,n1](c i+1<d i))( i:[0,n](c i,d i)=(c 0,d n))\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)


i:[0,n][ j:J(c i,d i)(a j,b j)]\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?

Revision on April 22, 2022 at 01:05:11 by Anonymous?. See the history of this page for a list of all contributions to it.