## Definition ## Given an [[Archimedean ordered field]] $F$, a **locator** for a term $c:F$ is a term $$\epsilon:\prod_{a:F} \prod_{b:F} (a \lt b) \to ((a \lt c) + (c \lt b))$$ ## See also ## * [[Dedekind cut structure]] * [[Dedekind cut]] * [[interval cut]] ## References ## * Auke B. Booij, Extensional constructive real analysis via locators, ([abs:1805.06781](https://arxiv.org/abs/1805.06781))