Homotopy Type Theory locator > history (changes)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

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

Definition

< locator

Given a type

category: redirected to nlab
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)

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

EditDiscussPrevious revisionHide changesHistory (5 revisions) Print Source