[[!redirects Sandbox &gt; history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Let $\mathbb{R}$ be a sequentially Cauchy complete Archimedean ordered field, and let $$\mathbb{R}^\mathcal{L} \coloneqq \sum_{l:\mathbb{R}} \sum_{x:\mathbb{N} \to \mathbb{Q}} \prod_{\epsilon:\mathbb{Q}_+} \sum_{N:\mathbb{N}} \prod_{n:\mathbb{N}} (n \geq N) \to (\vert x(n) - l \vert \lt \epsilon)$$ be the set consisting of a real number and a Cauchy sequence of rational numbers constructively converging to the real number. Then a function $f:\mathbb{R} \to \mathbb{R}$ lifts to Cauchy sequences of rational numbers if there is a function $f^\mathcal{L}:\mathbb{R}^\mathcal{L} \to \mathbb{R}^\mathcal{L}$ such that $\pi_1 \circ f^\mathcal{L} = f \circ \pi_1$, where $\pi_1:\mathbb{R}^\mathcal{L} \to \mathbb{R}$ is the first projection function of the dependent sum. category: redirected to nlab