Homotopy Type Theory locator > history (Rev #5)

Definition

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

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

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

See also

References

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

Revision on May 10, 2022 at 02:31:41 by Anonymous?. See the history of this page for a list of all contributions to it.