## Definition ## Given a type $T$ with a [[dense strict order]], a **locator** for a term $c:F$ is a dependent function $$\epsilon(c):\prod_{a:F} \prod_{b:F} (a,b) \to ((a,c) + (c,b))$$ where $(a,b)$ is an [[open interval]]. ## See also ## * [[Dedekind cut structure]] * [[Dedekind cut]] * [[interval cut]] * [[computable real number]] ## References ## * Auke B. Booij, Extensional constructive real analysis via locators, ([abs:1805.06781](https://arxiv.org/abs/1805.06781))