Homotopy Type Theory Dedekind cut structure real numbers > history (Rev #3)

Dedekind cut structure real numbers

Large Dedekind cut structure real numbers

The $\mathcal{U}$-large Dedekind cut structure real numbers for a universe $\mathcal{U}$ is defined as the type of all pairs of subtypes of the rational numbers $\mathbb{Q}$ which have a $\mathcal{U}$-Dedekind cut structure:

$\mathbb{R}_\mathcal{U} \coloneqq \sum_{(L, R):Sub_\mathcal{U}(\mathbb{Q}) \times Sub_\mathcal{U}(\mathbb{Q})} \left[DedekindCutStructure_\mathcal{U}(L, R)\right]$

Sigma-Dedekind cut structure real numbers

The $\Sigma$-Dedekind cut structure real numbers for a $\sigma$-frame $\Sigma$ is defined as the type of all pairs of open subtypes of the rational numbers $\mathbb{Q}$ which have a $\Sigma$-Dedekind cut structure:

$\mathbb{R}_\Sigma \coloneqq \sum_{(L, R):(\mathbb{Q} \to \Sigma) \times (\mathbb{Q} \to \Sigma)} \left[DedekindCutStructure_\Sigma(L, R)\right]$