[ add ] Relation.Binary._Reflects_⟶_ as a companion to _Preserves_⟶_

[jamesmckinna]

A preparatory PR ahead of tackling #1436 in earnest.
NB:

• illustrative refactoring of Function.Definitions.Injective
• surprisingly, attempting to do the same for Function.Definitions.Congruent in terms of Preserves results in many, many, unsolved metas... sigh. See [ refactor ] Function.Definitions and Function.Consequences? #2565 for details

[gallais]

What's the intuition for the Reflects name? Does it have any relationship to the ssreflect
style Reflects that we already have? http://agda.github.io/agda-stdlib/v2.1.1/Relation.Nullary.Reflects.html#1010

[jamesmckinna]

What's the intuition for the Reflects name? Does it have any relationship to the ssreflect style Reflects that we already have? http://agda.github.io/agda-stdlib/v2.1.1/Relation.Nullary.Reflects.html#1010

Nothing to do with Reflects as in ssreflect, nor Relation.Nullary.Reflects!

But absolutely conventional usage in first-order logic/relational algebra (eg. discussion in McKinna&Pollack 1999 on preserving and reflecting α-conversion in λ-calculus representations...): the aim is to [DRY] reconcile Function.Definitions.Injective and Algebra.Definitions.Cancellative as specialisations of the concept...