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:

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: