Homotopy Type Theory locator > history (Rev #3)

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 \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.