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

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

Definition

Given a type $T$ with a dense strict order, a locator for a term $c:F$ is a dependent function

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

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

where $(a,b)$ is an open interval.

See also

References

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

Revision on May 6, 2022 at 07:04:26 by Anonymous?. See the history of this page for a list of all contributions to it.