Homotopy Type Theory locator > history (changes)

Showing changes from revision #5 to #6: Added | Removed | Changed


< locator

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


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