testing stuff here Definition I found on the HoTT zulip chat. TODO: see if it is worthwhile to rephrase it using [[open interval]]s. 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: $$\begin{aligned} isDedekindCut(L, U) & := \Vert \sum_{q: \mathbb{Q}} L(q) = \top \Vert \\ & \times \Vert \sum_{r: \mathbb{Q}} U(r) = \top \Vert \\ & \times \prod_{q:\mathbb{Q}} \prod_{q^\prime: \mathbb{Q}} ((q \lt q^\prime) \times (L(q^\prime) = \top) \to (L(q) = \top)) \\ & \times \prod_{r: \mathbb{Q}} \prod_{r^\prime: \mathbb{Q}} ((U(r^\prime) = \top) \times (r^\prime \lt r) \to (U(r) = \top)) \\ & \times \prod_{q: \mathbb{Q}} \left((L(q) = \top) \to \Vert \sum_{q^\prime: \mathbb{Q}} (q \lt q^\prime) \times (L(q^\prime) = \top) \Vert \right) \\ & \times \prod_{r: \mathbb{Q}} \left((U(r) = \top) \to \Vert \sum_{r^\prime: \mathbb{Q}} (U(r^\prime) = \top) \times (r^\prime \lt r) \Vert \right) \\ & \times \prod_{q: \mathbb{Q}} \prod_{r: \mathbb{Q}} ((L(q) = \top) \times (U(r) = \top) \to (q \lt r)) \\ & \times \prod_{q: \mathbb{Q}}, \prod_{r: \mathbb{Q}} \left((q \lt r) \to \Vert (L(q) = \top) + (U(r) = \top) \Vert \right) \\ \end{aligned}$$ The type of __Dedekind real numbers__ is defined as follows: $$\mathbb{R}_D := \Sigma((L, U):(\mathbb{Q} \to 1_\bot) \times (\mathbb{Q} \to 1_\bot)).isDedekindCut(L, U)$$ definition in terms of open intervals $$\begin{aligned} isDedekindCut(C) & := \Vert \sum_{q: \mathbb{Q}} \sum_{r: \mathbb{Q}} I(q, r) = \top \Vert \\ \end{aligned}$$ see also: [[nlab: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: $$a:\mathbb{Q}, b:\mathbb{Q} \vdash p_1(a, b): (a \geq b) \to (I(a, b) = \top)$$ $$a:\mathbb{Q}, b:\mathbb{Q}, c:\mathbb{Q}, d:\mathbb{Q} \vdash p_2(a, b, c, d): (a \geq b) \times (I(b, c) = \top) \times (c \geq d) \to (I(a, d) = \top)$$ $$a:\mathbb{Q}, b:\mathbb{Q}, c:\mathbb{Q}, d:\mathbb{Q} \vdash p_3(a, b, c, d): (I(a, b) = \top) \times (b \gt c) \times (I(c, d) = \top) \to (I(a, d) = \top)$$ $$a:\mathbb{Q}, b:\mathbb{Q}, c:\mathbb{Q}, d:\mathbb{Q} \vdash p_4(a, b, c, d): ((a \lt b) \times (c \lt d) \to (I(b, c) = \top)) \to (I(a, d) = \top)$$ 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|$\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 lattice|$\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.)