# Homotopy Type Theory locator > history (changes)

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

## 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,b) \to ((a,c) + (c,b))$

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