[ add ] `Function.Metric.Core.DistanceRelation`

[jamesmckinna]

And then Triangle probably requires a slightly more involved refactoring to consider not just Function.Metric.Core.DistanceFunction but also Function.Metric.Core.DistanceRelation?
(Obviously out-of-scope here, but as ever... note-to-self/-selves)

Originally posted by @jamesmckinna in #3067 (comment)

Not every 'metric' arises as a (2-place) function d, valued in some hypothetical space I of possible 'measurement'; cf. Lawvere on generalised metric spaces as enriched categories: valuation in (the objects of) a (symmetric) monoidal category...

... rather, it may be 'easier' to capture via a relation D, relative to some pre-/partial-order _≲_ on I, such that D x y i is proxy for d x y ≲ i.

Cf. Data.List.Relation.Binary.Distance.Levenshtein.Core.Triangle defined in #3015

UPDATED: re title. Perhaps this should in fact be Relation.Metric.Core.Distance{Relation}? The pleonastic Relation, like that of Function, seems a bit much, looking again...?

Proposal:

• deprecate Function.Metric.Core.DistanceFunction in favour of Function.Metric.Core.Distance
• add Relation.Metric.Core.Distance in like fashion
• relate the two approaches

Question:

• which should be conceptually prior? Cf. Add definitions for function-like relations #3001