Homotopy Type Theory locator > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

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

References

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

Revision on April 22, 2022 at 20:41:45 by Anonymous?. See the history of this page for a list of all contributions to it.