[ DRY ] Refactor `Function.*` to rationalise the existence of a section to a given `Surjective f`

[jamesmckinna]

Lots of repetition in the hierarchy of various private definitions of a (not-necessarily Congruent) section : B → A to a given Surjective f for f : A → B, which should be rationalised into an appropriate eg. manifest field of the various Structures and Bundles...

Issues: cf. #2274 etc.

• is a property, derived from Function.Definitions.Surjective?
• is it a manifest field of Function.Structures.IsSurjection cf. IsGroup? [DRY] why is _≉_ defined both for Algebra.Bundles.Raw.RawX bundles, and via Setoid instances, for Algebra.Bundles.X? #2274 / Add new operations (cf. RawQuasigroup) to IsGroup #2251
• is it a manifest field of Function.Bundles.Surjection?

plus

• naming: section (neutral?), to⁻ (as now), or from emulating usage already present in other Structures with already a well-defined section, moreover Congruent? UPDATED: [ refactor ] fixes #2568; proves full symmetry for Bijection #2569 now makes the choice of from...
• ...

UPDATED: #2569 is a comprehensive attempt at tackling this, up to, but not (yet!) including breaking changes to remove the dependency on congruence of section in the proofs of symmetry for IsBijective and Bijection (because, for an Injective function f, its section automatically satisfies Congruent)

The solution chosen goes via a new module Section in Function.Consequences (could/should move to somewhere on its own?), which develops the comprehensive theory of the section map, but then successively re-exports that structure as manifest fields of both Function.Structures.{IsSurjection|IsBijection} as well as Function.Bundles.{Surjection|Bijection}, so in a sense the answer to the above design issues is: yes!