nLab lifting to locators

Contents

Contents

Definition

Let D\mathbb{R}_D be the Dedekind real numbers, and let \mathbb{R}_\mathcal{L} be the subset of all Dedekind real numbers with a locator, with canonical embedding η: D\eta:\mathbb{R}_\mathcal{L} \to \mathbb{R}_D. A function f: D Df:\mathbb{R}_D \to \mathbb{R}_D lift to locators if it comes with a function f : f_\mathcal{L}:\mathbb{R}_\mathcal{L} \to \mathbb{R}_\mathcal{L} such that the following square in Set commutes:

f η η D f D \array{& \mathbb{R}_\mathcal{L} & \overset{f_\mathcal{L}}\rightarrow & \mathbb{R}_\mathcal{L} & \\ \eta & \downarrow &&\downarrow & \eta\\ &\mathbb{R}_D & \underset{f}\rightarrow& \mathbb{R}_D & \\ }

See also

References

  • Auke Booij, Extensional constructive real analysis via locators, (abs:1805.06781)

Last revised on May 9, 2022 at 03:52:10. See the history of this page for a list of all contributions to it.