The $\mathcal{U}$-large Dedekind real closed intervals for a universe$\mathcal{U}$ is defined as the type of $\mathcal{U}$-interval cuts on the rational numbers$\mathbb{Q}$ in a universe: $\mathbb{R}_\mathcal{U} \coloneqq IntervalCut_\mathcal{U}(\mathbb{Q})$.