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

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

Definition

Given an a type~~Archimedean ordered field~~ $T$ with a ~~$F$~~ dense strict order, a locator for a term $c:F$ is a ~~term~~ dependent function

ϵ (c) : \prod_{a : F} \prod_{b : F} (a < b) \to ((a < c) + (c < b))

~~\epsilon:\prod_{a:F}~~ \epsilon(c):\prod_{a:F} \prod_{b:F} (a \lt b) \to ((a \lt c) + (c \lt b))

See also

References

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

Revision on April 23, 2022 at 07:55:16 by Anonymous?. See the history of this page for a list of all contributions to it.