Homotopy Type Theory UMyn8W7b (Rev #2, changes)

Definition I found on the HoTT zulip chat. TODO: see if it is worthwhile to rephrase it using open intervals.

Let $(L, U)$ be a pair of functions from the type of rational numbers $\mathbb{Q}$ to Sierpinski space $1_\bot$, i.e. $(L, U): (\mathbb{Q} \to 1_\bot) \times (\mathbb{Q} \to 1_\bot)$. $(L, U)$ is said to be a Dedekind cut if it comes equipped with the type family $isDedekindCut: (\mathbb{Q} \to 1_\bot) \times (\mathbb{Q} \to 1_\bot) \to \mathcal{U}$, defined by:

The type of Dedekind real numbers is defined as follows:

definition in terms of open intervals

see also: locale of real numbers

predicative definition: an open in the real number is a function $I: \mathbb{Q} \times \mathbb{Q} \to 1_\bot$ that satisfies the four properties listed below:

The opens form a sub-poset of the function poset $\mathbb{Q} \times \mathbb{Q} \to 1_\bot$. This poset is in fact a $\sigma$-frame, as we will now show. (It is not a sub-$\sigma$-frame of the function poset, since the joins are different. It is a sub-$\sigma$-complete distributive lattice of the function poset, although this seems to be a red herring at least for countably infinitary meets, since those are not part of the frame structure that we need.)