Add definitions for function-like relations

[Taneb]

From https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/Functional.20relation.3F/with/600727343

I've dithered and ruminated on the names for a while my initial choices were Injective, Functional, Total, and Surjective, but:

• Total is already defined in this module to be a total order
• Injective and Surjective conflict with definitions in Function.Definitions, both of which are imported unqualified in several places
• Tom de Jong on Zulip points out that Functional may imply a total function

I took these names from https://en.wikipedia.org/wiki/Binary_relation#Definition but I'm still open to further suggestions

[jamesmckinna]

Re: existing names

• Total has been a wart for a while (various issues have commented on this, as far back as Misnomer: Relation.Binary.Definitions.Total #453 ) so maybe we should consider a v3.0 breaking change? Otherwise, Entire is a usage I have seen for Surjective in this context, IIRC
• does the unqualified import of Function.Definitions matter, when such things could be made qualified (or is that a maintenance anti-pattern?)

In any case, surely we should be guided by the thought that the definitions (and names!) should be appropriately coherent with Function.Definitions such that if f has property P from there, then the Graph relation of f should have the corresponding property P from Relation.Definitions? Cf. #2981 we'd maybe eventually need to refactor to have the dependently-typed Graph.View defined there reconciled with the more modest/simpler

Graph : Rel B ℓ → (A → B) → REL A B ℓ
Graph _≈_ f x y = f x ≈ y