ordered family of equivalences
An ordered family of equivalences (OFE) is a set together with a sequence of equivalences satisfying the following criteria:
- is total; i.e., for all ;
- the equivalences are finer for larger ; i.e., if , then (hence );
- the intersection of all the equivalences is equality; i.e., .
1. intuition
Intuitively, an OFE describes a discrete notion of distance. Saying that is like saying that and are “ -close” to each other. Everything is -close to everything else, and a point is always -close to itself (and only itself).
2. as metric spaces
In fact, an OFE can equivalently be viewed as a kind of metric space. Define Then is a metric on .
This is useful because it lets us transport concepts from the theory of metric spaces back into the theory of OFEs.
3. category of OFEs
The natural notion of mapping between OFEs and is a function such that for all . OFEs equipped with this notion of mapping form a category.