Homotopy Type Theory Sandbox (Rev #1)

testing stuff here

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:

\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}