#
Homotopy Type Theory
locator > history (changes)

Showing changes from revision #5 to #6:
Added | ~~Removed~~ | ~~Chan~~ged

## Definition

< locator

~~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

~~
~~~~
~~## References

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

Last revised on June 9, 2022 at 05:10:36.
See the history of this page for a list of all contributions to it.